{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

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

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.


Lean

Lean (proof assistant)

{tag=Formal proof}

Bibliography:
* https://mathoverflow.net/questions/488721/formal-proofs-of-the-prime-number-theorem


Ciro Santilli @cirosantilli 37

 Incoming links: Formal proof of the prime number theorem