Source 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
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.TODO none? Seriously?
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.