iiinova — where your digital self keeps evolving

Lean Focused Research Organization @lean-lang.org · 15/09/2026

Lean 4.34.0 is out: 159 changes. Three kernel soundness vulnerabilities fixed, all requiring deliberately constructed inputs rather than ordinary code. 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 is up to 6x faster. lean-lang.org/doc/referenc...

092

Lean Focused Research Organization @lean-lang.org · 21/08/2026

The Lean FRO Year 4 Part 1 roadmap, covering September 2026 through February 2027, is now published. It sets out our priorities for Lean and ecosystem support for the first half of our fourth year of operations. 🔗 Read the full roadmap here: lean-lang.org/fro/roadmap/... #LeanLang #LeanProver

074

Lean Focused Research Organization @lean-lang.org · 10/08/2026

Lean 4.33.0 is live! 208 changes: a smoother editor, automatic try? suggestions, and Float finally has a logical model instead of staying opaque. Full notes: lean-lang.org/doc/referenc... #LeanLang #LeanProver

081

Lean Focused Research Organization @lean-lang.org · 13/07/2026

Lean 4.32.0 is live. 102 changes, including the new do elaborator now on by default, a new module linter framework, and roughly a 10% speedup importing Mathlib. Full release notes: lean-lang.org/doc/referenc... #LeanLang #LeanProver #FormalVerification

062

Lean Focused Research Organization @lean-lang.org · 23/06/2026

We're grateful that @simonsfoundation.org has included Lean in three articles of their 2025 annual report. President David Spergel calls it "a proof assistant that brings rigorous machine-verified structure for testing theorems." 📄 www.simonsfoundation.org/series/2025-...

042

Lean Focused Research Organization @lean-lang.org · 18/06/2026

Lean 4.31.0 is live! 305 changes: verifiable do-block loops with no source changes required, mvcgen' (100x+ faster than mvcgen on some benchmarks), and lake lint with Batteries/Mathlib linters built in. lean-lang.org/doc/referenc... #LeanLang #LeanProver #OpenSource

061

Lean Focused Research Organization @lean-lang.org · 09/06/2026

The Proof in the Code, Kevin Hartnett's new book on the development of Lean and Mathlib, is out today. www.quantabooks.org/books/the-pr... To mark the launch, two online panels with the author on June 11 and 12, both 5pm UTC. Registration in the reply.

192

Lean Focused Research Organization @lean-lang.org · 03/06/2026

Two online panels for the launch of The Proof in the Code, @kevinhartnett.bsky.social's new book on Lean and Mathlib. The Mathematicians, June 11. The Builders, June 12. Both 5pm UTC. Learn more and register: The Mathematicians: forms.gle/w16jkmsMqB2g... The Builders: forms.gle/PsxPkq3x2pES...

053

Lean Focused Research Organization @lean-lang.org · 27/05/2026

Lean 4.30.0 is live! 306 changes: new 𝚜𝚢𝚖 => interactive tactic (𝚐𝚛𝚒𝚗𝚍-based, user-controlled), 𝚌𝚋𝚟 out of experimental, LCNF backend complete (~15% smaller binaries), and a full Lake cache overhaul. Release notes: lean-lang.org/doc/referenc...

053

Lean Focused Research Organization @lean-lang.org · 02/04/2026

🚀 Lean 4.29.0 is out! Faster startup, simpler 𝚗𝚘𝚗𝚌𝚘𝚖𝚙𝚞𝚝𝚊𝚋𝚕𝚎 semantics, higher-order Miller pattern support in 𝚐𝚛𝚒𝚗𝚍, and a significant overhaul to reducibility and instance handling. 453 changes! 🔗 lean-lang.org/doc/reference/latest/releases/v4.29.0/ #LeanLang #LeanProver

1152

Lean Focused Research Organization @lean-lang.org · 01/04/2026

1/3 New Lean use case: Veil, a multi-modal verification framework for distributed protocols from George Pîrlea, Vladimir Gladshtein, Elad Kinsbruner, Qiyuan Zhao, and Ilya Sergey at NUS.

2114

Lean Focused Research Organization @lean-lang.org · 27/02/2026

The Lean Y3 roadmap is building infrastructure to keep performance "visible and actionable." Radar automatically benchmarks every commit and compares it to previous ones to catch regressions and improvements. See more: radar.lean-lang.org/about #LeanLang #LeanProver

081

Lean Focused Research Organization @lean-lang.org · 26/02/2026

The first-ever Lean in Munich meetup happened this week! 🎥 Watch Sebastian Ullrich's full talk on Lean's foundations, software verification, and AI: youtube.com/watch?v=2Dr2149l_9Y #leanlang #leanprover #formalverification #mathematics

084

Lean Focused Research Organization @lean-lang.org · 23/02/2026

Mathematician @davidbessis.bsky.social once waited 7 years for a paper to get accepted. Not because it was wrong, but because it was too complex to verify. In a recent conversation Bessis explained to @curtjaimungal.skystack.xyz how Lean could change that: Watch: www.youtube.com/watch?v=GHGi...

1121

Lean Focused Research Organization @lean-lang.org · 22/02/2026

CSLib just launched — an open-source effort to formalize computer science in Lean, inspired by Mathlib. CS researchers, practitioners & enthusiasts are invited to get involved! Learn more at: 🌐 cslib.io 🤝 Contribute: github.com/leanprover/c... #LeanLang #LeanProver #CSLib #FormalVerification

1207

Lean Focused Research Organization @lean-lang.org · 19/02/2026

Lean 4.28.0 is out! New symbolic simulation framework for 𝚐𝚛𝚒𝚗𝚍, user-defined 𝚐𝚛𝚒𝚗𝚍 attributes for custom tactics, a new 𝚜𝚘𝚕𝚟𝚎𝚛𝙼𝚘𝚍𝚎 in 𝚋𝚟_𝚍𝚎𝚌𝚒𝚍𝚎 for proof vs. counterexample search, and lean4checker available out of the box. lean-lang.org/doc/referenc... #LeanLang #LeanProver #ProofAssistant

0103

Lean Focused Research Organization @lean-lang.org · 12/02/2026

The next bi-monthly #Mathlib community meeting is tomorrow Friday, 13th at 3pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with other contributors! ➡️ See all upcoming community events on our website: lean-lang.org/community/#e...

021

Lean Focused Research Organization @lean-lang.org · 11/02/2026

Terence Tao on how math is changing, #formalverification as the enabler of scaled human-AI collaboration: "The reason why scaling and AI and broad participation actually is a net win is because we have formal verification." 📺 www.youtube.com/watch?v=SuTx... #leanlang #leanprover

0134

Lean Focused Research Organization @lean-lang.org · 10/02/2026

The next Lean FRO office hours are Feb. 11 at 4pm UTC. Bring your questions, share your projects, or just come to learn from others in the community! See our full calendar here: lean-lang.org/community/#e... #LeanLang #LeanProver

062

Lean Focused Research Organization @lean-lang.org · 23/10/2025

𝐋𝐞𝐚𝐧 𝟒.𝟐𝟒.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release improves the module system, strengthens the 𝚐𝚛𝚒𝚗𝚍 tactic, and advances the standard library. Key improvements: 3.5x faster auto-completion, streamlined "try this" suggestions, new 𝚐𝚛𝚒𝚗𝚍 AC solver, enhanced 𝚖𝚟𝚌𝚐𝚎𝚗 syntax. Read more: lean-lang.org/doc/referenc...

0111

Lean Focused Research Organization @lean-lang.org · 23/10/2025

Tactic tip: Lean's 𝚜𝚒𝚖𝚙? is an optimization tool that shows the minimal 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call needed to close a goal. Use the 𝚜𝚒𝚖𝚙? "Try this" suggestion to insert the precise 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call into your proof. Learn more: lean-lang.org/theorem_prov... #LeanLang #LeanProver #ProofAssistant

042

Lean Focused Research Organization @lean-lang.org · 21/10/2025

"Theorem Proving in Lean 4" is the essential guide for anyone using Lean for mathematical proofs. Kept up-to-date with each new Lean release, it covers everything from basic tactics to advanced proof strategies. Read the book here: lean-lang.org/theorem_prov... #LeanLang #LeanProver #Mathematics

0193

Lean Focused Research Organization @lean-lang.org · 17/10/2025

Reservoir is #LeanLang's package registry, inspired by crates.io (thanks @rustfoundation.org!) Browse community-created packages and discover new tools: reservoir.lean-lang.org Sharing is easy! GitHub repos meeting the inclusion criteria are auto-indexed: reservoir.lean-lang.org/inclusion-cr...

0103

Lean Focused Research Organization @lean-lang.org · 10/10/2025

💡Did you know you can run #LeanLang in your browser without installing anything? The Lean Playground provides a full environment for experimentation, learning, and for sharing code snippets with others. Try it out! live.lean-lang.org

192

Lean Focused Research Organization @lean-lang.org · 06/10/2025

Did you know the Info View in #LeanLang's #VSCode extension updates in real-time as you write proofs? Click on any part of your code to see the current proof state, goals, and hypotheses at that exact point. Learn more about the Lean VS Code extension: github.com/leanprover/v...

071

Lean Focused Research Organization @lean-lang.org · 24/09/2025

We really loved this series of tutorials on #metaprogramming in #LeanLang by Heather Macbeth. It's a great intro to a complex topic for novice users of #LeanProver! Pt 1: youtube.com/watch?v=cKvg... Pt 2: youtube.com/watch?v=5er4... Pt 3: youtube.com/watch?v=TJ8T...

1143

Lean Focused Research Organization @lean-lang.org · 18/09/2025

ICYMI: A great summary on the #LeanLang Community Blog of the @simonsfoundation.org 2025 MPS (Math and Phys Sciences) Workshop on #LeanProver. The post includes links to lecture slides, videos, and a list of proposed projects and participants! leanprover-community.github.io/blog/posts/s...

050

Lean Focused Research Organization @lean-lang.org · 16/09/2025

🎉 Lean 4.23.0 is here! Includes many usability improvements, including: 🎯 Enhanced 'Go to Definition' supporting type class instances 🔧 Interactive error hints for faster debugging Release notes: lean-lang.org/doc/referenc... #LeanLang #LeanProver #OpenSource #Mathematics #FormalVerification

0205

Lean Focused Research Organization @lean-lang.org · 05/09/2025

If you're you curious about #LeanLang and want to understand the connection between #programming and #proofs, check out this great new video by Ank Yog. The analogy between Chess and true propositions is particularly compelling! www.youtube.com/watch?v=QXQN...

0177

Lean Focused Research Organization @lean-lang.org · 15/08/2025

🎉 Lean 4.22.0 is here! It represents the culmination of our Year 2 roadmap! Including: 🧠 New grind tactic (SMT-style automated reasoning) 🏗️ New compiler (major performance foundation) Read the release notes: lean-lang.org/doc/reference/latest/releases/v4.22.0/ #LeanLang #LeanProver

1247

Lean Focused Research Organization @lean-lang.org · 07/07/2025

📣 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

22810

Lean Focused Research Organization @lean-lang.org · 30/06/2025

Really enjoyed this talk by @harrisongoldste.in that demonstrates inventive uses of the #LeanLang InfoView enhanced by metaprogramming techniques to display real-time testing data. #LeanProver #Metaprogramming #VSCode #PropertyTesting

1165

Lean Focused Research Organization @lean-lang.org · 30/06/2025

📣 #LeanLang v4.21 is released! This release brings 295 changes, including feature additions, bug fixes, refactors, documentation improvements and performance improvements, in support of our Y2 roadmap: lean-fro.org/about/roadma... ➡️ See the full changelog here: lean-lang.org/doc/reference/

173

Lean Focused Research Organization @lean-lang.org · 23/06/2025

In this 10-minute UCLA Connect talk, Terence Tao provides an accessible and compelling argument for "citizen math" and broad collaboration in research #mathematics via #formalverification using proof assistants like #LeanLang. 🎥 www.youtube.com/watch?v=K376...

0105

Lean Focused Research Organization @lean-lang.org · 18/06/2025

📣 This week, #LeanLang Chief Architect Leonardo de Moura will deliver a keynote in Seoul at #PLDI2025 titled "Lean: Machine-Checked Mathematics and Verified Programming, Past and Future." #pldi #formalmethods #programminglanguages #leanprover

130

Lean Focused Research Organization @lean-lang.org · 16/06/2025

🎉 #LeanLang 0.1 was released 11 years ago today! Lean had been in development since July 15, 2013, but Lean 0.1 was a major milestone. The screencap is a @waybackmachine.bsky.social 06/26/2014 snapshot from the @lean-lang.org GitHub, "Updated 10 days ago"! #LeanProver #ProgrammingHistory

190

Lean Focused Research Organization @lean-lang.org · 04/06/2025

📣 #LeanLang v4.20 has been released! This release brings a total of 346 changes, including feature additions, bug fixes, refactors, documentation and performance improvements, which support our Year 2 roadmap: lean-fro.org/about/roadma... #LeanProver #FuncationalProgramming #FormalVerification

2102

Lean Focused Research Organization @lean-lang.org · 03/06/2025

I think it's worth noting that the book reads particularly well in an online format, since all code samples in the book have live hover states that display their docstrings. For example, see the hover state on String.append below.

110

Lean Focused Research Organization @lean-lang.org · 30/05/2025

Lean community members Yaël Dillies and Paul Lezeau explain #LeanLang simprocs, or "custom simplification procedures", and describe three uses cases in the first of a series of new blog posts. ▶️ Read more here: leanprover-community.github.io/blog/posts/s...

030

Lean Focused Research Organization @lean-lang.org · 28/05/2025

We are humbled that the original paper describing #LeanLang: 𝘛𝘩𝘦 𝘓𝘦𝘢𝘯 𝘛𝘩𝘦𝘰𝘳𝘦𝘮 𝘗𝘳𝘰𝘷𝘦𝘳 (𝘚𝘺𝘴𝘵𝘦𝘮 𝘋𝘦𝘴𝘤𝘳𝘪𝘱𝘵𝘪𝘰𝘯) will be awarded the Skolem Award at CADE-30, which recognizes a "CADE paper that has passed the test of time, by being a most influential paper in the field." cadeinc.org/Skolem-Award

180

Lean Focused Research Organization @lean-lang.org · 28/05/2025

🔥 Google DeepMind just open-sourced their "formal conjectures" project in #LeanLang and #Mathlib! They're formalizing math's biggest unsolved mysteries to build richer datasets for AI reasoning. We love that Google continues to support the Lean ecosystem! Check it out: github.com/google-deepm...

0111

Lean Focused Research Organization @lean-lang.org · 16/05/2025

📣 TWO EXCITING NEW LEAN LECTURES! Just released: Two Strachey Lectures from @compscioxford.bsky.social featuring Leo de Moura (Chief Architect, Lean FRO) and Kevin Buzzard (Professor, Imperial College). A thread on these must-see talks 🧵👇 #LeanLang #LeanProver

192

Lean Focused Research Organization @lean-lang.org · 14/05/2025

The Lean FRO team met in Amsterdam last week for our annual retreat to discuss our Year 3 roadmap, including many productive conversations about Lean's future in verification, mathematics & AI for math. Stay tuned for our full updated roadmap coming end of July! #LeanLang #LeanProver #Lean4

061

Lean Focused Research Organization @lean-lang.org · 15/04/2025

🎉 Technical Debt Win: 3,000+ Mathlib papercuts eliminated! Last quarter we reduced porting notes from ~5,000 to 1,750. Most impressive? 95% required minimal effort, showing how Lean improvements are paying off! #LeanProver #LeanLang #Mathlib

181

Lean Focused Research Organization @lean-lang.org · 08/04/2025

Check out these great UX improvements in Lean 4.18! ✅ New gutter decorations for errors/warnings 🔧 "Unsolved goals" markers to guide your proof 🐙 "Goals accomplished!" celebrations ▶️ Try these now in the Lean4 VSCode extension: marketplace.visualstudio.com/items?itemNa... #LeanLang #LeanProver

043

Lean Focused Research Organization @lean-lang.org · 27/03/2025

💡Interested in learning what #LeanLang and #LeanProver is all about? Check out the talk "Verified Collaboration: How Lean is Transforming Mathematics, Programming, and AI" by Lean Chief Architect Leonardo de Moura. ➡️ Watch here: www.youtube.com/watch?v=rmMY...

071

Lean Focused Research Organization @lean-lang.org · 27/03/2025

Excited to share the recent @simonsfoundation.org talk by @leodemoura.bsky.social: It's a great overview of how #LeanLang is paving the way to a more reliable and collaborative future in math, software & AI! Watch here: www.youtube.com/watch?v=rmMY... #LeanProver #FormalVerification #Mathematics

131

Lean Focused Research Organization @lean-lang.org · 19/03/2025

Big congrats to 14-y.o. Daniel whose #Exporecerca project using #LeanLang to formalize Math Olympiad problems netted him an award from the Royal Society for Sciences and Arts in Barcelona! #LeanProver engineer Anne Baanen had a great chat with him about his award-winning project!

081

Lean Focused Research Organization @lean-lang.org · 13/03/2025

👩‍💻Lean users: Lean 4.17 adds inlay hints for automatically-inserted implicit parameters: With autoImplicit enabled you’ll see in-editor visual feedback for parameters that Lean has automatically inferred, improving readability and making code less error-prone! #LeanLang #LeanProver #DeveloperTools

3165