= 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
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.
Back to article page
