Can a law of biology be checked by a computer? One can.

This page reports on lean/, where DELPHI writes the mathematical laws it has extracted as theorems in Lean 4, a proof checker, and asks the checker whether each proof is complete. Every number here is read from lean.json, which lean/report.mjs writes after running the compiler. Nothing is typed by hand.

What is proved, from what

The argument, in plain words

Set up a population of M gene copies (M = 2N for N diploid individuals). A new mutation is present in 1 of them. Each generation, the next M copies are drawn at random from the current ones. That is the Wright–Fisher model, and in Lean it is literally the binomial formula C(M, j) (i/M)^j (1 - i/M)^(M-j).
Neutral means the average does not drift. If i copies are mutant now, the expected number next generation is exactly i. The Lean structure NeutralChain takes this as a hypothesis, and the Wright–Fisher instance proves it from the binomial formula (via Mathlib's Bernstein polynomials).
Sooner or later the lineage is lost or fixed. From any in-between state there is a positive chance of finishing in one step, so the chance of still being undecided after t generations shrinks like ρ^t for some ρ below 1. This is unresolved_le_pow.
Conservation of the mean does the rest. i = M × P(fixed by t) + (undecided mass), and the undecided mass vanishes, so P(eventual fixation) = i/M. For a single new mutant, 1/M. This is fixedBy_tendsto, with the explicit error bound in fixedBy_sub_le.
Kimura's step. Mutations arrive at Mμ per generation; each fixes with probability 1/M; so substitutions happen at Mμ × 1/M = μ per generation, whatever M is. That is neutral_substitution_rate. The population size cancels, which is why a molecular clock can exist.

A proof shows the conclusion follows from the assumptions. It says nothing about whether real genomes satisfy them. That is the job of the claim tests, and the gap is deliberate.

Second theorem, in plain words: Fisher's fundamental theorem

Types and fitnesses. A population has finitely many types (alleles at one locus in a haploid or clonal organism), each with a frequency p and a fitness w. Mean fitness w̄ is the frequency-weighted average of w. This is meanFitness.
One generation of selection. Each type's share next generation is p × w / w̄. The Lean theorem select_isFreq checks that this is again a set of frequencies summing to one.
Hold the fitnesses fixed and measure the change. That is the "partial change" of Price and Ewens: no frequency dependence, no changing environment. Then the new mean fitness minus the old equals the variance in fitness divided by the old mean. This is fisher_fundamental_theorem. Because every type breeds true in a haploid population, that variance is the additive genetic variance the claim names.
Corollary. A variance is never negative, so mean fitness never falls under fixed fitnesses: mean_fitness_nondecreasing. The claim's own context says the total change can fall when fitnesses are not fixed, and nothing here says otherwise.

Third theorem, in plain words: the twofold cost of sex

Two kinds of mothers. A fraction q of females reproduce without sex and have only daughters; the rest reproduce sexually and, with a 1:1 sex ratio, half their offspring are sons. Every mother has the same number of offspring. Males contribute nothing to the count.
Count next generation's daughters. The asexual share becomes q·f / (q·f + (1−q)·f/2). This is asexualNext.
The odds double. twofold_cost_of_sex proves that the odds of asexual to sexual females next generation are exactly twice this generation's, and the fecundity f cancels. Iterated, twofold_cost_of_sex_n gives 2ⁿ after n generations. That factor of two is the advantage sex must buy back to persist.

Did evolution have time? The flying-fish budget

Darwin (1859, ch. VI) wrote that flying-fish "might have been modified into perfectly winged animals". The fixation theorems above, extended to selection that does not oppose a mutant, bound how much substitution the Exocoetidae lineage has had since its oldest fossil. Every number below is computed by lean/bound/compute.mjs from lean/bound/parameters.json, where each value names its source.

Parameters and where each came from

What the lineage had (expected substitutions)

Ceiling as a function of N (vacuous by construction)

Why the verdict is inconclusive, and what this does not establish

Every theorem against the real flying fish

One row per theorem the compiler accepted: does it apply to Exocoetidae, which inputs are measured for flying fish (with the file), which are proxies, which are missing, and the verdict when instantiated. A theorem is never falsified by data; its hypotheses are. Full tables: lean/AUDIT-FLYING-FISH.md, lean/flying-fish-audit.json; per-part grounding of the 3D model: lean/morphology-grounding.json.

Measured facts used

All rows

Is the generated fish well-formed? A kernel-checked certificate

The organism thread's tool emits a graph of ontology terms: body, organ systems, organs, tissues, cell types, each placed under a whole by a part_of statement Ubergraph served. lean/Delphi/Blueprint.lean proves, for any such graph, that a decidable checker implies acyclicity of part_of, transitivity of its closure, that every node reaches the body root, and that the pinned taxon statements exclude nothing. lean/blueprint/certify.mjs turns one emitted blueprint into Lean literals and lets the kernel evaluate the checker. Regenerate it whenever the blueprint is rebuilt.

A morphological law with a formal statement and a data test

Thompson (1917): weight tends to vary as the cube of a linear dimension. lean/Delphi/Thompson.lean proves that an exact cube law has log-log exponent exactly 3, and that a measured exponent other than 3 refutes the exact law on that interval. The exponents below were measured by the claims thread; they are pointed to, not derived.

Measured log-log exponents of weight on stature (NHANES)

What the theorems can rule out: constraints and a candidate ledger

The theorems as constraints (`lean/constraints.json`)

The open-problems candidates (`open-problems/candidates.formal.json` → `lean/eliminate/ledger.open-problems.json`)

Other ledgers: the physics thread's flier, and the physiology chain against sustained flight

Illustrative candidate ledger (`lean/eliminate/ledger.json`)

Genotype-level checks: the code, pleiotropy, development, time

Five checks the Design Studio's genetic edits need. Each is small, each is a statement about data or about a named model, and each says plainly what it cannot do.

The five checks

Developmental ordering, certified on the fin subtree

What the map says a gene reaches (the closure check)

Candidate ledger

Observations the checker uses, and why none of them is an axiom

An observation is not a mathematical truth. Every measurement here is a field of a Lean structure whose proof obligations are the inequalities the observation asserts, so a theorem that needs one takes it as an argument and the axiom list stays clean. Reject an entry and you lose its eliminations, nothing else.

Is the set consistent? The non-vacuity witness

The entries

Eliminations conditional on an observation

The law catalogue: what is checked, what is assumed, what is missing

Every law the Studio can check, every hypothesis it carries without proof, and every gap it must not treat as checked. Built from the compiler's own report (lean/laws.json, lean/LAWS.md).

By level

The theorems the compiler accepted

Each row is a theorem declaration in the source, with its docstring and the statement exactly as Lean read it. Lemmas (the scaffolding) are listed below.

Supporting lemmas

Is the Lean statement the law? Ask a different model

The compiler checks the proof, not the translation. The project rule is that whether a Lean statement faithfully renders the paper's law is judged by an assessor from a different provider than the one that wrote it, blind to the proof. These modules were written by Claude, so Claude does not score them. Each assessor saw only the claim text, the theorem statement and its definitions.

The compiler's own audit

Two things make a Lean proof trustworthy: it compiled, and #print axioms lists only Lean's three standard axioms. A sorry (a hole in a proof) would show up as sorryAx. This table is parsed from the compiler's output.

Build log tail and raw audit output

Watch it converge

A numerical illustration, computed in your browser by iterating the same matrix the theorem is about. It is not part of the proof. Pick M and see the probability that a single new mutant is fixed by generation t approach the proved limit 1/M.

Gene copies M: Generations shown:

Table view

Reproduce it from a clean checkout

Versions pinned in the repo

Commands

cd lean
lake exe cache get      # Mathlib, prebuilt
lake build              # compiles every module
lake env lean Delphi/Audit.lean   # prints axioms
cd .. && node lean/report.mjs    # writes t/lean/lean.json

Needs elan (the Lean toolchain manager) and about 8 GB of disk for Mathlib. The exact Mathlib commit is in lean/lake-manifest.json; the toolchain is in lean/lean-toolchain.

Try to break it: mutation evidence

A proof nobody tried to break is not evidence. lean/mutate.mjs changes the statement of each headline theorem (or deletes a hypothesis of the model) in a copy of the module and asks the compiler to check the copy. Every mutant must be rejected; the unmodified modules must pass through the same command.

Nanopublication records

One record per nanopub, Delphi ontology v2.0: each law as a delphi:Concept carrying the Lean statement and an evidence item (build receipt and rejected mutants) linked from the published claim; the proof scope (kernel-checked vs assumed) as its own record; the faithfulness rubric; and one assessment record per claim per assessor with the verdict kept literal. Built by lean/nanopubs/build.mjs from the files on this page.

What this does not show

Not shown: that organisms obey the model

Strict neutrality, constant population size, non-overlapping generations and independent fates of mutants are assumptions. The theorem is exact inside the model and silent outside it. The claim's proposed empirical test compares synonymous-site substitution rates with pedigree-measured mutation rates; that is a claim-test job, not a Lean job.

Not shown: that the Lean statement is a faithful translation

The project rule is that whether a Lean statement renders the paper's law faithfully is judged by an assessor from a different model provider than the one that wrote it. These modules were written by Claude (Anthropic).

Not shown: a published nanopub

Nothing here has been signed or published. The plan is a delphi:Concept nanopub per law carrying the Lean source and a commit-pinned link, on the test registry first, with leanVerified true only because the audit above says zero sorry and standard axioms.

Scope of the fixation theorem

Kimura's 1962 formula covers selection (s ≠ 0) in the diffusion limit. The Lean theorem covers the neutral case only, for the exact finite Wright–Fisher chain rather than the diffusion approximation. That is the part the substitution-rate law actually needs.