A stress test for AI-assisted formal mathematics
- What it is
- A proposed Lean 4 blueprint formalizes norm-variation estimates for interacting processes, with substantial large-language-model assistance.
- Who did it
- Floris van Doorn, Polona Durcik, Joris Roos, Lenka Slavíková, and Christoph Thiele
- What it could mean
- AI helping with textbook exercises is one thing; AI helping formalize a deep modern theorem is another. Replaying this work would test whether machine assistance can scale while its reasoning stays inspectable.
See the check plan
Evidence & validation
From announcement to evidence
Discovery recorded. State of Proof has not yet examined this claim.
Read the original work
A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations ↗See the proposed checks
Pin a repository commit and run its Lean build in a clean toolchain; identify the formal theorem(s) corresponding to the stated norm-variation result; examination dependency closure, absence of axiomatic escapes, and the prose-to-formal statement map; independently assess the remaining real-variable estimate and hypotheses.
No proof docket yet
A docket is the public record of checks and open questions. This paper does not have one yet; the check plan above describes work still to do.
Explore existing proof dockets →
- What it claims
- The blueprint says its Lean 4 formalization, completed largely automatically with frontier large-language-model assistance, supports norm-variation estimates for multiple ergodic averages of commuting transformations, quantitatively strengthening Tao's norm-convergence theorem and answering an Avigad--Rute question.
- Why this could matter
- A stress test for AI-assisted formal mathematics This mathematics measures whether several interacting processes settle down—and how violently they fluctuate along the way. The bigger story is methodological: a deep modern analysis proof was formalized largely with AI, giving us a rare test of reviewable machine mathematics.
- If it holds up
- Methods: it would show AI-assisted formalization can carry a large, current analysis theorem into a proof checker, strengthening the case for faster mathematical work whose logical core remains inspectable.
- If it does not
- A mismatch would expose where the formal theorem, dependencies, or prose diverge—exactly the evidence needed to improve machine-proof workflows before trusting them at scale.
- Impact horizon
- Methods · AI verification · Dynamical systems · Formal proofs
- Version
- v1, submitted 2026-08-27 16:21:38 UTC. The linked repository reported an update on 2026-08-29 during retrieval.
- Why we tracked it
- It is a live, explicitly AI-assisted formalization claim with a stated machine-checkable artifact and a narrow theorem surface suitable for source-to-kernel and source-to-prose scrutiny.
- Highest-risk dependency
- Whether the repository's kernel-checked statements exactly cover the analytic theorem and claimed quantitative strengthening described in the manuscript, rather than a narrower supporting component.
- Available artifacts
- arXiv's author comment links the public Lean 4 repository; the paper also links generated documentation and a dependency graph.
- Current boundary
- Intake record only; examination not started.