In formal mathematics, there is a tempting escape hatch called native_decide. When a proposition is decidable but the proof term is too large for the Lean 4 kernel to evaluate, native_decide compiles the decision procedure to native code and trusts the result. It works — but it injects axioms (Lean.ofReduceBool, Lean.trustCompiler) that break the verification chain. The kernel no longer independently checks the proof.

For a formalization of modular forms in the Ripple project — specifically, the Sturm bound certificate for the modular polynomial $\Phi_{41}$ — this escape hatch had been in place for weeks. Every attempt to remove it had failed. This post describes how a combination of ChatGPT (for API search) and a Claude agent (for proof discovery) finally eliminated it.

The Problem

The Sturm bound principle says: if a modular form $f$ of weight $k$ and level $N$ has its first $S$ Fourier coefficients equal to zero, then $f = 0$. The bound $S$ depends on $k$ and $N$. For $\Phi_{41}$ (a weight-1008 form for $\Gamma_0(41)$), the Sturm bound is $S = 3528$.

Verifying that the first 3528 coefficients are zero requires bounding the height of intermediate computations. The recurrence relation for the coefficients involves products of Eisenstein series $E_4$ and the discriminant $\Delta$:

The coefficient bound we needed was:

for all $j \leq 42$ and $n < 3529$, where $B$ is some explicit finite bound. The previous proof used native_decide to evaluate $B$ directly — the kernel computed all 3529 coefficients of a 43-row recurrence array and checked each one. Fast, but axiom-contaminated.

The Wall

The analytical approach is to bound the coefficients using majorants. If $\lvert a_n \rvert \leq F(n)$ for all $n$, then $F$ is a majorant of the sequence $(a_n)$. Majorants are closed under convolution (corresponding to multiplication of power series), so:

where $G_4(n) = 2880 \cdot \binom{n+2}{3}$ is a known majorant of $\lvert [q^n] E_4 \rvert$ (from the bound $\sigma_3(n) \leq 2n^3$).

The majorant of a $k$-fold convolution of $\binom{n+d}{d}$ is given by the Vandermonde-type identity:

So the majorant of $E_4^{126}$ at index $n$ is bounded by:

At $n = 3528$, this is $2880^{126} \cdot \binom{4031}{503}$. And here is the wall: $\binom{4031}{503}$ is a 658-digit number. Neither norm_num nor decide can evaluate it in the Lean 4 kernel. Every previous attempt to prove the bound analytically had stalled at this exact computation.

The Breakthrough: Algebraic Overapproximation

The key insight, discovered by an AI agent after approximately 100 minutes of autonomous exploration: you do not need to compute the binomial coefficient at all.

The Sturm principle only needs the bound $B$ to be finite — its exact value is irrelevant. So instead of computing $\binom{4031}{503}$ precisely, overapproximate it with powers:

Step 1. $\binom{n}{k} \leq n^k$ for all $n, k$ (proved by induction via Pascal’s rule).

Step 2. $\binom{4031}{503} \leq 4031^{503}$.

Step 3. $4031 \leq 2^{12} = 4096$ (a 4-digit norm_num check).

Step 4. $4031^{503} \leq (2^{12})^{503} = 2^{6036}$.

Step 5. Similarly, $2880 \leq 2^{12}$, so $2880^{126} \leq 2^{1512}$.

Step 6. The product is bounded by $2^{1512} \cdot 2^{6036} = 2^{7548}$.

Step 7. $2^{7548} \leq 10^{2400}$, verified via the intermediate step $2^{100} \leq 10^{31}$ (a 31-digit comparison — well within norm_num’s range).

Every single step involves numbers of at most 31 digits. The kernel handles each one instantly. The final bound $10^{2400}$ is much larger than the original $10^{1090}$, but it does not matter — the Sturm principle cares only that the bound exists, not that it is tight.

The Collaboration

This result emerged from a specific division of labor:

• ChatGPT (with a repository connector) located the relevant Mathlib theorems in one round: PowerSeries.invOneSubPow_add for the multiplicative structure of $(1-X)^{-k}$, and Finset.sum_le_card_nsmul for bounding finite sums. Searching the 500K+ line Mathlib library by blind grep would have taken far longer.

• A Claude agent (Opus 4.6) ran autonomously for 100 minutes, reading the 960-line proof file, trying multiple approaches (including the Vandermonde identity route that required the 658-digit computation), and eventually discovering the power-chain overapproximation that bypassed the large-number wall entirely.

Neither tool alone would have solved this efficiently. ChatGPT cannot write and compile Lean proofs; the agent cannot search a 500K-line library as fast as an indexed connector. The combination — search with one, prove with the other — is what made it work.

Result

The file SturmCRTBound.lean now contains 530 lines of kernel-verified proof with:

• 0 sorry
• 0 native_decide
• 0 custom axioms
• Axioms: [propext, Classical.choice, Quot.sound] only

The entire Ripple repository — covering CRN-computable numbers, population protocols, modular forms, and Padé approximation — now has zero sorry across its codebase.

「善战者，求之于势，不责于人。」—— 《孙子兵法·势篇》 “The skilled strategist seeks victory from the situation, not from individuals alone.” — Sun Tzu, The Art of War, Chapter V