Lean is a dependently-typed programming language and theorem prover.
Seattle
- Tweets 781
- Following 49
- Followers 11,224
- Likes 699
Nice, Terence Tao (Fields Medal 2006) found a bug in one of his papers using Lean 4. mathstodon.xyz/@tao/11128774…
14
306
1,825
349,428
🔥 @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 for benchmarks and growing the Lean ecosystem.
The project was open sourced today! And you can be part of it! Check it out: github.com/google-deepmind/f…
#LeanProver #FormalMath #AIResearch #GoogleDeepMind
14
185
896
100,217
📣 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
14
97
492
44,192
Terry Tao's blog post on the PFR project is essential reading for anybody interested in formal mathematics with Lean. terrytao.wordpress.com/2023/…
2
84
438
102,912
🎉 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 future performance improvements
Release notes are here: lean-lang.org/doc/reference/…
#LeanLang #LeanProver #FormalMethods #AutomatedReasoning
2
67
311
21,328
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. 👇
3
74
387
24,333
DeepMind has formalized a theoretical result related to AI safety in Lean. 😍
Paper: arxiv.org/abs/2311.14125.
Code: github.com/google-deepmind/d…
4
70
391
91,248
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. mathstodon.xyz/@tao/11124771…
2
50
318
68,905
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.
2
47
176
76,477
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 #FormalMathematics
Today 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.
3
27
232
19,433
"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 everything from basic tactics to advanced proof strategies, with hands-on examples throughout.
Read the full book here: lean-lang.org/theorem_provin…
#LeanLang #LeanProver #FormalMathematics
6
39
249
16,867
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 announcement: renaissancephilanthropy.org/…
3
30
248
13,858
We're excited to see #LeanLang featured in the new @Stanford course CS 99: 𝘍𝘶𝘯𝘤𝘵𝘪𝘰𝘯𝘢𝘭 𝘗𝘳𝘰𝘨𝘳𝘢𝘮𝘮𝘪𝘯𝘨 𝘢𝘯𝘥 𝘛𝘩𝘦𝘰𝘳𝘦𝘮 𝘗𝘳𝘰𝘷𝘪𝘯𝘨 𝘪𝘯 𝘓𝘦𝘢𝘯 4, led by Leni Aniva, Abdalrhman Mohamed and sponsored by Clark Barrett.
✨ The course hosts a fantastic collection of well-produced slides and #LeanLang problem sets!
See the course here: web.stanford.edu/class/cs99/
#LeanLang #LeanProver #UniversityMath #StandfordMath
1
34
238
13,076
Great @SimonsFdn talk by Kevin Buzzard on math's future; he notes mathematical ideas have grown so complex that traditional writing methods struggle to cope.
He demonstrates how combining LLMs with proof assistants like Lean could eliminate hallucinations—the LLM proposes ideas while Lean verifies correctness.
Watch: piped.video/watch?v=K5w7VS2s…
#leanlang #leanprover #mathematics #ai
5
42
225
14,191
New blog post: "How the Lean Language Brings Math to Coding and Coding to Math"!
amazon.science/blog/how-the-…
1
37
152
16,084
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: piped.video/watch?v=cKvgMjuL…
Pt 2: piped.video/watch?v=5er4yLRd…
Pt 3: piped.video/watch?v=TJ8Tqv6A…
6
45
210
18,197
Mathlib is a community-built library of mathematics, formalized in #LeanLang and containing nearly 1.8MM lines of code and 190K mathematical theorems! Over 500 contributors have helped to drive this project forward at an incredible pace. Learn more at: leanprover-community.github.…
37
193
7,895
We're pleased to announce the first official release of Lean 4!
Release notes: github.com/leanprover/lean4/…
Post on the community blog about future release cycles: leanprover-community.github.…
2
70
188
22,082
"We live in the arguably the most exciting era of mathematics in human history since the time of Euclid."
Yang-Hui He's talk "The rise of the machines" for the Royal Institute, traces three ways #AI is reshaping #mathematics: bottom-up verification through systems like #LeanLang and #Mathlib, top-down discovery of new conjectures, and language models now solving research-level problems.
Watch the full lecture: piped.video/watch?v=oOYcPkBa…
3
41
197
15,857
Terence Tao’s recent lecture on AI - with references to Lean’s contributions - went live today! Check it out:
piped.video/watch?v=_sTDSO74…
#leanlang #leanprover
3
45
164
17,208
Great news! XTX Markets has just announced the launch of the Artificial Intelligence Mathematical Olympiad Prize (AI-MO Prize), a $10 million challenge fund. This initiative is designed to accelerate the development of AI models for mathematics. aimoprize.com
5
42
187
50,452
We are humbled that the original paper describing #LeanLang: 𝘛𝘩𝘦 𝘓𝘦𝘢𝘯 𝘛𝘩𝘦𝘰𝘳𝘦𝘮 𝘗𝘳𝘰𝘷𝘦𝘳 (𝘚𝘺𝘴𝘵𝘦𝘮 𝘋𝘦𝘴𝘤𝘳𝘪𝘱𝘵𝘪𝘰𝘯) will be awarded the Skolem Award at CADE-30 in Stuttgart this July!
✨The Skolem award recognizes a "CADE paper that has passed the test of time, by being a most influential paper in the field."✨
cadeinc.org/Skolem-Award
#LeanLang #LeanProver #FormalMathematics #SoftwareVerification
1
18
194
6,573
🎉 Technical debt milestone: Last quarter the team reduced Mathlib porting notes from ~5,000 to 1,750, eliminating thousands of papercuts! An estimate 95% required minimal effort—proof of continuous improvements to Lean!
#LeanProver #LeanLang #Mathlib
1
11
169
5,366
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!
piped.video/watch?v=QXQNet2y…
1
30
174
7,422
🎉 Lean 4.23.0 is here! Major improvements across the board including featuring 610 total changes. Usability specific highlights include:
🎯 Enhanced 'Go to Definition' - now shows specific type class instances involved
🔧 Interactive error hints - clickable suggestions for faster debugging
Release notes: lean-lang.org/doc/reference/…
#LeanLang #LeanProver #OpenSource #Mathematics #FormalVerification
1
23
148
7,727
Fascinating talk by Thomas Hubert on AlphaProof at IMO 2024! Combining Lean's formal verification with DeepMind's RL techniques led to solving one of the hardest problems that stumped most humans.
Watch: piped.video/watch?v=TFBzP78J…
#LeanLang #AlphaProof
42
158
12,908
Paperproof: A new proof interface for Lean 4
"Paperproof will inspect how the hypotheses and goals were changing throughout the Lean 4 proof, and display this history - making it equivalent to how we think of a mathematical proof on paper."
github.com/Paper-Proof/paper…
1
44
156
35,906
Great article in Scientific American about the potential of AI in mathematics.
scientificamerican.com/artic…
It is an interview with Terence Tao. We are happy to see Lean cited multiple times, and the recognition of how tools like Lean can revolutionize mathematical reasoning.
36
146
22,893
Incredibly grateful to @TheOfficialACM SIGPLAN for awarding #LeanLang the Programming Languages Software Award 2025 at #PLDI2025! 🎉
"The Lean theorem prover is a remarkable software artifact... Lean has had and continues to have a broad impact on industrial practice and scientific research."
This belongs to our amazing community - mathematicians building Mathlib (1.8M+ lines!), engineers at AWS/Microsoft/beyond doing critical verification work, and researchers pushing formal methods forward.
The citation says "formal methods based on Lean will play a central role in mathematics in the years to come" - that future is being built by the entire Lean community.
Thank you to everyone making formal mathematics and software verification more accessible! 🙏
#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics
5
41
155
12,526
Thrilled to hear about the "Harmonic Analysis with Lean Formalization" (HALF) project: 6 years of research-level formalization in #LeanLang, led by Dr. Christoph Thiele and Dr. Floris van Doorn at University of Bonn with a €6.4M ERC Synergy Grant.
Dr. van Doorn: "As the first project of its kind, HALF will mark a milestone on the path to the routine use of computer verification in mathematical research."
Read the press release: uni-bonn.de/en/news/194-2025
Read more about the Lean Roadmap: lean-lang.org/fro/roadmap/y3
#LeanProver #FormalMathematics #UniversityOfBonn #HausdorffCenter
20
148
9,977
Check out the new use cases on lean-lang.org showing real-world #LeanLang applications!
📚 Mathlib: Nearly 2M lines of formalized math spanning algebra, analysis, topology & more
🦀 Aeneas: Rust → Lean verification toolchain for functional correctness in #Rust beyond type safety
🔢 Fermat's Last Theorem: @XenaProject's Kevin Buzzard formalizing one of #math's most famous proofs
More use cases coming as the ecosystem grows!
👉 lean-lang.org/use-cases
1
19
146
7,597
It's exciting to see new autoformalization advancements featuring #LeanLang, in this case via @morph_labs newly announced Trinity system. More tools like this means creating more opportunities for the community to continue to build verified knowledge together!
#LeanProver #Mathematics #FormalVerification
1
23
124
7,793
The Lean FRO is happy to welcome Sofia Rodrigues and Henrik Böving as our newest part-time team members! Sofia has previously developed an entire ecosystem of Lean packages for a backend challenge. Henrik is the creator of doc-gen4 among other contributions to Lean's ecosystem.
1
11
136
15,667
The new Lean website is is live! lean-lang.org
Our team will continue to add to it in the coming weeks and months. 🎉
1
29
125
12,400
🆕 Lean 4 version 4.17 improves visual indicators for automatically-inserted implicit parameters!
Inlay hints now now clearly denote which identifiers have been automatically inferred by Lean, making code more readable and easier to debug.
#LeanLang #LeanProver #DeveloperTools
2
22
134
6,891
We were very excited to read Terence Tao's article "Machine-Assisted Proof" in the latest Notices of the American Mathematical Society, and pleased to see Lean recognized several times throughout the piece! #leanprover #leanlang
ams.org/journals/notices/202…
2
25
130
8,950
Check out this excellent video on proving the continuity of various functions using Lean 4. It's a fantastic introduction to Lean, and its tactic framework for proof automation.
piped.video/watch?v=BZjAghqK…
28
128
10,490
Lean 4.2.0 has been released
github.com/leanprover/lean4/…
1
7
122
12,358
𝐋𝐞𝐚𝐧 𝟒.𝟐𝟒.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings continued improvements to the module system and verification framework, strengthens the 𝚐𝚛𝚒𝚗𝚍 tactic, and advances the standard library. Notably:
- Auto-completion 3.5x faster
- "Try this" suggestions streamlined in InfoView
- New 𝚐𝚛𝚒𝚗𝚍 AC solver for complex operations
- Enhanced 𝚖𝚟𝚌𝚐𝚎𝚗 verification syntax
Full release notes: lean-lang.org/doc/reference/…
#LeanLang #LeanProver #ProofAssistant #OpenSource
18
130
6,097
📣#LeanLang v4.20 has been released! This release brings a total of 346 changes, including feature additions, bug fixes, refactors, documentation improvements and performance improvements, all of which support our Year 2 roadmap: lean-fro.org/about/roadmap-y…
#LeanProver #FunctionalProgramming #FormalVerificiation
3
19
123
6,809
We are blown away by David Renshaw's latest video on animating Lean proofs!
piped.video/watch?v=KuxFWwwl…
19
91
6,880
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!
12
114
4,604
This is a fantastic conversation well-worth listening to in full. And it was great to listen in on such a clear explanation of how #LeanLang is helping to break the "trust bottleneck" in mathematics!
➡️"1:32:51 - Lean programming language" for the discussion about Lean!
#LeanProver #FormalMethods #Mathematics
Here's my conversation with Terence Tao, one of the greatest mathematicians in history.
We talk about the hardest problems in mathematics & physics, and how AI might help us humans to solve them. This conversation was a huge honor for me. I can't quite put it into words, but once again I'm grateful for whatever simulation code resulted in me having the life I do 🙏
To further confirm simulation, podcast length accidentally turned out to be 3:14 (pi=3.141592). But it's not 3:14:15, because the simulation code has some bugs 🤣
Podcast is here on X in full, and is up everywhere else (see comment).
Timestamps:
0:00 - Introduction
0:49 - First hard problem
6:16 - Navier–Stokes singularity
26:26 - Game of life
33:01 - Infinity
38:07 - Math vs Physics
44:26 - Nature of reality
1:07:09 - Theory of everything
1:13:10 - General relativity
1:16:37 - Solving difficult problems
1:20:01 - AI-assisted theorem proving
1:32:51 - Lean programming language
1:42:51 - DeepMind's AlphaProof
1:47:45 - Human mathematicians vs AI
1:57:37 - AI winning the Fields Medal
2:04:47 - Grigori Perelman
2:17:30 - Twin Prime Conjecture
2:34:04 - Collatz conjecture
2:40:50 - P = NP
2:43:43 - Fields Medal
2:51:18 - Andrew Wiles and Fermat's Last Theorem
2:55:16 - Productivity
2:57:55 - Advice for young people
3:06:17 - The greatest mathematician of all time
13
120
7,605
Lean Together 2024, a free online conference about the Lean theorem prover and programming language, will be held 9-12 January, 2024. More details and registration are available at leanprover-community.github.…
29
114
20,519
Tim Gowers, Ben Green, Freddie Manners and Terence Tao just uploaded the paper arxiv.org/abs/2311.05762 proving the Polynomial Freiman-Ruzsa conjecture. Tao is planning to formalize this paper in Lean 🚀
mathstodon.xyz/@tao/11140447…
19
107
7,086
"Functional Programming in Lean" (or FPIL), the essential core text for learning how to program in #LeanLang, has been ported to Verso!👇
#FormalVerification #SoftwareVerification #Programming #LearnProgramming
2
11
112
5,366
Thorsten Altenkirch delivers an excellent explanation of Gödel's Incompleteness Theorem on @Computerphile, including demonstrations with #LeanLang definitions!
piped.video/watch?v=IuX8QMgy…
6
19
114
8,154
We're proud to share our progress, challenges, and the foundational steps we've taken to ensure Lean's continued success and impact across diverse fields, including mathematics, software verification, and AI.
lean-lang.org/blog/2024-8-13…
1
24
106
6,043
Lean 4.5.0 has been released!
github.com/leanprover/lean4/…
12
105
6,094
📣 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
4
16
107
5,607
We have just launched the new Lean reference manual, our core documentation intended as a comprehensive, precise description of Lean! #leanlang #leanprover
Check out the manual: lean-lang.org/doc/reference/…
Read more about the release: lean-lang.org/blog/2024-12-1…
26
107
5,790
We're excited to share the Lean FRO Year 3 Roadmap today! This roadmap builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026. Read the full document at lean-lang.org/fro/ for details on our seven key priority areas.
#LeanProver #FormalMathematics #FormalVerification
3
25
107
7,542
David Christiansen and Leo de Moura will be teaching Lean at the SSFT24 summer school next week!
📺 Lectures and labs will be live-streamed and recorded.
🖥️ Registration for virtual participation is still open: fm.csl.sri.com/SSFT24/
1
12
49
7,663
The first volume of the new Open Access journal "Annals of Formalized Mathematics" was released today!
➡️afm.episciences.org/volume/v…
#FormalMath #Mathematics #OpenAccess
1
24
107
5,273
The Lean FRO team gathered in Amsterdam last week to discuss our Year 3 roadmap! Exciting developments for verification, mathematics & AI coming soon. Full roadmap publication end of July! #LeanLang #LeanProver #Lean4 #FormalVerification #Mathematics
6
101
3,673
🎂#LeanLang 0.1 was released 11 years ago today!
While it's true that Lean had been in development for almost a year prior (earliest commit July 15, 2013!) the release of Lean 0.1 was a major milestone.
The screenshot below is from a June 26th, 2014 snapshot of the @leanprover GitHub, courtesy of @waybackmachine. Note the "Updated 10 days ago" tag on the lean0.1 repository.
#LeanProver #ProgrammingHistory
2
11
102
5,318
With Lean 4.18 we've improved Lean's visual clarity in VS Code!
✅ New gutter decorations for errors/warnings;
🔧 "Unsolved goals" markers to guide your proof;
🐙 "Goals accomplished!" celebrations!
▶️ Try these out now: marketplace.visualstudio.com…
#LeanProver #LeanLang
2
18
98
5,485
Rust's Creator Graydon Hoare Recommends Lean 4 for Those Seeking Advanced Types—Honored by the Mention. 🙏 #LeanProver #RustLang types.pl/@graydon/1110338074…
1
16
102
8,577
Lean 4.3.0 has been released
github.com/leanprover/lean4/…
10
95
6,452
🚀 Big news in the world of formal mathematics! Since the Mathlib port to Lean 4 on July 21, 2023, its size has expanded from 1.25 million lines of code (LoC) to 1.4 million LoC. 📈 Even more impressive, the instruction count for building Mathlib has plummeted by a whopping 40%!
1
13
93
7,477
Mario Carneiro just announced the release of lean4lean, a lean 4 kernel implementation written entirely in lean 4. We are so excited.
github.com/digama0/lean4lean
2
16
91
8,872
New use case: AWS's Cedar authorization policy language verified with Lean.
Emina Torlak and Kesha Hietala use "verification-guided development": creating formal models in Lean alongside production Rust code. The Lean models are 10x smaller, serving as both verification targets and clear documentation.
Their approach combines mathematical proofs with differential testing on millions of inputs. AWS has fully integrated this verification process into Cedar's development workflow.
➡️Read more: lean-lang.org/use-cases/ceda…
#LeanLang #LeanProver #Cedar #FormalVerification #AWS
3
21
98
5,847
The Lean 4 Language Reference is a comprehensive, precise description of #LeanLang: a reference work in containing detailed information on everything from basic types to specific use-cases of autoformalization tactics, such as 𝚐𝚛𝚒𝚗𝚍.
Read here: lean-lang.org/doc/reference/…
1
12
95
4,637
🌟 We're Hiring at the Lean FRO! 🌟 Interested in Lean, functional programming languages, and theorem provers? We have open positions that might be just right for you.
For more details and to apply, please visit: lean-fro.org/jobs/
1
25
68
10,332
We're thrilled to share that the roadmap for Lean FRO is now public!
lean-fro.org/about/roadmap/
🚀 Join us in shaping the future of Lean!
#LeanFRO #LeanLang #LeanProver
1
23
91
11,517
At AWS, Cedar is a language for defining permissions as policies, which describe who should have access to what. Words can't capture how excited we are to see the formalization of the Cedar policy language in Lean!
github.com/cedar-policy/ceda…
cedarpolicy.com/en
13
93
7,716
It's great to see more open source projects like clean enter the Lean ecosystem. Great news for folks working with ZK circuits!
#LeanLang #LeanProver #ZKProofs
Introducing 𝐜𝐥𝐞𝐚𝐧
We've been quietly working on a framework to write formally verified circuits, directly in Lean4
Blog post & video: blog.zksecurity.xyz/posts/cl…
Here's what it looks like 👀
8
87
5,141
Looking for a particular lemma or definition in Lean or Mathlib, but don't know its name? Use Loogle! to search:
By pattern: _ * (_ ^ _) finds lemmas with expressions matching the pattern—in this case a product where the second element is raised to a power
By conclusion: |- tsum _ = _ * tsum _ finds lemmas with specific conclusion shape—in this case an equivalence between summations of a particular shape
Combine multiple searches with commas for added precision!
Try Loogle! here: loogle.lean-lang.org/
#LeanLang #LeanProver #Mathematics
3
12
90
4,211
Really enjoyed this talk by Harry Goldstein that demonstrates inventive uses of the #LeanLang InfoView enhanced by metaprogramming techniques to display real-time testing data.
#LeanProver #Metaprogramming #VSCode #PropertyTesting
2
11
84
4,740
Lean 4.11.0 has been released.
lean-lang.org/blog/2024-9-1-…
16
84
6,243
Congratulations to @leodemoura and to the entire Lean community on Lean’s 10th Birthday! Lean 0.1 was released on June 16, 2014 🐙
#leanlang #leanprover
1
9
82
5,510
This talk by @yannfleureau is a great introduction to Project Numina and their open-source dataset of mathematics problems and solutions. We look forward to the results from IMO 2025!
➡️ Watch the video here: piped.video/watch?v=mSbf7IoI…
#AI #Mathematics #OpenSource #FormalMath #LeanLang
18
86
6,064
$18M in new funding to push the boundaries of math and AI! Grantees of the AI for Math Fund will advance mathematical discovery and research. Excited that 14 of the research proposals feature #LeanLang!
Today @xtxmarkets and @RenPhil21 announce 29 grantees and $18M to accelerate the discovery of AI tools for mathematics — one of the largest philanthropic investments in AI+math to date.
Learn more and explore the projects: renaissancephilanthropy.org/…
#AIforMath
11
82
5,829
We're really excited to hear about #LeanLang's importance to AlphaProof in this great conversation about AI and reinforcement learning between Hannah Fry and David Silver!
#LeanProver #AI #ReinforcementLearning
Human generated data has fueled incredible AI progress, but what comes next? 📈
On the latest episode of our podcast, @FryRsquared and David Silver, VP of Reinforcement Learning, talk about how we could move from the era of relying on human data to one where AI could learn for itself.
Watch now →
00:00 Introduction
01:50 Era of experience
03:45 AlphaZero
10:19 Move 37
15:20 Reinforcement learning and human feedback
24:30 AlphaProof
29:50 Math Olympiads
35:00 Experience based methods
42:56 Hannah's reflections
44:00 Fan Hui joins
12
82
4,028
We're happy to announce live.lean-lang.org/, the official online playground for Lean 4 + std/mathlib hosted by the Lean FRO and based on github.com/leanprover-commun… by Alexander Bentkamp and Jon Eugster. Many thanks to Alex for helping with the setup!
1
19
82
21,889
If you missed Lean Together 2025 check out the new leanprover community YouTube playlist, including all recorded sessions, and showcasing the latest in Lean and Mathlib! Thanks to the Mathlib community for hosting a fantastic event!
piped.video/watch?v=ZPPDktjL…
19
83
7,247
Great news for the #LeanLang verification community!
"Lean-SMT... is a significant step toward
building a Lean hammer that enhances automation... The ultimate objective is to develop a Lean hammer
that brings unprecedented automation and verification capabilities to Lean."
Lean-SMT: An SMT tactic for discharging proof goals in Lean. ~ Abdalrhman Mohamed, Tomaz Mascarenhas, Harun Khan, Haniel Barbosa, Andrew Reynolds, Yicheng Qian, Cesare Tinelli, Clark Barrett. arxiv.org/abs/2505.15796 #ITP #LeanProver
1
13
78
7,153
Did you know the InfoView 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/vscode…
3
10
81
3,764
At the Lean FRO we're excited that #LeanLang is at the forefront of "how AI will transform mathematics", now and into the future.
➡️ Read more about the Equational Theories project here: teorth.github.io/equational_…
#LeanProver #Mathematics #AI
In fall of 2024, Terence Tao launched the equational theories project, which drew together more than 50 participants, many of them amateur mathematicians, to assess and explore 22 million mathematical relationships.
quantamagazine.org/mathemati…
12
76
5,311
We're thrilled that the Mathlib Initiative is getting off the ground!
The Mathlib Initiative is live!
After years of volunteer-driven progress in formal math, we're scaling up with professional infrastructure, building the future of math with rigor and scale.
mathlib-initiative.org 👇
13
79
5,898
The Lean FRO welcomes its newest employee, @d_christiansen! David is the author of Functional Programming in Lean and co-author of The Little Typer. He's worked on Idris 1, on software verification tools at Galois, and as the Haskell Foundation's Executive Director.
1
4
74
4,413
📢This is an incredible result! We're very excited to see how this evolves!
#leanlang #leanprover
🚀 Introducing Goedel-Prover: A 7B LLM achieving SOTA open-source performance in automated theorem proving! 🔥
✅ Improving +7% over previous open source SOTA on miniF2F
🏆 Ranking 1st on the PutnamBench Leaderboard
🤖 Solving 1.9X total problems compared to prior works on Lean Workbook
[1/n]
website: goedel-lm.github.io
huggingface: huggingface.co/Goedel-LM/Goe…
github: github.com/Goedel-LM/Goedel-…
Amazing collaborators: @sangertang1999 (co-first author) @Lyubh22 @wujiayun12 @hongzhou__lin @KaiyuYang4 @JiaLi52524397 @xiamengzhou @danqi_chen @prfsanjeevarora @chijinML
9
69
4,297
Tactic tip: Lean's 𝚜𝚒𝚖𝚙 tactic simplifies goals using lemmas tagged with [𝚜𝚒𝚖𝚙], but 𝚜𝚒𝚖𝚙? is your optimization tool. It reports an equivalent 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call that would be sufficient to close the goal and speed up processing.
When you use 𝚜𝚒𝚖𝚙?, Lean displays a "Try this" suggestion showing the minimal 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call. Click to replace your 𝚜𝚒𝚖𝚙? with the precise, faster version.
This makes your proofs more explicit and helps you understand which mathematical facts Lean is using.
Learn more: lean-lang.org/theorem_provin…
#LeanLang #LeanProver #ProofAssistant
3
8
72
3,857
After almost three years and 9745 commits, the first milestone release of Lean 4 is here!
github.com/leanprover/lean4/…
18
67
ICYMI: There is a great summary on the Lean Community Blog of the @SimonsFdn 2025 MPS (Mathematics and Physical Sciences) Workshop on Lean, that took place in June.
The post includes links to lecture slides, videos, and a list of proposed projects and participants!
leanprover-community.github.…
#LeanLang #LeanProver #Formalization
1
11
73
5,079
📣 We're pleased to welcome our newest team member, Jason Reed, to Lean FRO this week!
Jason brings valuable experience in proof assistant implementation and web infrastructure development to Lean FRO. In past roles, Jason has contributed to GitHub's CodeQL VS Code plugin, and he created an open source web sandbox for Twelf - a logical framework developed by Frank Pfenning and collaborators at Carnegie Mellon.
Jason will be leading development on the recently announced mathematical workbench project made possible via donation from Alex Gerko, CEO of XTX Markets. We're grateful for this support and excited to collaborate with Jason on advancing formal mathematics tooling.
#LeanLang #LeanProver #FormalMathematics #OpenSource
6
70
3,974
Great @SpringerNature article by @TaliaRinger on first experiences with @GoogleDeepMind's #AlphaProof by mathematicians experienced with #LeanLang, and demonstrating potential for future workflows in research-level mathematics.
Read here: nature.com/articles/d41586-0…
1
13
69
4,834
📣 #LeanLang v4.21 has been released! This release brings a total of 295 changes, including feature additions, bug fixes, refactors, documentation improvements and performance improvements, all of which support our Year 2 roadmap: lean-fro.org/about/roadmap-y…
➡️ See the full changelog here: lean-lang.org/doc/reference/…
9
68
2,864
This is a great introduction to Lean and what it means to write formal mathematics! Big thanks to @dan_abramov2 for writing it!
16
67
9,394
Very exciting new project using Lean :)
Terry Tao and I are pleased to announce the "Prime Number Theorem and Beyond" project, which you can find here:
github.com/AlexKontorovich/P…
with blueprint here:
alexkontorovich.github.io/Pr…
and dedicated stream in the Leanprover Zulip chat.
The initial goal is to get the Prime Number Theorem formalized in Lean (of course it's been done a few times in other systems) via either/both Fourier and/or complex analysis (especially the latter, which can lead to the classical exp-root-log error -- which has *not*, to my knowledge, been formalized before), followed by things like Dirichlet's theorem, Chebotarev density, etc etc.
This kind of project is ideal for distributed efforts. Contributions are welcome from people who know just math but not Lean (who can add to the blueprint), as well as people who know (even some) Lean but not the mathematical content.
There's already a lot of very low-hanging fruit in the dependency graph - if you ever wanted to try to impress Terry Tao, here's your chance! :)
4
62
4,977
Lean community members Yaël Dillies and Paul Lezeau explain #LeanLang simprocs, or "custom simplification procedures", and outline three use cases in the first of a series of new blog posts.
1
6
60
3,585
Recently came across @filiplajszczak's four-part blog series to formalize a classic 1967 mathematics textbook in #LeanLang.
Filip take an accessibility-minded focus: designed for those "with no prior experience with formalization or computer-assisted theorem proving" but with basic math background. A nice bridge for newcomers to #LeanProver!
Read the introductory post here: filip.lajszczak.dev/lean-4-w…
8
62
3,845
🔥 Big news from Morph labs! Introducing Morph Prover v0 7B - the first open-source chat assistant designed for #LeanProver. The Lean FRO and all of us Lean developers are truly thrilled about this fantastic development 🚀
13
59
10,858
Joining the Lean Community Zulip channel (leanprover.zulipchat.com/) is a great way to start, if you're interested in contributing to the Lean ecosystem!
Attended Leo de Moura’s talk about @leanprover at #CADE_30 in Stuttgart/Germany. Lot’s of stuff in the pipeline! And whether it’s #Agda or #lean_lang I want to learn more about dependent types, proofs and how to apply them in my daily work!
The slides: leodemoura.github.io/files/C…
10
59
3,252
Lean 4.14.0 has been released!
lean-lang.org/blog/2024-12-9…
9
60
3,341
📖 Read the blog post: terrytao.wordpress.com/2025/…
💻 See the code: github.com/teorth/analysis
8
63
2,539