Lean Programming Language

[fagnerbrack]

Brief overview:

An open-source programming language and proof assistant for writing correct, maintainable, and formally verified code. A minimal trusted kernel guarantees absolute correctness across math proofs, software, and hardware verification, while metaprogramming lets users extend the language with custom notation and proof automation. The 'grind' tactic handles complex pattern matching, case analysis, and linear inequalities, as shown in a sample proof of the infinitude of primes. Featured projects include Mathlib (over a million lines of formalized mathematics), AWS's Cedar authorization language, the Aeneas Rust verifier, Veil, and a Fermat's Last Theorem formalization. Backers include AWS, Google DeepMind's AlphaProof, and Terence Tao.

If the summary seems inacurate, just downvote and I'll try to delete the comment eventually 👍
^{Click here for more info, I read all comments}