Embracing AI and formalization: Experimenting with tomorrow’s mathematical tools. ~ Jarod Alper. pubs.ams.org/BULL/0000-00... #AI4Math #LeanProver #ITP #Math

Formally verifying digital circuits with category theory in Lean. ~ Matt Hunzinger. matt.hunzinger.me/2026/03/28/c... #LeanProver #ITP #CategoryTheory

Videos of talks at Swiss Mathematical Society Spring Meeting "Formalization and Proof Assistants" at UniDistance Suisse, 27/03/2026. tube.switch.ch/collections/... #LeanProver

Autoformalization: A year of progress. ~ Auguste Poiroux. tube.switch.ch/videos/NVLp5... #AI4Math #LeanProver

A Lean formalisation of sphere packing in dimension 8. ~ Siddharth Hariharan. tube.switch.ch/videos/NHXRC... #LeanProver #ITP #Math

Formalizing the sphere packing problem. ~ Maryna Viazovska. tube.switch.ch/videos/ggmRt... #LeanProver #ITP #Math

Lean: Collaboration using formalization. ~ Floris van Doorn. tube.switch.ch/videos/AftiL... #LeanProver #ITP #Math

As AI keeps improving, mathematicians struggle to foretell their own future First Proof is an effort to see whether LLMs can contribute meaningfully to pure mathematics research. The dust has settled on round one, and the results are surprising

As AI keeps improving, mathematicians struggle to foretell their own future. ~ Joseph Howlett. www.scientificamerican.com/article/as-a... #AI4Math #LeanProver

What happens when AI starts checking mathematicians’ work A start-up has surprised the scientific community with a breakthrough: translating a modern proof into a programming language for verification using AI. But not everyone is celebrating

What happens when AI starts checking mathematicians’ work. ~ Manon Bischoff. www.scientificamerican.com/article/what... #AI4Math #LeanProver

Shaping the future of mathematics in the age of AI. ~ Johan Commelin, Mateja Jamnik, Rodrigo Ochigame, Lenny Taelman, Akshay Venkatesh. www.math.ias.edu/~akshay/mnot... #AI4Math #LeanProver #ITP

Executable Gödel encodings: A verified runtime for logical syntax. ~ Adrian Diamond. aadsystems.com/papers/godel... #LeanProver #ITP #Logic #Math

On the paucity of lattice triangles A rational triangle $T$ (one whose angles are rational multiples of $π$) unfolds to a translation surface $(X_T,ω_T)$. The lattice triangle problem asks to classify those $T$ for which $(X_T,ω_T)$ is ...

On the paucity of lattice triangles. ~ David Kurniadi Angdinata, Evan Chen, Ken Ono, Jiaxin Zhang, Jujian Zhang. arxiv.org/abs/2603.239... #LeanProver #ITP #Math

Readings shared March 24, 2026 The readings shared in Bluesky on 24 March 2026 are: Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. #LeanProver #ITP #Math The spectral comb and the Riemann hypothesi

Readings shared March 24, 2026. jaalonso.github.io/vestigium/po... #AI4Math #Autoformalization #FunctionalProgramming #Haskell #ITP #IsabelleHOL #LeanProver #Math

Verso: a platform for writing documents, books, course materials, and websites with Lean. verso.lean-lang.org #LeanProver

OpenGauss: an open source, state of the art autoformalization harness — Math, Inc. OpenGauss is a state-of-the-art open-source autoformalization harness for Lean, built for practical proof engineering workflows.

OpenGauss: an open source, state of the art autoformalization harness. www.math.inc/opengauss #AI4Math #LeanProver #ITP #Autoformalization

Code Proven to Work - The Math Way This post is aimed at a general programmer and no prior knowledge of math or CS is assumed. I got nerd-sniped to write this after reading Simon’s excellent post Code proven to work. As someone who wor...

Rado's radical reflections. ~ Rado Kirov. rkirov.github.io/posts/code-p... #LeanProver #ITP #FunctionalProgramming

Semi-Autonomous Formalization of the Vlasov-Maxwell-Landau Equilibrium We present a complete Lean 4 formalization of the equilibrium characterization in the Vlasov-Maxwell-Landau (VML) system, which describes the motion of charged plasma. The project demonstrates the ful...

Semi-autonomous formalization of the Vlasov-Maxwell-Landau equilibrium. ~ Vasily Ilin. arxiv.org/abs/2603.159... #LeanProver #ITP

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case We present a formal verification of the classical isoperimetric inequality in the plane using the Lean 4 proof assistant and its mathematical library Mathlib. We follow Adolf Hurwitz's analytic approa...

Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. arxiv.org/abs/2603.146... #LeanProver #ITP #Math

The spectral comb and the Riemann hypothesis: A proof via fixed-point theory. ~ Engin Atik. kleis.io/docs/papers/... #LeanProver #ITP #Math

Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. hal.science/hal-05555752... #LeanProver #ITP #Math

Prismriver Formalization of music in Lean 4

Introducing codeberg.org/aniva/Prismr..., a #leanprover formalization of #musictheory and #music DSL with flexible support for xenharmonic systems and algorithmic composition. #lean4

Readings shared March 19, 2026 The readings shared in Bluesky on 19 March 2026 are: Aristotle: The World's most advanced formal reasoning agent. #LeanProver #ITP #Math Formalization of QFT (quantum field theory). ~ Michael R. Doug

Readings shared March 19, 2026. jaalonso.github.io/vestigium/po... #ATP #ITP #IsabelleHOL #LLMs #LeanProver #Logic #Math #Physics #Prover9

Synthetic Differential Geometry in Lean This article is about the formalization of synthetic differential geometry with the Lean proof assistant and the mathematical library mathlib. The main result we prove and formalize is a Taylor theore...

Synthetic differential geometry in Lean. ~ Riccardo Brasca, Gabriella Clemente. arxiv.org/abs/2603.17457 #LeanProver #ITP #Math

Formalizing the Classical Isoperimetric Inequality in the Two-Dimensional Case We present a formal verification of the classical isoperimetric inequality in the plane using the Lean 4 proof assistant and its mathematical library Mathlib. We follow Adolf Hurwitz's analytic approa...

Formalizing the classical isoperimetric inequality in the two-dimensional case. ~ Miraj Samarakkody. arxiv.org/abs/2603.146... #LeanProver #ITP #Math

Formalization of QFT A foundational result in constructive quantum field theory is the construction of the free bosonic quantum field theory in four-dimensional Euclidean spacetime and the proof that it satisfies the Glim...

Formalization of QFT (quantum field theory). ~ Michael R. Douglas, Sarah Hoback, Anna Mei, Ron Nissim. arxiv.org/abs/2603.157... #LeanProver #ITP #Physics

Aristotle: The World's most advanced formal reasoning agent. aristotle.harmonic.fun #LeanProver #ITP #Math

Announcing our fully open-source code agent to support writing proofs and code in @lean-lang.org. This has been a labor of love by our team at Mistral AI, and we look forward to seeing what the #LeanProver community does with it!

Readings shared March 14, 2026 The readings shared in Bluesky on 14 March 2026 are: From SMT solvers to Lean and the future of automated reasoning. ~ Leo de Moura, Nicola Gigante. #LeanProver #ITP A formalization of Borel determin

Readings shared March 14, 2026. jaalonso.github.io/vestigium/po... #AI #Agda #ITP #LeanProver #Math #Mizar

Optimal Caverna Gameplay via Formal Methods - Stephen Diehl Personal blog of Stephen Diehl - Software engineer writing about technology, programming, and the future

Optimal Caverna gameplay via formal methods. ~ Stephen Diehl. www.stephendiehl.com/posts/caverna/ #LeanProver #ITP

Duality theory in linear optimization and its extensions -- formally verified Farkas established that a system of linear inequalities has a solution if and only if we cannot obtain a contradiction by taking a linear combination of the inequalities. We state and formally prove several Farkas-like theorems over linearly ordered fields in Lean 4. Furthermore, we extend duality theory to the case when some coefficients are allowed to take "infinite values".

Duality theory in linear optimization and its extensions - formally verified. ~ Martin Dvorak, Vladimir Kolmogorov. afm.episciences.org/17678 #LeanProver #ITP #Math