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/env
lean
lean
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
This used to have the best name ever allowing you to say:to English speakers and watch their faces drop.
This will never work but OK. New custom language after Lean.
It seems to implement Zermelo-Fraenkel set theory.
Articles by others on the same topic
There are currently no matching articles.