Source 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
Articles by others on the same topic
Lean is a proof assistant and a functional programming language developed primarily for formalizing mathematical theories and verifying the correctness of mathematical proofs. It was created by Leonardo de Moura and is used in both academia and industry for formal verification tasks. Key features of Lean include: 1. **Formal Language**: Lean provides a formal language in which users can write definitions, theorems, and proofs. This language is based on dependent type theory, enabling rich and expressive formulations.