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: http://lean-lang.org/community/#events
Comparing leanprover-community:master...usernamenotavailablepleasechooseanother:sphericalCoord · leanprover-community/mathlib4
The math library of Lean 4. Contribute to leanprover-community/mathlib4 development by creating an account on GitHub.
"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!"
https://leanprover.zulipchat.com/#narrow/channel/287929-mathlib4/topic/2.20million/near/553410451
#leanprover #mathlib
Public view of Lean | Zulip team chat
Browse the publicly accessible channels in Lean without logging in.
Readings shared October 8, 2025
The readings shared in Bluesky on 8 October 2025 are:
Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Mic
Growing Mathlib: Maintenance of a large scale mathematical library. ~ Anne Baanen, Matthew Robert Ballard, Johan Commelin, Bryan Gin-ge Chen, Michael Rothgang, Damiano Testa.
https://arxiv.org/abs/2508.21593 #ITP #LeanProver #Mathlib #Math
Growing Mathlib: maintenance of a large scale mathematical library
The Lean mathematical library Mathlib is one of the fastest-growing libraries of formalised mathematics. We describe various strategies to manage this growth, while allowing for change and avoiding maintainer overload. This includes dealing with breaking changes via a deprecation system, using code quality analysis tools (linters) to provide direct user feedback about common pitfalls, speeding up compilation times through conscious library (re-)design, dealing with technical debt as well as writing custom tooling to help with the review and triage of new contributions.
Readings shared October 03, 2025
The readings shared in Bluesky on 03 October 2025 are:
Kevin Buzzard and Alex Kontorovich on the future of formal mathematics: A Mathlib initiative interview. ~ Oliver Nash. #ITP #LeanProver #Mathlib
Kevin Buzzard and Alex Kontorovich on the Future of Formal Mathematics: A Mathlib Initiative Interview — Renaissance Philanthropy – A brighter future for all through science, technology, and innovation
Renaissance Philanthropy is launching the Mathlib Initiative to professionalize and scale the world's largest library of computer-verified mathematics. The Mathlib community has created an open-source library containing nearly two million lines of computer-verified mathematics, and is beginning
The Mathlib initiative (Building the digital foundation of mathematics).
https://mathlib-initiative.org/ #ITP #LeanProver #Mathlib #Math
The Mathlib Initiative
The Mathlib Initiative supports the development of mathematical libraries in the Lean theorem prover.
Yapay zeka, büyük veri setlerini analiz etmekten karmaşık simülasyonlar oluşturmaya kadar, hesaplamalı matematiğin ağır işlerini üstlenerek büyük bir güç haline geldi. Şu an itibarıyla, YZ genellikle kendisine verilen ispatları adım adım doğrulayabiliyor; ancak nihai kararı ve en yaratıcı kanıt yöntemlerinin keşfini hâlâ insan zekasına bırakıyor.
Peki ya bu denge değişirse?
#YapayZeka #Matematik #AlphaProof #Lean #mathlib #DeepMind #YaşamOyunu https://youtu.be/ZERkY5kExjIhttps://monologblg.com/matematik-sadece-insana-mi-ait/Readings shared September 17, 2025
The readings shared in Bluesky on 17 September 2025 are:
Formalizing dimensional analysis using the Lean theorem prover. ~ Maxwell P. Bobbin, Colin Jones, John Velkey, Tyler R. Josephson. #ITP #LeanP
Lean
Hacker News
theHigherGeometer
José A. Alonso
Hakan Tanar