AI 中文总结
介绍用于CRN计算实数数学的Ripple框架，它形式化多种模型阶梯，开发可靠，暴露并修复证明漏洞，还证明新结果，且形式化主要由人工智能代理利用公开模型完成，工作流程可重现。
AI 中文摘要
我们展示了Ripple，一个用于通过化学反应网络（CRN）计算实数数学的开放的、人工智能形式化的Lean 4框架。Ripple形式化了完整的模型阶梯，包括GPAC/CRN连续统和CRN可计算实数、大种群协议（LPP）编译管道，以及通过库尔茨定理的三个机器检查版本与确定性平均场极限相连接的连续时间马尔可夫链（CTMC）层，还有两个图灵完备性结果。该开发是可靠的，暴露了已发表证明中的真正可修复漏洞，还证明了新结果，如通过其完整生成函数将阿佩里常数ζ(3)构造为CRN可计算数。形式化主要由人工智能代理仅使用公开可用模型完成，工作流程可重现。
英文摘要
We present Ripple, an open, AI-formalized Lean 4 framework for the mathematics of computing with chemical reaction networks (CRNs) -- one extensible, machine-checked development that gathers several strands of the field into a single setting, and is built to grow. It formalizes: the theory of which real numbers a CRN can compute -- a single Lean definition of real-time CRN computation, the class of reals it captures, and the compilation pipeline (a GPAC / polynomial-ODE layer, a dual-rail compiler, and four stages down to large-population protocols) that realizes them, built so that adding a new number is a plug-in; three landmark population-protocol majority algorithms -- approximate, exact, and self-stabilizing exact majority; the stochastic-to-deterministic bridge, through three machine-checked versions of Kurtz's mean-field theorem; and two classical Turing-completeness results -- Bournez--Graca--Pouly for the deterministic GPAC and Soloveichik--Cook--Winfree--Bruck for stochastic CRNs. Each of these is verified to depend on exactly the three Mathlib foundational axioms, with no sorry. Along the way the formalization repaired genuine, previously unnoticed gaps in published proofs -- a compilation step that can transiently leave the unit interval, and an algebraic-number construction that silently rests on Catalan's conjecture -- and surfaced a sharp open problem about when a holonomic series admits an exact, rational-data polynomial-ODE encoding. The whole development is open and every proof is kernel-checked, so the results can be independently re-verified; and because it was written predominantly by AI agents using only publicly available models, the workflow that produced it can be reproduced with the same public toolchain.
Comments26 pages. v2 removes the incorrect claim that the formalization found a gap in the Angluin-Aspnes-Eisenstat (2008) approximate-majority proof: the flawed inequality was internal to our formalization, not their argument. It also corrects the attribution of zeta(3)'s CRN-computability to the Fermi-Dirac integral route. Abstract revised
