The Warranty Card Metaphor
A mathematical theorem is like a warranty card: the conclusion is the headline on the front ("error within 1+ε times the optimal"), while the applicability conditions (rank of A at least k, positive parameters, non-zero inputs) are the fine print on the back. Human readers implicitly fill in missing conditions hidden behind words like "obviously"—but an AI using the theorem to provide guarantees must hold every clause. Miss one, and the AI may declare a claim "successfully formalized" while nobody notices.
The FARMS paper (Faithful Alignment and Representation of Mathematical Statements) by Di Wu (University of Maryland), Ling Liang (University of Tennessee, Knoxville), and corresponding author Haizhao Yang (University of Maryland) formalizes 171 targets—theorems, propositions, and key statements—from four classic textbooks into Lean 4.
Four Textbooks, 171 Theorems
FARMS draws from two hardcore areas of computational mathematics:
- Drineas & Mahoney textbook: 32 targets
- Halko, Martinsson & Tropp survey on randomized NLA: 35
- Martinsson & Tropp textbook: 20
- Larsson & Thomée monograph on numerical PDEs: 84
- A = zero matrix, k = 1: no valid output exists—the rank restriction k ≤ rank(A) was missing.
- n = 1: α = k·log(n)/ε² vanishes and log(α) is undefined; Lean silently defines log(0) = 0, so the compiler let undefined values slip through as 0.
- Steady-state heat flow: −(a_ηu′)′ = f with conductivity contrast 100 and 1,000 (η = 0.01, 0.001), 512 unknowns, 8,192×512 weighted gradient matrix. Gaussian sketch to 2,048 rows, QR factor as preconditioner: condition numbers 8.83–8.95 vs. diagonal-preconditioning references of 99.6 and 964.0. All 6 runs reached 10⁻⁶ relative discrete energy error within 22 iterations—iteration counts did not degrade with contrast, exactly the shape of the formalized bound.
- Wave-response compression: string u_tt = u_xx, 384 initial excitations in a 256-dimensional energy coordinate matrix. Gaussian sampling with exact residual checks selected 128 basis responses with residual bounds 0.00877–0.00938, under the 0.01 target. A 32-timestep response library compressed from 24 MiB to 8.375 MiB. Energy conservation carries the initial representation-error bound to all future times—one factorization check covers all allowed queries and all non-negative times.
- Paper: FARMS: A Verifiable Foundation for Automated Computational Science
- arXiv: 2610.40560 (2026-10-29), https://arxiv.org/abs/2610.40560
- Code: https://github.com/Woody2357/FARMS-Computational-Science
- Project page: https://woody2357.github.io/FARMS-Computational-Science/
Phrases like "for n sufficiently large" mean nothing to Lean—they must become explicit threshold functions such as n ≥ C·log(1/δ)/ε², with every constant and parameter range pinned down. Even more dangerous is the semantic level: a candidate statement can compile while a quantifier is silently flipped from "exists" to "for all", reversing the theorem's meaning.
The Pipeline: A Multi-Window Notary Office
FARMS is a multi-agent pipeline where each role watches the others:
1. Source auditor – checks that every statement comes with all material needed for formalization; gaps go to the retriever (deterministic retrieval, no improvisation), and the evidence reviewer verifies whether gaps are filled. The loop is bounded. 2. Formalizer – generates Lean 4 statements using evidence and a shared domain library of already-formalized definitions. 3. Lean compiler – only a syntactic/type check. Passing compilation says nothing about faithfulness. 4. Semantic referee – checks objects, assumptions, quantifier order, algorithmic constructions, and quantitative guarantees against the source. Mismatches go to the repairer. 5. Consistency reviewer – final review; disagreements return to the semantic referee.
A side path handles abstention: if a gap persistently cannot be filled, the abstention referee judges whether abstaining is justified and the explainer records the reason. Honest abstention is treated as distinct from repair—like a library marking an item "temporarily unavailable" rather than fabricating an entry.
Vacuous Truth: Formalization's Top Enemy
An implication "if P then Q" is vacuously true when P has no true instances—"all unicorns are white." For randomized low-rank approximation theorems, omitting the precondition "a valid output exists" makes "all valid outputs satisfy the error bound" vacuously true if the algorithm can never produce a valid output. The system declares success, and the success is counterfeit.
This trap is uniquely lethal for computational guarantees: their entire purpose is to reassure a running machine. Downstream experiment design, hyperparameter choice, even funding decisions can rest on a fake "guaranteed." Silent vacuous truth is more dangerous than honest failure—which at least makes noise.
Case 1: Two Lost Lines of Fine Print
On the randomized low-rank approximation theorem, the initial candidate compiled cleanly, but the semantic referee caught two dropped cases:
Both errors escaped the compiler entirely; only semantic review against the source caught them.
Case 2: A Textbook Caught by Its Own Student, 50 Years Later
The climax: a textbook claim on random matrix multiplication states that norm-weighted sampling (probability of item i proportional to ‖A's i-th column‖·‖B's i-th row‖) minimizes expected squared Frobenius error, optimal over all admissible distributions q (non-negative entries summing to 1).
The formalizer faithfully kept the domain allowing qᵢ = 0. The semantic referee constructed an explicit counterexample with A = [1, 1], B = [1, −1]ᵀ, one sample: exact product AB = 0. The "optimal" distribution p* = (1/2, 1/2) gives E(p*) = 4, while admissible q = (1, 0) gives E(q) = 1. The claim would require 4 ≤ 1—impossible.
The root cause: the unbiasedness argument needs every non-zero contribution to have positive sampling probability—a condition missing from the original text. The textbook itself was wrong. The pipeline kept the source claim intact, recorded the missing condition as an explicit source warning, and marked the run as not accepted. Source-vs-repaired claim miscalibration must be distinguishable—readers and downstream AI deserve to know whether the warranty card is factory-original with a publicized defect or has been quietly swapped.
20x Cheaper, and More Rigorous
Results: 157 of 171 targets accepted (91.8%)—154 clean, 3 with source warnings; the rest abstained with recorded reasons.
Cost per target across the four sources: $1.92, $0.85, $2.29, $2.08 (all-in). On 6 random targets, FARMS spent $17.06 total (2.275M tokens) vs. AutoformBot's statement-level adaptation at $348.09 (63.071M tokens): $2.84 vs $58.02 per target (20.4x), 0.379M vs 10.512M tokens (27.7x).
The savings come from eliminating uncertainty *before* generation: source audits pin down what to formalize, retrieval takes only needed evidence, the shared domain library avoids re-invention, bounded loops prevent spinning, and semantic review catches "compiles but wrong meaning" candidates early instead of burning tokens retrying the same semantic errors.
Turning Theorems into Skills
Unlike RAG-style retrieval where a model vibes its way to "this theorem probably applies," FARMS compiles each theorem with all conditions into an implication whose premises are machine-checkable propositions. An agent invoking a skill must mechanically verify the premises (rank sufficient, parameters positive, dimensions correct) before citing the conclusion—if premises fail, the skill refuses to fire. Guarantees upgrade from "the model thinks it's fine" to "the compiler verified it's fine."
Two demonstrations:
The Middle Chapter: Legislator and Notary
This is the second of a trilogy. The first, AWM, has AI propose and prove its own conjectures—a legislator. FARMS is the notary: registering a century of human computational mathematics, verifying its clauses, publicizing its defects. Both are needed: without legislators there are no new laws; without notaries, old laws' fine print silently disappears in translation. When AI comes to claim on the warranty card, the fine print is now complete—and if the card truly has a defect, the sign is posted in the open. That is the foundation verifiable automated science should have: before building the tower, verify every brick's factory certificate.
---
References