Lean (proof assistant)
ID: lean-proof-assistant
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
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.
New to topics? Read the docs here!