3 ms·
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 dis
by compacct27 3y 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.