Lean Focused Research Organization
@lean-lang.org
Supporting the Formal Mathematics revolution
𝐋𝐞𝐚𝐧 𝟒.𝟐𝟒.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! 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...
Key improvements: 3.5x faster auto-completion, streamlined "try this" suggestions, new 𝚐𝚛𝚒𝚗𝚍 AC solver, enhanced 𝚖𝚟𝚌𝚐𝚎𝚗 syntax.
Read more: lean-lang.org/doc/referenc...
October 23, 2025 at 12:01 AM
𝐋𝐞𝐚𝐧 𝟒.𝟐𝟒.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! 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...
Key improvements: 3.5x faster auto-completion, streamlined "try this" suggestions, new 𝚐𝚛𝚒𝚗𝚍 AC solver, enhanced 𝚖𝚟𝚌𝚐𝚎𝚗 syntax.
Read more: lean-lang.org/doc/referenc...
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
Use the 𝚜𝚒𝚖𝚙? "Try this" suggestion to insert the precise 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call into your proof.
Learn more: lean-lang.org/theorem_prov...
#LeanLang #LeanProver #ProofAssistant
October 22, 2025 at 11:06 PM
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
Use the 𝚜𝚒𝚖𝚙? "Try this" suggestion to insert the precise 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call into your proof.
Learn more: lean-lang.org/theorem_prov...
#LeanLang #LeanProver #ProofAssistant
"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
Read the book here: lean-lang.org/theorem_prov...
#LeanLang #LeanProver #Mathematics
October 20, 2025 at 11:34 PM
"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
Read the book here: lean-lang.org/theorem_prov...
#LeanLang #LeanProver #Mathematics
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...
Sharing is easy! GitHub repos meeting the inclusion criteria are auto-indexed: reservoir.lean-lang.org/inclusion-cr...
October 16, 2025 at 11:36 PM
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...
Sharing is easy! GitHub repos meeting the inclusion criteria are auto-indexed: reservoir.lean-lang.org/inclusion-cr...
💡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
Try it out! live.lean-lang.org
October 10, 2025 at 4:17 PM
💡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
Try it out! live.lean-lang.org
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...
Learn more about the Lean VS Code extension: github.com/leanprover/v...
October 6, 2025 at 5:52 PM
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...
Learn more about the Lean VS Code extension: github.com/leanprover/v...
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...
Pt 1: youtube.com/watch?v=cKvg...
Pt 2: youtube.com/watch?v=5er4...
Pt 3: youtube.com/watch?v=TJ8T...
September 24, 2025 at 7:11 PM
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...
Pt 1: youtube.com/watch?v=cKvg...
Pt 2: youtube.com/watch?v=5er4...
Pt 3: youtube.com/watch?v=TJ8T...
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...
The post includes links to lecture slides, videos, and a list of proposed projects and participants!
leanprover-community.github.io/blog/posts/s...
September 18, 2025 at 7:52 PM
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...
The post includes links to lecture slides, videos, and a list of proposed projects and participants!
leanprover-community.github.io/blog/posts/s...
🎉 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
🎯 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
September 16, 2025 at 6:46 PM
🎉 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
🎯 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
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...
www.youtube.com/watch?v=QXQN...
September 5, 2025 at 3:58 PM
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...
www.youtube.com/watch?v=QXQN...
🎉 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
🧠 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
August 15, 2025 at 7:40 PM
🎉 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
🧠 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
📣 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
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
July 7, 2025 at 9:02 PM
📣 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
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
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
#LeanProver #Metaprogramming #VSCode #PropertyTesting
June 30, 2025 at 9:14 PM
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
#LeanProver #Metaprogramming #VSCode #PropertyTesting
📣 #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/
➡️ See the full changelog here: lean-lang.org/doc/reference/
June 30, 2025 at 8:22 PM
📣 #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/
➡️ See the full changelog here: lean-lang.org/doc/reference/
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...
🎥 www.youtube.com/watch?v=K376...
June 23, 2025 at 6:42 PM
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...
🎥 www.youtube.com/watch?v=K376...
Incredibly grateful to @sigplan.bsky.social and @sigplan-pldi.bsky.social for awarding #LeanLang the Programming Languages Software Award 2025 at #PLDI2025!
#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics #SoftwareVerification
#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics #SoftwareVerification
June 20, 2025 at 4:04 AM
Incredibly grateful to @sigplan.bsky.social and @sigplan-pldi.bsky.social for awarding #LeanLang the Programming Languages Software Award 2025 at #PLDI2025!
#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics #SoftwareVerification
#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics #SoftwareVerification
📣 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
#pldi #formalmethods #programminglanguages #leanprover
June 17, 2025 at 11:12 PM
📣 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
#pldi #formalmethods #programminglanguages #leanprover
🎉 #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
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
June 16, 2025 at 8:47 PM
🎉 #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
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
📣 #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
#LeanProver #FuncationalProgramming #FormalVerification
June 4, 2025 at 7:07 PM
📣 #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
#LeanProver #FuncationalProgramming #FormalVerification
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.
June 3, 2025 at 10:11 PM
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.
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...
▶️ Read more here: leanprover-community.github.io/blog/posts/s...
May 29, 2025 at 11:09 PM
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...
▶️ Read more here: leanprover-community.github.io/blog/posts/s...
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
cadeinc.org/Skolem-Award
May 28, 2025 at 9:29 PM
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
cadeinc.org/Skolem-Award
🔥 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...
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...
May 28, 2025 at 7:04 PM
🔥 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...
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...
📣 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
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
May 16, 2025 at 7:10 PM
📣 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
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
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
Stay tuned for our full updated roadmap coming end of July!
#LeanLang #LeanProver #Lean4
May 14, 2025 at 8:55 PM
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
Stay tuned for our full updated roadmap coming end of July!
#LeanLang #LeanProver #Lean4