Ripple: An Open, AI-Formalized Lean 4 Framework for Computing with CRNs

Ho-Lin Chen and Xiang Huang
32nd International Conference on DNA Computing and Molecular Programming
Fayetteville, Arkansas · August 3–7, 2026

• Open the interactive talk slides
• Download the Beamer talk (PDF)
• Beamer LaTeX source package (zip) · ripple-talk.tex
• View the poster (PDF)
• Poster LaTeX source (zip) · poster.tex
• Read the technical report

Ripple supplies the domain-specific definitions and reusable lemmas needed to build machine-checked proofs about chemical reaction networks and population protocols. The talk presents the library, its experimental formalization landscape, and a workflow in which AI writes proofs, Lean checks them, and domain experts review whether the formal statement captures the intended theorem.