Weekly editions
The stream is also published as one edition a week, newest first.
- Oct 15, 202621 itemsOpenAI publishes 719 model-produced math manuscripts, about 42% Lean-formalized
- Sep 24, 202615 itemsPaper ports Iris, a concurrent separation logic framework, to Lean
- Sep 17, 202614 itemsXTX Markets grants $10mn each to Lean FRO and the Mathlib Initiative
- Sep 3, 202613 itemsPalomar, a registry of Lean verified mathematics, opens for submissions
- Aug 27, 202618 itemsLean FRO publishes six-month roadmap for September 2026 to February 2027
- Aug 15, 202611 itemsKim Morrison releases an integer polynomial factorization library for Lean
- Aug 6, 202610 itemsPramaana Labs reports solving all 6 IMO 2026 problems in Lean
- Jul 23, 20269 itemsPatrick Hulin reports a kernel check gap allowing a proof of False
- Jul 16, 20266 itemsLean v4.32.0 makes the new do elaborator the default
- Jul 9, 20268 itemsKim Morrison releases first packages of Hex, a computational algebra library
- Jul 2, 20265 itemsArkLib anchors a growing ecosystem of Lean libraries for verifying SNARKs
- Jun 25, 20269 itemsLean 4.33 gives Float a pure Lean model, making float proofs possible
- Jun 18, 20266 itemsLean 4.31.0 released with new do loops, Lake linting, mvcgen'
- May 28, 20268 itemsThe Mathlib Initiative launches Formal Frontier for open-source AI autoformalization
- May 14, 202610 itemsLean publishes Lean Workbench, an experimental online environment for Lean
- May 7, 202610 itemsSebastian Graf merges experimental mvcgen' tactic into the Lean toolchain
- Apr 30, 202613 itemsLeo de Moura presents scalable software verification in Lean at SViL 2026
- Apr 23, 20265 itemsBeneficial AI Foundation launches Signal Shot to verify Signal in Lean
- Apr 9, 20269 itemsLean releases Nerodia, a work-in-progress library for writing Python modules in Lean
- Apr 2, 202613 itemsLean 4.29.0 released with a new extensible do elaborator
- Mar 19, 20264 itemsMistral AI releases Leanstral, an open-source code agent for Lean 4
- Mar 5, 20264 itemsMath, Inc.'s Gauss completes formal proof of sphere packing in dimensions 8 and 24
- Feb 26, 20263 itemsEmilio Jesús Gallego Arias built a Lean DSL debugger with GPT-Codex 5.3
- Feb 19, 20268 itemsLean v4.29.0-rc1 changes how isDefEq handles transparency on implicit arguments
- Feb 12, 20263 itemsLeo de Moura merges two Lean core elaborator changes
- Feb 5, 20267 itemsLeo de Moura's Lean change stops simp from simplifying instances by default
- Jan 29, 20264 itemsLean publishes leansqlite, SQLite bindings for Lean
- Jan 22, 20266 itemsLeo de Moura presents The State of Lean at Lean Together 2026
- Jan 15, 20266 itemsAxiom's AxiomProver solves all 12 Putnam problems with Lean proofs
- Jan 8, 20264 itemsLean Community holds Lean Together 2026 virtually via Zoom, January 19 to 23