|
|
|
|
|
|
by compacct27
894 days ago
|
|
|
It's been amazing learning about this. From "The Little Typer" book to Computerphile's videos on dependent (and homotopy, somewhat related?) type theory, to discovering Lean for interactive (math) proof construction, the history of it all dating back to Bertrand Russel trying to explain math from first principles, just wow. So lucky to live in a world where this is true. |
|
|