The Curry-Howard Correspondence

Why This Matters

The Curry-Howard correspondence is the single observation that makes dependent-type theorem provers possible. It identifies, structurally, the syntax of intuitionistic logic with the syntax of typed lambda calculus. Under the identification:

• Propositions correspond to types.
• Proofs of a proposition correspond to inhabitants (terms) of the corresponding type.
• Logical connectives correspond to type constructors: conjunction becomes the product type, disjunction becomes the sum type, implication becomes the function type, universal quantification becomes the dependent product, existential becomes the dependent sum.
• Proof composition (modus ponens) corresponds to function application.

Under this view, checking a proof is type-checking a term. Lean's kernel does not need a separate "proof checker": it only has a type checker, applied to the type universe Prop where the propositions live. That economy of mechanism is the reason a few-thousand-line kernel can verify proofs of theorems whose paper version runs to dozens of pages.

The correspondence reaches further. It identifies propositional logic with simply-typed lambda calculus, first-order logic with dependent types, second-order logic with System F, and so on. Lean 4 sits in the dependent-type rung, which is the right level for most mathematics.

The Translation Table

Implication-elimination (modus ponens) is function application: from h : P → Q and hP : P, the term h hP : Q is a proof of $Q$.

And-introduction is pairing: from hP : P and hQ : Q, the term ⟨hP, hQ⟩ : P ∧ Q.

Or-introduction is injection: from hP : P, the term Or.inl hP : P ∨ Q for any Q.

Existence-introduction is also a pair: from a witness a : A and hP : P a, the term ⟨a, hP⟩ : ∃ x, P x.

Why This Is Not a Metaphor

The correspondence is a structural identity in the formal sense: there is a bijection between proofs and terms that preserves the operations on both sides. The bijection is not an analogy; the kernel does not first translate "logical proof" into "typed term" and then check the term. The kernel has only ever dealt with typed terms. Propositions and proofs are objects in the language that the kernel was already designed to type-check.

The consequence: if you can write a term of type P, you have a proof of P, period. Conversely, if P is provable, you can in principle write down the term. The "in principle" carries a complexity caveat: minimum proof length can be very large: but no semantic gap.

Intuitionistic by Default, Classical by Axiom

The correspondence as stated above is for intuitionistic logic. Lean's type theory, like Coq's and Agda's, is intuitionistic by default. The law of excluded middle ($P \lor \neg P$) is not a theorem; you cannot construct a term of this type for arbitrary P.

Two ways to recover classical reasoning:

Decidability. For each P : Prop, an instance of Decidable P provides a term of type P ⊕ ¬ P. Decidability is provable for many specific propositions (equality of natural numbers, comparison of integers, membership in a finite set). Working with decidable propositions, classical-looking reasoning is constructive.

The Classical.choice axiom. Lean ships with three axioms: propositional extensionality, quotient soundness, and Classical.choice. The latter says: for any non-empty type, an inhabitant can be chosen. From Classical.choice plus propext you get Classical.em : ∀ P : Prop, P ∨ ¬ P: the law of excluded middle, derivable but axiomatic.

Mathlib uses classical reasoning extensively (the standard $\epsilon$-$\delta$ definitions, the axiom of choice in topology and measure theory). A proof in Mathlib generally depends on Classical.choice; constructive Mathlib is a smaller fragment. #print axioms shows which axioms a specific theorem uses; see sorry-free discipline and axiom auditing.

Worked Translation: Modus Ponens

Paper statement: "If $P$ implies $Q$ and $P$ holds, then $Q$ holds."

Lean type:

theorem modus_ponens (P Q : Prop) (h : P → Q) (hP : P) : Q := h hP

The proof term is h hP: function application. The kernel checks: h has type P → Q, hP has type P, the result of applying h to hP has type Q. Match.

In tactic mode the same proof is:

theorem modus_ponens (P Q : Prop) (h : P → Q) (hP : P) : Q := by
  exact h hP

The exact tactic accepts a term and uses it directly. Underneath, Lean is doing the same kernel check.

Worked Translation: Conjunction Elimination

Paper statement: "If $P \land Q$ holds, then $P$ holds."

Lean type:

theorem and_left (P Q : Prop) (h : P ∧ Q) : P := h.left

The proof term is h.left: project the first component of the pair. The kernel knows And is defined as a structure with fields left : P and right : Q, so the projection has the right type. In paper math we would write "destructure $h$ as $\langle hP, hQ \rangle$ and return $hP$"; the term h.left is that destructuring, compiled to direct projection.

Common Misconceptions

Exercise

Problem. Translate the paper statement "if $P$ implies $Q$ and $Q$ implies $R$, then $P$ implies $R$" into a Lean type and provide a term-mode proof.

Hint. The proof is function composition.

Solution.

theorem transitivity (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) : P → R :=
  fun hP => hQR (hPQ hP)

Or, using function composition (·):

theorem transitivity (P Q R : Prop) (hPQ : P → Q) (hQR : Q → R) : P → R :=
  hQR ∘ hPQ

The kernel accepts either; the second is a pure-term version that mathematicians may find more natural. The fact that "if-then composition" and "function composition" are the same term is exactly the Curry-Howard correspondence applied here.

Implementation Note

When debugging a stuck proof, #check, #print, and the goal view in VS Code are essential. #check term shows the type. #print term shows the definition. The Lean LSP shows the current proof state at the cursor; reading the displayed goal as a type makes the next tactic choice obvious. If the goal is P → Q, you usually want intro h (introduce the hypothesis, leaving goal Q with new hypothesis h : P). If the goal is P ∧ Q, constructor splits into two subgoals. Each tactic is the term-construction operation read in tactic-mode syntax.

Connection to TheoremPath

Every theorem in the FormalSLT manifest corresponds, under Curry-Howard, to a kernel-checked term of the appropriate Lean type. The manifest lists, for each theorem, the file, the type signature, the term name, and the axioms the term depends on. The trust story is: the kernel saw the term, the kernel type-checked the term, the term has the declared type, therefore the proposition is provable. No other "proof check" happens.

Cross-references: /methodology explains why the kernel-check is the right notion of "verified", and /evidence lists the specific Mathlib commit and toolchain pin.