So, just double-checking how #Lean4 and #Mathlib work:
* Lean takes 3GiB of RAM and a minute to open Mathlib
* Lean requires about 10min to build itself in CI, only verifying required theorems
* Verifying all of Mathlib is measured in hours
* Lean's kernel is untrustworthy due to junk theorems
And yet I'm a clown for using #Metamath? At some point we ought to reconsider the type-theory fetish.
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
"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
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.
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
Corbin
Lean
Hacker News
theHigherGeometer
José A. Alonso
Hakan Tanar