AI-produced Lean proof checks convergence result for reaction-network models
A new preprint reports an AI-produced Lean 4 formalization of a convergence theorem for detailed-balanced mass-action systems.
A machine-checked route through a reaction-network theorem
A preprint submitted on October 22 reports a Lean 4 formalization of a convergence result for detailed-balanced mass-action systems, mathematical models used to describe chemical reaction networks. The stated theorem says that every positive stoichiometric compatibility class has one positive equilibrium and that every positive trajectory converges to it. The paper is relevant to mathematical AI because its authors say the research decisions, implementation and manuscript were produced through an agent harness, with Lean's kernel checking the formal proof.
What the formal check does—and does not—settle
The manuscript builds its route from a persistence argument for weakly reversible systems, an entropy-dissipation identity associated with Horn and Jackson, and a bounded-speed descent argument. Its public Lean development is intended to make the formal statement and all encoded dependencies inspectable by others. A successful kernel check is a strong guarantee about the proof term against the definitions and trusted kernel used in that development.
That is not identical to independent validation of every modelling choice, theorem statement, imported result or informal explanation. The paper relies in part on prior work for its persistence component, and the project is an unreviewed preprint. MathsAI has not built the repository or audited the Lean source. Still, it offers a concrete example of an AI-assisted workflow whose final mathematical artifact can be checked by a proof assistant rather than only read as natural-language prose.