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
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.This tutorial has the merit of actually trying you to do some meaningful mathematics before teaching you a billion items of syntax and dependent type theory nuances.
Here is a specific minimal example of how to use mathlib4: proofassistants.stackexchange.com/questions/2526/how-to-run-lean4-with-mathlib-manually/5299#5299
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.