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

Workshop on AI and Theorem Provers in Mathematics (AITPM)

Workshop on AI and Theorem Provers in Mathematics

Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL

Formal Verification of Axiom-Free Gödelian Ontological Argument and Trinity Necessity Proof in Isabelle HOL in the Archive of Formal Proofs

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 theorem for functions of several variables, where the series expansion is around an infinitesimal neighborhood. Most of our proofs are in fact new. Our investigations highlight the possibility of using mathlib to do constructive mathematics.

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 approach to establish the inequality $L^2 \ge 4πA$, which states that among all simple closed curves of a given perimeter $L$, the circle uniquely maximizes the enclosed area $A$. The formalization proceeds in two phases. In the first phase, we establish the Fourier-analytic foundations required by Hurwitz's approach: we formalize orthogonality relations for trigonometric functions over $[-π,π]$, Parseval's theorem for classical Fourier series, uniform convergence of Fourier partial sums via the Weierstrass M-test, term-by-term differentiability, and Wirtinger's inequality. In the second phase, we carry out Hurwitz's proof itself: working with simple closed $C^1$ curves given in arc-length parametrization, we reparametrize over $[0,2π]$, establish the shoelace area formula, apply integration by parts, invoke the AM--GM inequality, apply Wirtinger's inequality, and use the arc-length constraint to derive the bound $A \le L^2/(4π)$. We discuss the key formalization challenges encountered, including the interchange of infinite sums and integrals, term-by-term differentiation, and the coordination of different indexing conventions within Mathlib. The complete formalization is available at https://github.com/mirajcs/IsoperimetricInequality

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 Glimm-Jaffe axioms, a variant of the Osterwalder-Schrader axioms. We present a formalization of this result in the Lean 4 interactive theorem prover. The project is intended as a proof of concept that extended arguments in mathematical physics can be translated into machine-checked proofs using existing AI tools. We begin by introducing interactive theorem proving and constructive quantum field theory, then describe our formalization and the design decisions that shaped it. We also explain the methods we used, including coding assistants, and conclude by considering how AI assisted formalization may influence the future of theoretical physics. Our original release assumed three results, Minlos' theorem, the nuclear property of Schwartz space, and Goursat's theorem. In subsequent releases from our group and from contributors from the Lean community, these assumptions have been proven (or avoided), so that the OS/GJ axioms are now proven using only Lean and its library Mathlib.

Aristotle API

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