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
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
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.