Sorry-Free Discipline and Axiom Auditing in Lean 4

Why This Matters

A Lean 4 codebase claims its theorems are "kernel-checked." The claim is meaningful only if two operational disciplines are enforced:

1. No sorry. Lean accepts the keyword sorry as a placeholder term of any type. Lean will type-check a file that contains sorry. The file appears to compile, the lean command exits cleanly, and any downstream code that imports the file is type-correct under the assumption that the sorry-marked theorem holds. If sorry is anywhere in your codebase, the kernel-check claim has a hole.

2. Audit the axioms. Lean ships with three primitive axioms: propext, Classical.choice, Quot.sound. Mathlib uses these freely. Any additional axiom: anything declared axiom foo : T := ... in a file you imported: is a new article of faith. #print axioms reports exactly what a given theorem depends on. CI should gate on the expected list.

This page covers the operational machinery: how to grep for sorry, how to audit axioms automatically, what the standard axioms mean, and what the FormalSLT project at TheoremPath enforces.

The sorry Problem

theorem riemann_hypothesis : ∀ s : ℂ, ZetaFunction.zeros s → s.re = 1/2 := sorry

This file type-checks. The lean command exits with status 0. Anything that imports this file has access to riemann_hypothesis as if it were proved. The theorem is not proved; the term sorry is a placeholder of arbitrary type. Lean emits a warning to stderr:

warning: declaration uses 'sorry'

But the warning does not block compilation. A production-quality project needs CI that converts the warning into a build failure.

The Mathlib4 CI does this with a grep gate:

if grep -rn "^[^/-]*\bsorry\b" Mathlib/ --include="*.lean" \
   | grep -v "^Mathlib/Tactic/Sorry" \
   | grep -v -- "-- sorry" ; then
  echo "Found sorry in Mathlib"; exit 1
fi

The grep matches the keyword sorry outside of comments, excluding the Sorry tactic file itself (which legitimately mentions the name). If any match, CI fails.

A weaker version that suffices for small projects:

if grep -rn "^\s*sorry\b\|:= sorry\b" Mathlib/ --include="*.lean" ; then
  exit 1
fi

The grep gate is necessary but not sufficient: it does not catch axioms or unsafe declarations. Both need separate checks.

The Three Standard Axioms

Lean 4's type theory is intuitionistic but admits three classical axioms:

propext : ∀ {p q : Prop}, (p ↔ q) → p = q: propositional extensionality. Two propositions that are logically equivalent are equal as propositions. This is the bridge that lets you rw with a biconditional and treat propositions as data.

Classical.choice : ∀ {α : Sort u}, Nonempty α → α: for any non-empty type, an inhabitant can be produced. From this plus propext you derive the law of excluded middle (Classical.em), decidability of arbitrary propositions, and the standard $\epsilon$-$\delta$ analysis machinery. Mathlib uses Classical.choice extensively.

Quot.sound : ∀ {α : Sort u} {r : α → α → Prop} {a b : α}, r a b → Quot.mk r a = Quot.mk r b: quotient soundness. If two elements are related by r, then their images in the quotient α / r are equal. The technical foundation for setoids and quotient types.

These three are the only axioms Lean ships with. Every other "axiom" in Mathlib is either (a) a definition that introduces no axiom, (b) a theorem provable from the three, or (c) a Decidable instance certifying that a particular proposition's truth value can be computed.

A proof that depends only on [propext, Classical.choice, Quot.sound] is what the Lean community considers "fully classical, fully verified." A proof that depends only on [propext, Quot.sound] (no choice) is constructive. A proof that depends on a longer list has a custom axiom and needs justification.

#print axioms and the CI Gate

The #print axioms command lists every axiom that a specific theorem depends on, transitively:

#print axioms add_comm
-- 'add_comm' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms sqrt_two_irrational
-- 'sqrt_two_irrational' depends on axioms: [propext, Classical.choice, Quot.sound]

#print axioms my_attempted_theorem
-- 'my_attempted_theorem' depends on axioms: [propext, Classical.choice, Quot.sound, sorryAx]
-- The 'sorryAx' is the marker for 'sorry' usage.

In a project, you grep the build output for the expected axiom list. The FormalSLT pattern:

-- File: verification/lean/Audit.lean
import TheoremPath.Hoeffding.OneSidedFiniteSum
import TheoremPath.Massart.FiniteClass
-- ... (all top-level theorems)

#print axioms Hoeffding.oneSidedFiniteSum
#print axioms Massart.finiteClass
-- ... (one #print line per theorem)

A CI step builds this file and checks each line. If any theorem reports an axiom outside [propext, Classical.choice, Quot.sound], the build fails:

lake build TheoremPath.Audit 2>&1 | \
  awk '/depends on axioms:/ {
    if ($0 !~ /\[propext, Classical.choice, Quot.sound\]/) {
      print "non-standard axiom in:", $0; exit 1
    }
  }'

This is the operational machinery that turns "kernel-checked" from a claim into a checked fact.

The sorryAx Mechanism

Internally, sorry is not a special form. It is a term of type ? (any type) whose elaborator inserts sorryAx: an axiom. When the kernel type-checks sorry, it consults the axiom list and finds sorryAx : ∀ α : Sort u, α. The check succeeds (because the axiom guarantees a term of any type), and the proof is "complete."

The sorryAx axiom is unsoundness in disguise: it lets you produce a proof of False. The reason Lean ships with it is convenience during proof development. You can stub out parts of a long proof with sorry, build the file, see the proof skeleton compile, and fill in the holes later. The discipline is to never ship a file with sorry in it.

#print axioms reports sorryAx explicitly, which is why the CI gate works. Stripping sorry from the codebase is equivalent to ensuring sorryAx does not appear in any reported axiom list.

Other Axiom Hazards

Custom axioms. A file may declare axiom my_axiom : .... Any theorem that uses my_axiom lists it via #print axioms. CI catches it as a non-standard axiom.

unsafe declarations. Lean has an unsafe keyword for declarations that bypass the kernel's termination check. unsafe def collatz_iterate (n : Nat) : Nat := ... is allowed but cannot be used in proofs. A CI grep grep "^unsafe " Mathlib/ catches these.

partial definitions. partial def declarations are not unfolded by the kernel. They produce opaque values; you can prove facts about a partial def but cannot compute with it inside the kernel. Less dangerous than unsafe but worth flagging.

Implementation details (opaque). An opaque def blocks the kernel from unfolding the definition. Not unsoundness, but it can hide a sorry. The Mathlib.Lemmas.LemmaNameSpace files use opaque for performance; FormalSLT avoids it in proof-bearing definitions.

The robust audit policy: greg for sorry, unsafe, custom axiom declarations, and run #print axioms on every theorem.

The FormalSLT Standard

The TheoremPath FormalSLT project (manifest at /lean) enforces the following on every kernel-checked theorem:

1. No sorry anywhere in verification/lean/. CI greps and fails.
2. #print axioms reports exactly [propext, Classical.choice, Quot.sound] for every theorem in the manifest. CI parses the build output and fails on deviations.
3. Mathlib version pin. The lean-toolchain and lakefile.lean pin Mathlib to a specific commit hash. Updating the pin requires re-running the entire suite. CI fails if the pin moves without manifest revalidation.
4. No opaque def in proof-bearing files. Reserved for performance-tuning of definitions; not used in lemma bodies.

A theorem that does not pass all four checks is not listed in the manifest. The current manifest has 56 entries (as of May 2026), each kernel-checked, axiom-audited, and pinned.

The methodology is documented at /methodology and the per-theorem audit trail (build status, axiom list, file location) at /evidence.

Worked Example: A sorry-Caught Proof

theorem hopefully_true (n : Nat) : n^2 + 1 ≠ 0 := by
  intro h
  -- I want to show n^2 + 1 ≥ 1, but I am going to be lazy:
  sorry

Lean accepts this file. lake build succeeds. The theorem hopefully_true is now usable in downstream code.

Run #print axioms hopefully_true:

'hopefully_true' depends on axioms: [sorryAx]

The audit fails. The fix is to replace sorry with a real proof:

theorem hopefully_true (n : Nat) : n^2 + 1 ≠ 0 := by
  intro h
  have h1 : n^2 + 1 ≥ 1 := Nat.succ_le_succ (Nat.zero_le _)
  omega

Run #print axioms hopefully_true again:

'hopefully_true' depends on axioms: [propext, Classical.choice, Quot.sound]

Now the audit passes. The theorem is kernel-checked under the standard axioms.

Common Misconceptions

Exercise

Problem. Set up a minimal Lean 4 project with one theorem and CI configured to: (a) fail on sorry, (b) fail on any axiom outside [propext, Classical.choice, Quot.sound].

Sketch the CI script.

Hint. The CI runs lake build, then lean Audit.lean against a separate file containing #print axioms calls, then greps the build output.

Solution.

Minimal .github/workflows/lean-audit.yml:

name: Lean audit
on: [push, pull_request]
jobs:
  audit:
    runs-on: ubuntu-latest
    steps:
      - uses: actions/checkout@v4
      - uses: leanprover/lean-action@v1
      - name: Build
        run: lake build
      - name: No sorry
        run: |
          if grep -rn "\bsorry\b" --include="*.lean" . | grep -v "^./Mathlib/Tactic/Sorry"; then
            echo "Found sorry"; exit 1
          fi
      - name: Standard axioms only
        run: |
          lake build Audit 2>&1 | awk '
            /depends on axioms:/ {
              if ($0 !~ /\[propext, Classical\.choice, Quot\.sound\]/) {
                print "Non-standard axiom: " $0; exit 1
              }
            }
          '

The Audit.lean file lists #print axioms for every top-level theorem you want to certify. The build step prints the axiom dependency for each; the awk filter fails on any deviation from the standard list. Two checks (grep for sorry, awk for axioms) are sufficient for a small project; large projects (Mathlib4-scale) layer additional checks for unsafe, partial, and opaque.

Implementation Note

For day-to-day Lean development, the recommended workflow:

1. Write a theorem skeleton with := sorry.
2. Run the file in VS Code; observe the goal display.
3. Write tactics to discharge the goal incrementally.
4. When the goal is closed, remove sorry.
5. Before committing, run #print axioms my_theorem in the file and confirm only the three standard axioms.
6. Push. CI catches any regression.

In production-quality projects (FormalSLT, Mathlib4), the gate happens automatically. In personal projects, build the habit of running #print axioms before committing.

For a one-off check from the CLI:

echo "#print axioms Hoeffding.oneSidedFiniteSum" | lean --run - \
  --root=verification/lean \
  --imports="TheoremPath.Hoeffding.OneSidedFiniteSum"

Returns the axiom list to stdout; exit code 0 means the kernel accepted the theorem.

Connection to TheoremPath

Every theorem in the FormalSLT manifest has been built, kernel-checked, and axiom-audited under the FormalSLT discipline described above. The manifest column "Axioms" reports the dependency list; deviations from the standard three are flagged in red. The CI configuration at .github/workflows/lean-verification.yml is the operational realization of this page.

See /methodology for the rationale behind kernel-checking, and /evidence for the per-theorem audit trail showing build hash, Mathlib commit, and axiom list.