Ciro Santilli
OurBigBook.comSource code:
- github.com/leanprover/lean4 why a separate repo per version... but it is what it is.
- github.com/leanprover/lean
The way Lean and Coq mix programming and mathematics is a thing of great beauty. This is especially notable in lean as you start to play with with things such as:
partialenv lean functions, and usingterminates_byto prove that certain functions terminate. Lean requires explicitly known if functions terminate or not to be able to use them in proofs.noncomputablefunctions. Lean allows you to define mathematical functions which you can't actually execute, and it tracks that explicitly
They are huge fans of Unicode characters! Check this out from a formal proof of the prime number theorem: github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/fbdbb5310d036d33b9797b35f3b04b08f2447a6e/PrimeNumberTheoremAnd/ZetaBounds.lean Here's map to Ascii: proofassistants.stackexchange.com/questions/954/does-lean-have-a-standard-ascii-representation/5289#5289
Their dependency graph thingy is just beautiful however: alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html
Their 2025 current installation method is bullshit, recommends VS Code extension on Ubuntu. Lol.
From CLI:Then when you run:it downloads the
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/envleanlean executable for you. Insane shit, could only come from a Microsoft mindset.