Adolfo NetoI interviewed Leo de Moura (the creator of #LeanLang) a few years ago, just at the start of the recent AI boom. Maybe I got the wrong impression, but I felt he left Microsoft because it was focusing too much on AI. Now his Lean FRO is working with several companies that use AI for math. And these
Formalization is not just about proving. It is about understanding, communicating, and building trust at a scale beyond our cognitive abilities."
#LeanLang
Lean: Extensible, Scalable, Trusted.
Slides by Leonardo de Moura
Paris, 2026
#LeanLang
#LeanProver
leodemoura.github.io/static/paris...
Lean: Extensible, Scalable, Tr...
Lean: Extensible, Scalable, Tr...
๐ ๐ฎ๐๐ต๐ ๐ฃ๐ฟ๐ผ๐ผ๐ณ๐ ๐ถ๐ป ๐๐ฒ๐ฎ๐ป - ๐๐ถ๐ฟ๐๐ ๐ฆ๐๐ฒ๐ฝ๐
#LeanLang
mathstodon.xyz/@rzeta0/1164...
Tariq (@[email protected])
Tariq (@[email protected])
Tariq (@[email protected])
Attached: 2 images ๐ ๐ฎ๐๐ต๐ ๐ฃ๐ฟ๐ผ๐ผ๐ณ๐ ๐ถ๐ป ๐๐ฒ๐ฎ๐ป - ๐๐ถ๐ฟ๐๐ ๐ฆ๐๐ฒ๐ฝ๐ You don't need to be a PhD to write simple maths proofs in Lean. This course takes you from a complete beginner, and gives you enough confidence to read and write simple proofs. Each chapter has one exercise, designed to build confidence, not destroy it! youtube: https://www.youtube.com/@LeanFirstSteps/videos free content: https://leanfirststeps.blogspot.com/p/contents.html book: https://www.amazon.com/dp/B0DWHS1RDJ #leanprover #education #maths
Signal Shot is a public moonshot to verify the Signal protocol and its Rust implementation using Lean. Not the math on paper. The actual code.
#LeanLang
leodemoura.github.io/blog/2026-4-...
Signal Shot: The Platform Is R...
Signal Shot: The Platform Is R...
Lean"Can we prove that Signal's cryptography is secure โ not just on paper, but in actual code?"
Signal Shot, launched today at the Software Verification in Lean workshop in Paris, is a public moonshot to formally verify the Signal protocol and its Rust implementation using Lean. A joint effort of Signal, the Beneficial AI Foundation, and the Lean FRO.
Open to contributions from anyone working on software verification, cryptography, protocol design, Rust, or Lean.
Lean 4.29.0 released with 453 changes.
Highlights: reduced startup time through static initialization of closed terms, simpler ๐๐๐๐๐๐๐๐๐๐๐๐๐ semantics improving predictability, higher-order Miller pattern support in ๐๐๐๐๐'s e-matching engine, and a significant overhaul to instance and reducibility handling.
Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.29.0/
Adolfo Neto"ZK proofs are headed for real-world deployment โ but writing correct ZK statements is tricky.
Our new post by James Parker introduces zkLean, a Lean library that defines a domain specific language for specifying and formally verifying ZK statements."
#LeanLang
https://www.galois.com/articles/zklean-a-dsl-for-zk-statement-verification
Leanstral: Open-Source foundation for trustworthy vibe-coding
by Mistral AI
#LeanLang
https://mistral.ai/news/leanstral
by Mistral AI
#LeanLang
https://mistral.ai/news/leanstral
Ruchira S. Datta