Nice, Terence Tao (Fields Medal 2006) found a bug in one of his papers using Lean 4. mathstodon.xyz/@tao/111287749…
Lean
777 posts
Lean is a dependently-typed programming language and theorem prover.
- 🔥 @GoogleDeepMind just dropped their "formal conjectures" project - formalizing statements of math's biggest unsolved mysteries in #LeanLang and #Mathlib! This Google-backed project is a HUGE step toward developing "a much richer dataset of formalized conjectures", valuable
- 📣 We're excited to share the new lean-lang.org! Relaunching our website was a key deliverable in our Year 2 roadmap to provide "improved navigation and access to valuable content, resources, and tools." We hope you like it! #LeanLang #LeanProver
- Terry Tao's blog post on the PFR project is essential reading for anybody interested in formal mathematics with Lean.
- 🎉 Lean 4.22.0 is here! This marks the culmination of our Year 2 roadmap. Two major highlights: 🧠 grind tactic: New SMT-style automated reasoning with theory-specific solvers and Gröbner basis support 🏗️ New compiler: Closes long-standing issues and sets the foundation for
- Terence Tao has released a new #LeanLang project that connects #FormalVerification with #MathematicsEducation: The companion to "Analysis I" is intended to provide a new avenue for engaging with the proofs and exercises in Tao's foundational "Analysis I" text. 👇
- DeepMind has formalized a theoretical result related to AI safety in Lean. 😍 Paper: arxiv.org/abs/2311.14125. Code: github.com/google-deepmin…
- We are super excited to see daily updates from Terence Tao describing his experience learning Lean. Terence Tao is one of the greatest living mathematicians and a Fields medalist.
GIF- We are excited to share the news of the Lean Focused Research Organization (FRO): lean-fro.org! A new nonprofit dedicated to advancing the Formal Mathematics revolution, we aim to tackle the challenges of scalability, usability, and proof automation in Lean.
- Congratulations to the @mathematics_inc team on their announcement! AI-assisted autoformalization is a promising area with significant potential impact. We're looking forward to the community discussion and seeing how this space evolves. #AI #ProofAutomation #FormalMathematicsToday we're announcing Gauss, our first autoformalization agent that just completed Terry Tao & Alex Kontorovich's Strong Prime Number Theorem project in 3 weeks—an effort that took human experts 18+ months of partial progress.
- "Theorem Proving in Lean 4" is the essential guide for anyone using Lean for mathematical proofs. This comprehensive resource is kept up-to-date with each new Lean release, ensuring all examples and techniques remain current with the latest Lean developments. It covers
- Big day for Lean! Alex Gerko of XTX Markets is donating $10M to the Lean FRO and the new Mathlib Initiative to support the future of formal mathematics and machine-checked proofs. Thank you, Alex Gerko and Convergent Research, for believing in the mission. Read the full







