A machine-checked account of RNA folding in Lean 4: base-pair optimality, the Zuker/Turner thermodynamic model, and a precise boundary between the algorithm we prove optimal and the empirical energy tables we leave as named, open inputs.
Lean 4 v4.14.0 · Mathlib dde4f2e · 0 axioms · nosorry
K-Lean formalizes RNA folding as three levels. At each level it states plainly what is
proven and what remains an open input, never hiding an unproven step behind a sorry
or an unconstrained axiom. Every result on this page is checked by the Lean 4 kernel; what
remains open is named explicitly, in the same breath, as a parameter you supply.
K-Lean audits computational integrity: that a folding computation matches a stated objective and its mathematical properties. It does not assert clinical or biological correctness, nor that any single objective is the right model of real RNA in a cell.
Free energy (ΔG) and ensemble diversity are the two inputs a fold predictor (e.g. an external ViennaRNA MFE computation) supplies. K-Lean does not assume the predictor is correct: it proves properties of the confidence function built from those two inputs, and treats the predictor itself as an untrusted external value.
Structural confidence is defined as a function of the free energy
ΔG and the ensemble diversity d:
The following are proven about it (4 theorems, live at
POST /api/v1/klean/compute/riboswitch_confidence):
confidence_pos and confidence_lt_one together give
conf ∈ (0,1) whenever ΔG < 0 and d > 0, combined in
confidence_in_unit_interval.insufficient_knowledge_of_unstable_fold: whenever ΔG ≥ 0 (a
thermodynamically unfavorable fold), conf falls below the 0.35 threshold, the
InsufficientKnowledge gate, where the system declines rather than guesses.An earlier version of this section described a MfeOracle structure and a theorem
oracle_stable_mfe_nonpos. Both were removed from the Lean source in a 2026-07-20
root-cleanliness audit: with the fold-validity predicate fixed to True, that theorem degenerated
into the unconditional (and physically false) claim that every fold has non-positive free energy, backed only
by projecting an assumed field, a disguised axiom. No genuine reproof exists, since an external MFE binary is
not decidable in Lean. This page now describes only what is genuinely proven.
Canonical pairing canPair admits the Watson–Crick pairs (A·U, G·C) and the G·U wobble.
It is symmetric (canPair_symm) and irreflexive
(canPair_irrefl). A secondary structure is a non-crossing (nested) partial matching
of canonically-complementary positions, and its score is the number of pairs.
The dynamic program nussinov computes the value γ(i,j) by well-founded recursion on interval
length, with no axioms, no sorry. Optimality is proven in both directions:
nussinov_sound: γ(i,j) is an upper bound on the pair count of every valid nested structure
on the interval.nussinov_achievable: that bound is actually attained.This is base-pair-count optimality, not the Turner ΔG
(Gibbs free energy) that production ViennaRNA minimizes. It is a cleaner, related objective, and the page
is explicit about the difference.
On novelty, stated exactly and no more strongly: “No prior formalization of Nussinov optimality is known to us in any proof assistant (Lean / Coq / Isabelle).”
Level 3 moves toward the thermodynamic objective ViennaRNA actually minimizes. It separates cleanly into two sub-states. Both are now kernel-verified and merged, for an abstract, parameterized cost. We prove that the dynamic program is optimal for whatever energy parameters you supply; we do not claim to have validated the empirical Turner energies themselves. Those remain explicit, named open inputs, and the page keeps that line sharp.
The Turner energy table is held as abstract parameters in TurnerModel:
no numeric constants baked in. Only qualitative sign/shape hypotheses are assumed: stacking is
non-positive (stacked_helix_nonpos) and loop penalties are non-negative
(multiloop_penalty_nonneg).
The Zuker W/V recursion Vstep/Wstep satisfies the structural facts
Wstep_le_Vstep, Wstep_le_other and Vstep_mono. For a
context-free per-pair cost, the min-energy DP is optimal and unique over all valid
structures (IsZukerOptimal, zuker_optimal_unique; energy is additive via
energyOf_append).
Real Turner stacking depends on the enclosing pair, so
energy((i,j)::P) ≠ cost(i,j) + energy(P), so the additive model of L3(a) no longer holds.
This is modeled with a nested-tree PairForest/PairTree, each pair's energy
depending on its immediate parent context (forestEnergy, treeEnergy,
abstract cost pc).
A context-carrying DP zukerCtx (well-founded recursion on interval length) is proven
optimal in both directions: soundness zukerCtx_sound, where the DP
lower-bounds the energy of every valid forest, and achievability zukerCtx_achievable_aux, where
that bound is attained. The closing-cost lemmas closeCostC /
closeCostC_of_legal are defined and proven, and the context-carrying decomposition (former
obligation O1) is closed.
Honest scope: this is optimality over an abstract, parameterized cost;
no numeric Turner constants are baked in. The empirical energy table (O5) is now closed
(Turner 2004 ViennaRNA table instantiated, sorry-free). The affine multi-loop term (O4) is now
closed for c_unpaired = 0 (achievability and optimality proven;
arbitrary-c_unpaired extension requires a 2D DP tracking loopUnpaired).
Whole module is sorry-free, axiom-free, and native_decide-free.
| Obligation | What it requires | Status |
|---|---|---|
| O1 | Context-carrying decomposition for zukerCtx |
closed · proven |
| O4 | Affine multi-loop energy term: achievability & optimality | closed · proven (c_unpaired = 0) |
| O5 | Empirical Turner-table bridge to ViennaRNA's experimental constants | closed · proven |
The Nussinov result (Level 2) is served as a verified compute endpoint. It returns the value together with a certificate naming the Lean theorems that back it, and a provenance block identifying the exact toolchain and Mathlib revision the proofs were kernel-checked against. The endpoint produces the value from our own kernel-verified contract, and it does not re-check a number you supply.
Request: every call carries an
X-API-Key header:
curl -s https://kpp.kenosian.com/api/v1/klean/compute/nussinov \
-H "Content-Type: application/json" \
-H "X-API-Key: $KPP_API_KEY" \
-d '{"sequence": "GGGAAACCC"}'
Response: the exact body returned by the live endpoint (toolchain and Mathlib revision are real, not illustrative):
{
"contract": "RnaNussinov",
"value": 3,
"value_kind": "exact",
"inputs": { "sequence": "GGGAAACCC" },
"certificate": {
"contract": "RnaNussinov",
"namespace": "KLean.RnaNussinov",
"verified": true,
"key_theorems": [
"nussinov_optimal", "nussinov_sound", "nussinov_achievable"
],
"theorem_count": 35,
"optimality_status": "proven_optimal",
"optimality_note": "nussinov_optimal proven: γ equals the max non-crossing
canonical base-pair count (sound + achievable), no sorry/axiom.",
"provenance": {
"lean_toolchain": "leanprover/lean4:v4.14.0",
"mathlib_rev": "dde4f2ecaec222a1c7db638d7536f0b195d8e953",
"build_time_utc": "2026-06-19T06:43:51Z",
"kernel_verified_source": "olean-existence",
"manifest_schema": "klean.verified_contracts/v1"
}
},
"disclaimer": "Theorems prove properties of the Lean spec that this value
implements; they do not assert biological/clinical correctness."
}
Reading the certificate: value_kind: "exact" appears only for the integer
Nussinov result, because it is proven to be the maximum (nussinov_optimal). The other
compute contracts (kinetics, GC content, identity, entropy) return "f64_approx", and their cited
theorems bound the real-valued spec, not the floating-point error of the returned
f64. GET /api/v1/klean/contracts lists every computable contract and its
value_kind.
It means the named theorems are kernel-verified in the cited build and that this value is the output of the algorithm those theorems describe. It does not mean the value is the biological ground truth, nor that the realistic Turner energy model has been validated; see Levels 2 and 3 for the exact boundary.
Prefer to run it locally? See the researcher guide: Python + Rust →
These RNA folding proofs connect directly to the FDA's electronic-records rule. The kernel-verified
results are validation evidence in the sense of §11.10(a): a computation
shown to match its specification for all covered inputs, re-checkable by the Lean 4 kernel rather than
asserted in a report. Sealed under a TTTPS tamper-evident timestamp, each verified result also carries a
secure, computer-generated audit trail in the sense of §11.10(e), recording
the date and time independently of the operator.
K-Lean supplies these technical controls; it does not replace a sponsor's full Part 11 compliance program, and makes no clinical or biological claim.