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...
"Mathlib has reached 2 million lines of code as of October 28. Thanks to everyone that contributed to Mathlib during the roughly 8 years of Mathlib's existence!"
leanprover.zulipchat.com/
#leanprover #mathlib
Looking for a lemma in #LeanLang / #Mathlib but don't know its name? Use Loogle! to search:
By pattern: _ * (_ ^ _) finds expressions matching the pattern
By conclusion: |- tsum _ = _ * tsum _ finds specific conclusion shapes
Combine searches with commas for precision!
loogle.lean-lang.org
The next bi-monthly #Mathlib community meeting is tomorrow (Friday Oct 10) at 2pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with contributors.
See all community events on our website:
lean-lang.org/community/?u...
Readings shared October 8, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib
Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa. arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib #Math
Readings shared October 3, 2025. jaalonso.github.io/vestigium/po... #AI #ATP #AlphaProof #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib
Kevin Buzzard and Alex Kontorovich on the future of formal mathematics: A Mathlib initiative interview. ~ Oliver Nash. www.renaissancephilanthropy.org/news-and-ins... #ITP #LeanProver #Mathlib #Math
The Mathlib initiative (Building the digital foundation of mathematics). mathlib-initiative.org #ITP #LeanProver #Mathlib #Math
Lean 4 Formalizes Mason‑Stothers Theorem and Polynomial Corollaries
The Mason‑Stothers theorem and polynomial corollaries have been formally verified in Lean 4 and merged into mathlib; the work was submitted on 27 Aug 2024 and revised on 25 Sep 2025. Read more: getnews.me/lean-4-formalizes-mason-... #lean4 #mathlib
Lean Formalization of Harder‑Narasimhan Theory Enhances Proofs
The Harder‑Narasimhan theory has been fully formalized in the Lean 4 proof assistant, with machine‑checked proofs of the canonical filtration released on 23 Sep 2025. Read more: getnews.me/lean-formalization-of-ha... #hardernarasimhan #lean4 #mathlib
Lean Formalizes Multi‑Graded Proj Construction
On 18 September 2025 a new arXiv paper showed the multi‑graded Proj construction fully formalized in Lean4, demonstrating Mathlib’s ability to verify advanced algebraic‑geometry concepts. Read more: getnews.me/lean-formalizes-multi-gr... #lean4 #mathlib
Readings shared September 17, 2025. jaalonso.github.io/vestigium/po... #AI #Autoformalization #CAS #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Macaulay2 #Math #Mathlib #Physics #Rocq #SMT
Domain specific (Documentation for Mathlib). ~ John Talbot, Richard M. Hill. www.renaissancephilanthropy.org/domain-speci... #ITP #LeanProver #Mathlib
Readings shared September 1, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #Haskell #ITP #LeanProver #Math #Mathlib #RustLang
Growing Mathlib: maintenance of a large scale mathematical library. ~ Anne Baanen et als. arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib
Readings shared July 19, 2025. jaalonso.github.io/vestigium/po... #CoqProver #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Mathlib #Reasoning #Rocq
Lean Finder: Semantic search for Mathlib that understands user intents. ~ Jialin Lu et als. openreview.net/forum?id=5SF... #ITP #LeanProver #Mathlib
Visited the #Lean / #mathlib community this past week on their Zulip server to learn about connections between
- the #TheoremProving software/communities and
- #ComputerAlgebra / exact mathematical computing communities.
Findings (sparse) documented in
github.com/passagemath/...
#MathSky
Nice article from Quanta about current work on FLT. Also check out the efforts by Kevin Buzzard (@xenaproject.bsky.social) and team to formalize a "21st century" version of FLT in #LeanLang and #Mathlib here: imperialcollegelondon.github.io/FLT/
🔥 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...
Readings shared May 10, 2025. jaalonso.github.io/vestigium/po... #ITP #LeanProver #Math #Mathlib #Python
LeanExplore: a new Mathlib search engine that combines semantic search embeddings, AI-generated translations, and PageRank to give optimized search results. www.leanexplore.com #ITP #LeanProver #Mathlib
🎉 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
Readings shared April 2, 2025. jaalonso.github.io/vestigium/po... #FunctionalProgramming #HOL4 #Haskell #ITP #IsabelleHOL #LLMs #LeanProver #Logic #LogicProgramming #Math #Mathlib #Prolog
Basic probability in Mathlib. ~ Rémy Degenne. leanprover-community.github.io/blog/posts/b... #ITP #LeanProver #Mathlib #Math
Readings shared February 5, 2025. jaalonso.github.io/vestigium/po... #ITP #IsabelleHOL #LeanProver #Mathlib #LLMs #Math
A semantic search engine for Mathlib4. ~ Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, Bin Dong. arxiv.org/abs/2403.13310 #ITP #LeanProver #Mathlib
The Matrix Cookbook, using Lean's mathlib. ~ Eric Wieser. github.com/eric-wieser/... #ITP #LeanProver #Lean4 #Mathlib #Math
Readings shared September 21, 2024. jaalonso.github.io/vestigium/po... #ITP #IsabelleHOL #LeanProver #Lean3 #Lean4 #Mathlib #Logic #Math #AI #LLMs #DeepLearning
