Tag
A guest post by leading formalization researchers (Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, Adam Topaz) reflecting on AI's rapid theorem-proving advances, cautioning against rushed large-scale formalization efforts like Math, Inc.'s sphere-packing project and Anthropic's Fermat's Last Theorem verification, and outlining a positive vision for high-quality, community-driven formalization of mathematics.
Thomas Hales writes a guest post for Terence Tao's blog explaining what mathematicians should know about the Lean theorem prover, covering formal proof reliability, the growth of the mathlib library, and how AI-driven autoformalization has become a practical reality in 2026.
A tutorial-style walkthrough for software engineers that formalizes a constructive proof about regular languages in the Lean theorem prover, explaining specification, implementation, induction, and the anatomy of a formal proof step by step. The piece demonstrates how Mathlib's existing theorems make formalizing textbook automata theory accessible to developers.
This paper introduces AViD Journal, a pipeline for automated novelty verification of mathematical theorems using Lean 4, evaluating it on withdrawn arXiv papers and highlighting challenges in formal verification.
PriorProof introduces a method to measure the novelty of proof techniques in formal mathematics by analyzing the dependency footprint of Lean proof terms against a prior built from an earlier snapshot of Mathlib. The method agrees with human raters on 69.7% of pairs and provides interpretable score gaps.
This paper demonstrates that the axiom of choice has a measurable geometric correlate in proof space, using Lean 4's kernel-level tracking to show a one-parameter mixture law and operational consequences for neural theorem provers.
Terence Tao demonstrates how to use Claude Code as a red teaming tool to align Lean code style with Mathlib's official style guide, using the Riemann–Stieltjes integral formalization project as an example. The demonstration showcases the practical value of AI in code auditing and style alignment.