/home/
/braindump/
/longform/
metamath
2024-04-03 - Curry-Howard correspondence