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

Ho-Lin ChenNational Taiwan University
holinchen@ntu.edu.tw
Xiang HuangUniversity of Illinois Springfield
xhuan5@uis.edu
xianghuang.org

DNA 32 · August 3–7, 2026 · Fayetteville, Arkansas

Math problem and coffee into mathematician, producing a proof
Math problem and token into AI, producing a Lean proof

Being a theoretical computer scientist is an awesome job.

  • They hire us to prove theorems. They don’t tell us which theorem to prove.
  • “A mathematician is a machine for turning coffee into theorems.” — Alfréd Rényi

But there is a caveat.

Your proof may haunt you—maybe for life.

  • a typo
  • a hand-waved step
  • a false theorem you cite
  • a hidden assumption
  • a hidden error
  • …

How do we stop a proof from haunting us?

Formal proofs.

Formal means machine-checked.

What is a proof?

A step-by-step natural-number induction proof

boring · mechanical
(virtues of a proof)

A healthy mix of English and math
= informal proof

found in most books and papers

What is a formal proof?

Interlocking gears

Lean

Lean is a strict logical system: every step must mesh, with no gaps left unchecked.

What do we do with Lean?

  • Write proofs in Lean.
  • boring · mechanical (same old, same old)
  • This time, you can do it with AI!

AI writes. Lean checks.

Comparison of ordinary AI output and Lean-checked proof

But a proof checker is not yet a domain library.

Mathlib, Lean’s mathematical library, does not yet cover every domain—for example, chemical reaction networks or population protocols.

The missing layer

Definitions and reusable lemmas for proving properties of CRNs and population protocols.

Ripple connects research targets to Mathlib, published papers, and common mathematics

We treated it as an experiment.

Three experimental classes: our work, landmark papers, and open problems that the DNA community still wants to prove

What did we formalize?

Landscape table of the papers, results, and supporting mathematics formalized in Ripple

Find the shared mathematics.

Application threads resting on shared domain language and common mathematics

What grew inside Ripple?

≈ 920Lean files
≈ 768K≈ 768K1M+lines of Lean
≈ 23.4Ktop-level declarations

Current Ripple scale · experimental and still growing

So, what does our workflow look like?

1. What counts as an acceptable proof?

Three gates: faithful statement, kernel checking, and a successful fresh build

2. How do we finish checked proofs sooner?

Parallel work helps only when tasks stay independent—and every result still passes Lean.

Split work, run independent tasks in parallel, check every branch with Lean, and merge only passing proofs

3. Cost is a routing problem.

Different kinds of work routed to suitable models

August 3, 2026 · ongoing discussion

One of OpenAI’s ten announced advances is now being disputed.

OpenAI announcement: Ten advances in mathematics and theoretical computer science

OpenAI announced ten results on August 1. A new critique appeared today. The community has not yet reached a verdict.

We do not yet know where the issue lies.

Original
problem
Does this match?→
Formal
statement
→
Checked
proof

One possible failure mode is a valid proof of the formal statement—but a formal statement that does not faithfully capture the original problem.

Lean checks the proof. Domain experts must check the target.

Sources: OpenAI, August 1, 2026 · critique posted August 3, 2026

Future work: keep humans in the loop.

The live dispute turns “human review” from a general precaution into a concrete research requirement.

  • Human reviewDomain experts verify that the formal statement faithfully captures the intended theorem.
  • RefactorConsolidate duplicated infrastructure.
  • CurateDistill essential structures into a clean, minimal library.
  • Track MathlibContinuously test Ripple against upstream updates.
  • UpstreamContribute CTMC, Kurtz, and Frobenius foundations to Mathlib.

Kernel checking is necessary. Domain review is necessary too.

Thank you for your time.

AI writes. Lean checks. Ripple gears up the domain.

We gratefully acknowledge our funding agencies

Taiwan National Science and Technology Council

NSTC (Taiwan) · Grant 113-2221-E-002-204-MY3

U.S. Department of Energy Office of Science

U.S. DOE Office of Science, ASCR
Grant DE-SC0024278