= Lean
{disambiguate=proof assistant}
{c}
{tag=Microsoft product}
{tag=Open source software}
{wiki}
= Lean
{c}
{synonym}
<Source code>:
* https://github.com/leanprover/lean4 why a separate repo per version... but it is what it is.
* https://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:
* `partial`env lean functions, and using `terminates_by` to prove that certain functions terminate. Lean requires explicitly known if functions terminate or not to be able to use them in proofs.
* `noncomputable` functions. 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>: https://github.com/AlexKontorovich/PrimeNumberTheoremAnd/blob/fbdbb5310d036d33b9797b35f3b04b08f2447a6e/PrimeNumberTheoremAnd/ZetaBounds.lean Here's map to Ascii: https://proofassistants.stackexchange.com/questions/954/does-lean-have-a-standard-ascii-representation/5289#5289
Their dependency graph thingy is just beautiful however: https://alexkontorovich.github.io/PrimeNumberTheoremAnd/web/dep_graph_document.html
Their 2025 current installation method is bullshit, recommends <VS Code> extension on Ubuntu. Lol.
From CLI:
``
curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source $HOME/.elan/env
``
Then when you run:
``
lean
``
it downloads the `lean` executable for you. Insane shit, could only come from a <Microsoft> mindset.
Back to article page
