Machine-checked Lean 4 proofs for mRNA-LNP delivery, from in-vivo decay to structural design.
Pardi N, Weissman D et al. · J Controlled Release 217 (2015)Pardi N, Tuyishime S, Muramatsu H, Karikó K, Mui BL, Tam YK, Weissman D. “Expression kinetics of nucleoside-modified mRNA delivered in lipid nanoparticles to mice by various routes.” Journal of Controlled Release 217 (2015) 345–351 (open access). 1-methylpseudouridine-containing mRNA is the platform referenced under Chemistry below.
Each contract takes its own inputs and proves its own bounds. Decay, translation, and structure are independent rate processes, each kernel-verified. The API returns a certificate naming the exact Lean 4 theorems. Sorry count 0, axiom count 0 across all six contracts.
Three contracts bound exponential decay kinetics: half-life from a fitted rate constant, the Pardi and Weissman 2015 two-point bioluminescence estimator, and abundance at any elapsed time t. All three describe the same decay law from different measurement angles.
n0, nt, delta_t from bioluminescence. The exact Pardi & Weissman 2015 estimator.
t½ = ln 2 / kdeg. Closed form once the rate is fitted.
m(t) = m₀·e−k·t. A point on the decay curve.
Does not claim: that your kdeg was fitted correctly, or that the result is the half-life of any specific construct.
Two contracts quantify ribosome machinery: a coverage fraction proved to stay in [0, 1], and a translation rate proved positive and increasing with transcript copy number.
n_ribosomes / l_mrna. Proved in [0, 1] for any nonnegative inputs.
codon_rate × density × mrna_copies. Proved positive and monotone.
Does not claim: that your assay data is correct, or that the coverage fraction is biologically meaningful for any particular transcript.
riboswitch_confidence maps minimum free energy and ensemble diversity into a proof-backed score in (0, 1). modified_nucleotide_ratio quantifies the fraction of 1-methylpseudouridine substitutions. Structural design relies on three independent folding levels, each kernel-verified.
conf(MFE, d) in (0, 1). Nonneg MFE forces score below threshold.
RNA Folding page →Globally optimal W-C + G·U base-pair count, both directions.
RNA Folding page →Zuker DP proven optimal for any per-pair cost (au/gc/gu). Not the full nearest-neighbour loop model.
RNA Folding page →Score in (0, 1). Nonneg MFE forces low score via InsufficientKnowledge gate.
modified / total. Proved in [0, 1], both boundary cases characterized exactly.
Does not claim: that the reported MFE or ensemble_div values are correct, or that a confidence score predicts how a riboswitch behaves in a cell.
Every value above was computed live against a Lean 4 contract at kpp.kenosian.com. Across all six contracts: sorry count 0, axiom count 0.
The theorems establish properties of the mathematical spec behind each formula: positivity, monotonicity, the [0, 1] bound on ratios and densities. They do not establish the biological correctness of any specific sequence, dose, or manufacturing run. K-Lean makes no clinical claim.
Every fact on this page is independently checkable against the live API, without trusting the prose.
GET /api/v1/klean/contracts returns every live endpoint with its Lean namespace, key theorems, and description.certificate.provenance naming the exact Lean toolchain (leanprover/lean4:v4.14.0) and mathlib revision.sorry or a cited axiom unless explicitly declared. These contracts carry neither. Documented on the technical README.Formally proved bounds on IGF1 receptor binding and Rett syndrome pathway contracts.
Query the K-Lean biomedical language model, trained on formally verified contract outputs.
Riboswitch interface, Nussinov optimality, and base-pair-additive MFE. The full RNA folding corpus.