In 1969, William Howard observed that the rules of natural deduction
in logic mirror the typing rules of the lambda calculus exactly —
one is a notational variant of the other.
The implication is profound: propositions are types, and proofs are programs.
To prove a proposition P is to construct a term of type P.
Curry-Howard in Lean 4
-- A proposition is a typedefMyProposition : Prop := ∀ n : ℕ, n + 0 = n
-- A proof is a term of that typetheoremmyProof : MyProposition := fun n => Nat.add_zero n
-- sorry = placeholder proof (compiles, but is NOT verified)theoremunfinishedProof : MyProposition := sorry-- ⚠ warning: declaration uses 'sorry'-- The AXLE goal: eliminate every sorry from the paper's argument-- #check myProof → MyProposition ✓-- #check unfinished → MyProposition ✗ (sorry)
In Lean 4, sorry is a magic term
that inhabits any type — it makes the file compile regardless of whether
the proof is actually valid.
A paper can do the same: a well-written argument reads as if every claim
is proven, even when some critical connections are asserted without evidence.
Those invisible sorrys are what peer review hunts for.
AXLE (Algebraic eXpression Language for Evaluation) applies this framework
to academic writing: every claim in a paper has a type
(what kind of evidence could inhabit it), and the paper is verified
only when every claim has an explicit evidence term — no sorry remaining.
§2 · The Operator Chain as a Lean 4 Structure
The operator chain G = U ∘ F ∘ K ∘ C can be formalised as a dependent type:
each operator takes the output type of the previous as its input type.
A well-typed paper is one where the composition is valid —
no type mismatches between operators.
G = U ∘ F ∘ K ∘ C as Lean 4 Types
structureRawDatawhere
measurements : List Float
n : ℕ
structureCompressedDatawhere-- output of C
features : List Float
compression_ratio : Float
h_valid : compression_ratio > 1 -- proof of non-trivial compressionstructureThresholdEventwhere-- output of K
crossed : Bool
k_star : Float
h_evidence : crossed → ∃ e, e ∈ evidence_set ∧ e > k_star
structureFoldedNarrativewhere-- output of F
results_section : String
h_subcritical : ¬overclaims results_section -- Ch9 conditionstructureUnfoldedDiscussionwhere-- output of U
claims : List Claim
h_stable : ∀ c ∈ claims, spectralReach c ≤ 1 -- Ch11 condition-- The composition G is well-typed iff every h_ proof is inhabiteddefG (d : RawData) : UnfoldedDiscussion :=
U (F (K (C d))) -- verified iff no sorry in h_ fields
The proof fields h_valid,
h_evidence,
h_subcritical,
h_stable
correspond precisely to the theorems in Chapters 5, 9, 11, and 12.
A paper that passes all four chapter-tests has implicitly constructed
all four proof terms — it is Lean-verifiable in spirit,
even without running #check.
§3 · Type Errors in Academic Arguments
Lean 4 rejects programs with type errors. An argument can also have type errors —
using the wrong kind of evidence for a claim,
regardless of whether the evidence is real.
A randomised controlled trial and a case study both constitute evidence,
but they are different types — and using the wrong type for a causal claim
is a type mismatch.
type mismatch
Evidence type does not match claim type. Correlation evidence for a causal claim.
"X causes Y" supported only by r = 0.6 observational data.
unsolved ?metavariable
A claim that requires an unstated assumption to type-check. The missing piece is not cited.
"Under standard assumptions, X follows from Y." — which assumptions?
failed to synthesize
No evidence exists in the literature that could inhabit this claim's type.
"This is the first demonstration of…" with no novelty check performed.
⊢ type-checks ✓
Claim type matches evidence type. The connection is explicit and warranted.
"RCT (n=200) shows X increases Y by 15% (95% CI 9–21%), p < 0.001."
Theorem 14.1 — The AXLE Verification Criterion
A paper P is AXLE-verified if and only if:
For every claim C in P, there exists an explicit evidence term
h : C constructible from P's data and cited literature,
such that type(h) = required_evidence_type(C).
Equivalently: P is sorry-free — no claim relies on an implicit assumption
that has not been stated as a premise, cited as prior work,
or demonstrated within P.
P passes AXLE iff it also passes the four nirvana tests of Ch13:
T(Conclusion) = Conclusion (Ch12),
ρ(claims) ≤ 1 (Ch11),
λ < 0 (Ch10), and β → ∞ (Ch13).
The AXLE criterion subsumes all four.
§4 · DNA Proofreading — Biological Formal Verification
DNA polymerase III replicates the genome at ~1,000 bases per second
while maintaining extraordinary accuracy.
It achieves this through a three-stage verification cascade —
biological formal verification with error rates that improve by five orders of magnitude.
Verification Stage
Mechanism
Error Rate
Sorry Count (per 10⁹ bases)
Base selection
Geometry / H-bonding specificity
~10⁻⁵
~10,000 sorries
3′→5′ proofreading
Exonuclease removes mismatched 3′ end
~10⁻⁷
~100 sorries
Mismatch repair (MMR)
MutS/MutL/MutH scan for distortions post-replication
~10⁻⁹ to 10⁻¹⁰
~1 sorry per genome
Each stage is an application of the AXLE criterion at the molecular level:
a mismatched base is a type mismatch — the wrong nucleotide type
in a position whose type is defined by the template strand.
The proofreading exonuclease is the reviewer; mismatch repair is AXLE itself.
The Drosophila melanogaster connectome — all ~130,000 neurons
and ~50 million synapses, published in 2023 — represents the same achievement
at the cellular scale: a formal verification of the fly brain's wiring,
every connection typed and checked.
A sorry-free paper aspires to the same completeness in its own domain.
When MMR fails — in Lynch syndrome — the mismatch error rate rises to ~10⁻⁷,
and colorectal cancer risk increases dramatically.
A paper without AXLE verification has the same vulnerability:
every unresolved sorry is a potential site of argument collapse under review pressure.
Each sorry is a claim without evidence.
Click "Add Evidence" to replace it with a real proof term. Reach 0 sorries to verify the paper.
0 / 5 sorries eliminated
⚠ Paper uses 'sorry' — 5 unverified claims
⬡ LLM Prompt Portal · Chapter 14
PROMPT 7.4 · SORRY INVENTORY
Map Every Implicit Assumption in Your Paper
Read your paper as if you were writing it in Lean 4. For every claim C, ask:
"If I had to write h : C, what is h?"
List every claim where h is implicit — where you asserted C without constructing
the evidence term. These are your sorries.
For each sorry: (a) Can it be replaced by a citation? (b) By your own data?
(c) Does it need to be stated explicitly as a premise/assumption?
(d) Should the claim be removed entirely?
Output: a sorry inventory table with columns: Claim / Type of h needed / Replacement strategy / Status.
PROMPT 8.1 · TYPE-CHECK YOUR ARGUMENT
Evidence Type Matching
For each major claim in your paper, identify its required evidence type:
· Causal claim → requires RCT or natural experiment
· Mechanistic claim → requires in vitro / molecular / pathway data
· Associative claim → observational / correlation evidence is sufficient
· Universal claim (∀ x) → requires proof or very large n
· Existential claim (∃ x) → a single example suffices
For each claim, state: (a) claim type, (b) evidence type you used,
(c) type-check result: MATCH ✓ / MISMATCH ✗ / METAVARIABLE ?.
For every MISMATCH: either downgrade the claim to match the evidence,
or upgrade the evidence to match the claim.
EXTENSION · PROOFREADING CASCADE
Three-Stage Verification Protocol
Apply the DNA proofreading cascade to your paper:
Stage 1 — Base selection (error rate 10⁻⁵): Read each sentence in isolation.
Does it make a claim? Is the claim typed correctly?
Flag mismatches.
Stage 2 — Exonuclease proofreading (10⁻⁷): Apply Prompts 5.3 (Lyapunov),
5.2 (spectral), and 6.3 (conclusion audit).
How many sorries remain?
Stage 3 — Mismatch repair (10⁻¹⁰): Apply Prompt 7.3 (nirvana check).
Run the sorry inventory (Prompt 7.4). Eliminate all remaining sorries.
Report error rates at each stage: how many sorry-level claims per 1,000 words
survived Stage 1? Stage 2? Stage 3?