Skip to content

Heime-Jorgen/kenosian-lean4

BranchesTags

Repository files navigation

K-Lean

Formal proofs as infrastructure.

Mathematical certainty for computational biology — no formal verification expertise required.

A Note to Maintainers

Computational biology is accumulating mathematical debt. The formulas underlying our tools — Michaelis-Menten, Hardy-Weinberg, pharmacokinetic decay, Shannon entropy — have been implemented, re-implemented, and approximated across thousands of codebases, rarely with machine-checked proofs that the implementation faithfully reflects the published claim.

K-Lean was built to address this: 94 Lean 4 theorems, each sorry-free, each verifiable by the Lean kernel. We serve them as a live REST API (Rust, 3,095+ req/s) so any project can call machine-certified biology math directly — no formal methods toolchain required.

We reach out to projects directly — not to promote, but to contribute. The researchers most likely to benefit are those already working on these problems. Some find this immediately relevant. Many do not. Both outcomes are legitimate, and both help us sharpen our work.

If we have contacted your project and it is not a fit, we respect that without reservation. If you would prefer we not engage with your repository going forward, please say so and we will stop immediately.

We are researchers building infrastructure we believe the field needs. We welcome scrutiny, pushback, and honest feedback.

CI License: Apache 2.0 Follow on X

What K-Lean does

Layer Technology What it verifies
Phase A JSON Schema + TTTPS I/O contract + operator-independent timestamp seal
Phase B Lean 4 kernel check Bounds, monotonicity, conservation laws — machine-certified
Phase C Standalone lake package Use in your own Lean 4 project without Mathlib PR approval

Quick start

Use in your Lean 4 project

Add to your lakefile.lean:

require KLean from git
  "https://github.com/Heime-Jorgen/kenosian-lean4" @ "main"

Then import any contract:

import KLean.Contracts.MichaelisMenten
import KLean.Contracts.PhenoAge
-- etc.

Verify locally

git clone https://github.com/Heime-Jorgen/kenosian-lean4
cd kenosian-lean4
lake build

Check a theorem

#check KLean.MichaelisMenten.velocity_monotone
#check KLean.HardyWeinberg.hardy_weinberg_equilibrium
#check KLean.ContactProbability.sigmoid_pos

Contract Coverage

94 contracts across 9 domains. Every theorem is sorry-free — verified by the Lean 4 kernel. No sorry. No trust required.

Real-World Applications

K-Lean contracts are in active use for verifying computational models in ongoing research:

Hematology ODE validation: A biomedical researcher applied ErythropoiesisODE.lean to formally verify boundary conditions of an erythropoiesis model — confirming RBC count non-negativity and convergence under physiological stimulation rates. The machine-verified contract replaced a manual parameter review step.

Enzyme Kinetics & Drug Response

Contract Key theorems Domain
MichaelisMenten velocity_pos, velocity_lt_vmax, velocity_monotone Enzyme kinetics
HillEquation effect_nonneg, effect_lt_emax Dose-response
CompetitiveInhibition velocity_pos, velocity_lt_vmax, velocity_decreases_with_inhibitor Drug inhibition
IC50Relationship ic50_pos, ic50_ge_KI, ic50_increases_with_substrate Cheng-Prusoff
HillCooperativity hillOccupancy_pos, hillOccupancy_lt_one, hillOccupancy_half_at_K Cooperativity
LangmuirIsotherm coverage_pos, coverage_lt_one, coverage_monotone Surface binding
ReceptorBinding occupancy_pos, occupancy_lt_one, half_occupancy_at_KD Drug-receptor
CatalyticEfficiency catalytic_efficiency_pos, catalytic_efficiency_increases_with_kcat Enzyme efficiency

Longevity & Biological Age

Contract Key theorems Domain
PhenoAge mortalityScore_pos, mortalityScore_lt_one, phenoage_M_range Levine 2018
Telomere telomere_pos, telomere_decreasing, telomere_wellDefined Herrmann 2023
BiologicalAge ensemble_nonneg, ensemble_upper_bound, insufficient_knowledge_propagates Composite age
GompertzMortality mortality_pos, mortality_increasing Aging rate
WeibullSurvival survival_pos, survival_le_one, survival_decreasing Survival analysis
TelomereAttrition telomereLength_pos, telomereLength_decreasing, hayflick_bound L-DNA
GCContent gcContent_nonneg, gcContent_le_one L-DNA stability
DnaTm meltingTemp_nonneg, meltingTemp_increases_with_GC, meltingTemp_pos_of_gc L-DNA melting
EpigeneticClockAcceleration clock_age_nonneg, acceleration_real, reversal_possible Epigenetic aging
SenolyticSelectivity selectivity_nonneg, selectivity_bound, clearance_monotone Senolytic therapy
InflammAgingScore score_nonneg, score_monotone_il6, score_bounded Inflammaging
StemCellSelfRenewal symmetric_renewal_one, asymmetric_renewal_half, symmetric_gt_asymmetric Stem cell niche

Clinical & Renal Function

Contract Key theorems Domain
CkdMdrd egfr_pos MDRD equation
CkdEpi ckdEpi_pos CKD-EPI 2021
CockcroftGault crcl_pos Renal clearance
MeldScore meld_increases_with_bili, meld_increases_with_inr, meld_increases_with_creat Liver function
HendersonHasselbalch pH_eq_pKa_when_equal, pH_increases_with_ratio Acid-base
Osmolarity osmolarity_pos, osmolarity_increases_with_na Serum osmolarity
OsmoticPressure osmoticPressure_pos, osmoticPressure_increases_with_concentration van't Hoff
BloodOxygenSaturation saturation_nonneg, saturation_le_one, full_saturation SpO2
BMI bmi_pos, bmi_increases_with_weight, bmi_decreases_with_height Body composition
CardiacOutput cardiacOutput_pos, cardiacOutput_increases_with_hr Fick principle
ErythropoiesisODE equilibrium_nonneg, equilibrium_pos, equilibrium_monotone_epo Hematopoiesis

Genetics & Population Biology

Contract Key theorems Domain
HardyWeinberg hardy_weinberg_equilibrium, freq_AA_nonneg Population genetics
SirEpidemic reproductionNumber_pos, epidemic_threshold Epidemiology
LogisticGrowth population_pos, population_le_K Cell proliferation
CellDoublingTime doublingTime_pos, doublingTime_decreasing Growth kinetics
AllometricScaling allometric_pos, allometric_increases_with_mass Scaling laws
ClonalExpansion expansion_nonneg, expansion_pos_when_fit Immune/tumor dynamics
MonodGrowth growth_nonneg, growth_le_mumax, growth_monotone Microbial kinetics
NucleotideBalance energyCharge_nonneg, energyCharge_le_one ATP/ADP/AMP
AbsorbingStateProbability absorption_prob_nonneg, absorption_prob_le_one, terminal_has_full_absorption Markov chains
BranchProbabilitySimplex branch_prob_nonneg, branch_prob_le_one, branch_simplex Phylogenetics
CigarInvariant refLen_nonneg, queryLen_nonneg, cigarItem_len_pos Sequence alignment
CodingSequenceLength valid_cds_divisible_by_three, num_codons_pos, concat_preserves_frame CDS
GOEnrichmentClosure closure_monotone, closure_union_superset, closure_singleton Gene ontology
MarkovTransitionStochasticity entry_le_one, stochastic_row, entry_mem_unit_interval Stochastic matrices
NucleotideCompositionSum composition_sums_to_one, all_fractions_nonneg Sequence composition

AlphaFold & Protein Structure

Contract Key theorems Domain
ProteinRMSD squaredDeviation_nonneg, rmsd_nonneg, rmsd_zero_iff Structure comparison
BoltzmannDistribution boltzmannFactor_pos, probability_pos, probability_le_one Energy states
ContactProbability sigmoid_pos, sigmoid_lt_one, sigmoid_monotone Contact prediction
TmScore tmTerm_pos, tmTerm_le_one, tmTerm_eq_one_iff Structure similarity
PairwisePotential totalEnergy_linear, totalEnergy_append Residue energy
SequenceIdentity seqIdentity_nonneg, seqIdentity_le_one, seqIdentity_one_iff_identical MSA
AlphaFoldConfidence plddt_bounds, high_confidence_threshold pLDDT bounds
ProteinAggregationRate rate_nonneg, rate_monotone, proteostasis_balance Aggregation kinetics
TMScore tmScore_nonneg TM-score (variant)

Biophysics & Physical Chemistry

Contract Key theorems Domain
BeerLambert absorbance_pos, absorbance_monotone_concentration Spectroscopy
NernstEquation nernstPotential_increases_with_cout Membrane potential
FickDiffusion flux_nonneg_with_gradient, flux_proportional_to_D Mass transport
FretEfficiency fret_pos, fret_lt_one, fret_decreases_with_distance FRET biosensors
EinsteinStokes diffusionCoeff_pos, diffusionCoeff_decreases_with_radius Diffusion
PoiseuilleFlow flowRate_pos, flowRate_increases_with_radius Blood flow
ArrheniusEquation rateConstant_pos, rateConstant_increases_with_temp Reaction kinetics
GibbsFreeEnergy gibbs_neg_when_exothermic_and_entropy_pos, gibbs_decreases_with_temp Thermodynamics
DiffusionMapEntropy entropy_nonneg, uniform_entropy Dimensionality reduction

Mitochondria & Cell Biology

Contract Key theorems Domain
ProtonMotiveForce pmf_pos_of_dominant_potential, pmf_linear_in_potential Mitchell equation
AtpSynthaseEfficiency efficiency_pos, efficiency_le_one, efficiency_lt_one_strict Bioenergetics
TranslationRate translationRate_pos, translationRate_increases_with_mRNA Ribosome
RibosomeDensity coverage_nonneg, coverage_le_one, coverage_increases_with_ribosomes TASEP model
CellCycleFraction conservation, g1_le_one, s_le_one, g2_le_one, m_le_one Cell cycle
MrnaHalfLife halflife_pos, decay_nonneg, decay_decreasing RNA stability
ProteinSteadyState steadyState_pos, steadyState_increases_with_synthesis Protein turnover
AutophagyFluxBalance flux_nonneg, net_autophagy_nonneg, starvation_upregulates Autophagy
MitochondrialMembranePotential healthy_potential_neg, potential_lower_bound, healthy_range Membrane potential
NADPlusRatio nad_plus_pos, ratio_pos, ratio_decreasing NAD+/NADH

Pharmacokinetics & Lab Methods

Contract Key theorems Domain
FirstOrderPK concentration_pos, concentration_decreasing, halflife_positive PK
BodySurfaceArea bsa_pos, bsa_nonneg Mosteller
PcrAmplification copies_pos, copies_increasing_in_cycles, copies_doubles_per_cycle PCR
DilutionSeries concentration_pos, concentration_decreasing Lab protocol
ShannonEntropy entropy_at_half, entropy_symmetric Information theory
FluorescenceQuantumYield quantumYield_pos, quantumYield_lt_one, quantumYield_eq_one_iff_no_nonradiative Biosensors

Synthetic Biology

Contract Key theorems Domain
SynNotch and_gate_logic, and_gate_true_iff_both, and_gate_false_if_either_absent Cell engineering
Riboswitch confidence_in_unit_interval, insufficient_knowledge_when_low_confidence RNA design
LongevityProtocol pipeline_confidence_bounded, valid_age_range, ik_propagates_pipeline K-Lean pipeline
CircularRNABacksplice backsplice_score_nonneg, canonical_backsplice_positive, higher_score_preferred circRNA
IRESActivity activity_mem_unit_interval, higher_activity_more_translation, inactive_ires_no_initiation IRES
RNAFoldingFreeEnergy stable_implies_nonpos_energy, more_negative_dg_more_stable RNA folding
StemLoopStability hairpin_energy_nonpos, more_pairs_more_stable, loop_size_valid Stem-loop
ModifiedNucleotideRatio ratio_nonneg, ratio_le_one, full_substitution_iff mRNA modification
PolyASiteStrength strength_mem_unit_interval, canonical_site_strength_one, stronger_site_dominates Poly-A site
TranslationInitiationContext kozak_score_mem_unit_interval, perfect_kozak_score_one, better_kozak_not_worse Kozak sequence
CodonAdaptationIndex cai_pos, cai_le_one, cai_eq_one_iff_optimal Codon optimization

ML & Single-Cell Analysis

Contract Key theorems Domain
GPPosteriorVariance posterior_variance_nonneg, dirac_has_zero_variance, variance_zero_iff_dirac Gaussian process
PseudotimeOrdering pseudotime_nonneg, root_pseudotime_zero, root_is_minimal Trajectory analysis
SparseApproximationBound approx_error_nonneg, more_inducing_tighter, max_budget_minimal_error Sparse methods

Academic Usage (Paper Appendix Pattern)

K-Lean follows the leanblueprint academic standard:

\appendix
\section{Formal Verification (K-Lean)}
All numerical claims in this paper have been machine-verified using Lean 4.
See \texttt{FORMALIZATION.md} and \url{https://github.com/Heime-Jorgen/kenosian-lean4}.

Reference as:

@software{klean2026,
  title  = {K-Lean: Machine-Verified Mathematical Contracts for Biology},
  author = {Jang, Peter},
  year   = {2026},
  url    = {https://github.com/Heime-Jorgen/kenosian-lean4},
  note   = {Lean 4 formal proofs, sorry-free}
}

See FORMALIZATION.md for per-contract theorem references.

CI Integration

K-Lean contracts are mathematical specifications. To connect them to your implementation:

Python / pytest-hypothesis (no Lean installation required)

Each K-Lean contract corresponds to a property you can test against your code:

from hypothesis import given, strategies as st

@given(st.text(alphabet="ACGT", min_size=1))
def test_gc_content_bounds(seq):
    gc = compute_gc_content(seq)
    assert 0.0 <= gc <= 1.0  # KLean.GCContent invariant

@given(st.floats(min_value=0), st.floats(min_value=0))
def test_mrna_halflife_positive(k, t):
    result = mrna_concentration(k, t)
    assert result >= 0  # KLean.MrnaHalfLife invariant

Coming soon: klean-py (Rust/PyO3)

We are building a Rust implementation of all 64 contracts, compiled to a Python extension via PyO3:

pip install klean  # coming soon
from klean import gc_content, mrna_halflife, sequence_identity

This closes the gap between formal Lean specification and running Python code.

R / testthat

test_that("gc_content bounds", {
  expect_true(gc_content(seq) >= 0 && gc_content(seq) <= 1)
})

Phase A: API Integration

K-Lean contracts are enforced at runtime via the KPP API (kpp.kenosian.com):

curl -X POST https://kpp.kenosian.com/api/v1/verify/klean \
  -H "X-API-Key: YOUR_KEY" \
  -H "Content-Type: application/json" \
  -d '{
    "tool_id": "klean:bloodwork:phenoage:v1",
    "request_payload": {"chronological_age": 45, "albumin": 4.1},
    "response_payload": {"phenotypic_age": 38.2}
  }'

Returns a TTTPS-sealed badge with roughtime_k >= 3 (operator-independent timestamp).

Repository Structure

KLean/
├── Basic.lean              -- Core types (ConfidenceGrade, InsufficientKnowledge)
├── Verifier.lean           -- Phase A <-> Phase B bridge
└── Contracts/              -- 64 sorry-free contracts
    ├── AllometricScaling.lean
    ├── ArrheniusEquation.lean
    ├── AtpSynthaseEfficiency.lean
    ├── BMI.lean
    ├── BeerLambert.lean
    ├── BiologicalAge.lean
    ├── BloodOxygenSaturation.lean
    ├── BodySurfaceArea.lean
    ├── BoltzmannDistribution.lean
    ├── CardiacOutput.lean
    ├── CatalyticEfficiency.lean
    ├── CellCycleFraction.lean
    ├── CellDoublingTime.lean
    ├── CkdEpi.lean
    ├── ClonalExpansion.lean
    ├── CockcroftGault.lean
    ├── CompetitiveInhibition.lean
    ├── ContactProbability.lean
    ├── DilutionSeries.lean
    ├── DnaTm.lean
    ├── CkdMdrd.lean
    ├── EinsteinStokes.lean
    ├── FickDiffusion.lean
    ├── FirstOrderPK.lean
    ├── FluorescenceQuantumYield.lean
    ├── FretEfficiency.lean
    ├── GCContent.lean
    ├── GibbsFreeEnergy.lean
    ├── GompertzMortality.lean
    ├── HardyWeinberg.lean
    ├── HendersonHasselbalch.lean
    ├── HillCooperativity.lean
    ├── HillEquation.lean
    ├── IC50Relationship.lean
    ├── LangmuirIsotherm.lean
    ├── LogisticGrowth.lean
    ├── LongevityProtocol.lean
    ├── MeldScore.lean
    ├── MichaelisMenten.lean
    ├── MonodGrowth.lean
    ├── MrnaHalfLife.lean
    ├── NernstEquation.lean
    ├── NucleotideBalance.lean
    ├── Osmolarity.lean
    ├── OsmoticPressure.lean
    ├── PairwisePotential.lean
    ├── PcrAmplification.lean
    ├── PhenoAge.lean
    ├── PoiseuilleFlow.lean
    ├── ProteinRMSD.lean
    ├── ProteinSteadyState.lean
    ├── ProtonMotiveForce.lean
    ├── ReceptorBinding.lean
    ├── RibosomeDensity.lean
    ├── Riboswitch.lean
    ├── SequenceIdentity.lean
    ├── ShannonEntropy.lean
    ├── SirEpidemic.lean
    ├── SynNotch.lean
    ├── Telomere.lean
    ├── TelomereAttrition.lean
    ├── TmScore.lean
    ├── TranslationRate.lean
    └── WeibullSurvival.lean

Honest Scope

K-Lean verifies computational integrity — that a function matches its published formula. It does not assert:

  • Clinical or biological correctness
  • Efficacy of the underlying algorithms
  • Safety for medical use

Contributing

All theorems must be sorry-free. CI checks this on every push:

grep -r "sorry" KLean/ && exit 1

See CONTRIBUTING.md for the contribution guide and FORMALIZATION.md for the academic paper appendix format.

We welcome contributions — new biology contracts, proof improvements, or domain extensions.

  • Issues and pull requests welcome.

License

Apache 2.0 — see LICENSE.

K-Lean is the first Lean 4 library for computational biology. Analogous: TLA+ : distributed protocols :: K-Lean : biological computation.

klean-server (live)

A Rust-native HTTP API serving all 94 contracts at 3,095+ req/s (GCP, single instance):

  • klean-server — Axum REST API, live at https://kpp.kenosian.com/v1/
  • klean-py — PyO3 Python bindings (pip install klean, coming soon)
  • Sub-millisecond per-call latency
import requests
r = requests.post("https://kpp.kenosian.com/v1/michaelis_menten",
    json={"substrate": 0.5, "km": 0.1, "vmax": 2.0})
print(r.json())
library(httr2)
req <- request("https://kpp.kenosian.com/v1/shannon_entropy") |>
  req_body_json(list(sequence = "ATCGATCG")) |>
  req_perform()
resp_body_json(req)

See bindings/klean-rs/ for the implementation.

Kenosian Protocol Platform

K-Lean is part of the Kenosian Protocol Platform — machine-verifiable bio-audit with TTTPS operator-independent timestamping.

kpp.kenosian.com/k-lean.html

About

K-Lean: 64 machine-verified contracts for computational biology (Lean 4, sorry-free)

kpp.kenosian.com/k-lean.html

Topics

bioinformatics reproducible-research biology theorem-proving mathematics computational-biology proof-assistant formal-methods formal-verification lean4

Resources

Readme

License

View license

Contributing

Contributing
Activity

Stars

4 stars

Watchers

0 watching

Forks

0 forks
Report repository

Releases

1 tags

Packages

 
 
 

Contributors

Languages