Axioms and proof checking

Inspect which foundational assumptions a theorem’s proof uses.

Start with a concrete example

A board game starts with agreed rules. A proof also rests on explicitly allowed foundational rules. Lean can list the axioms used by a theorem; this differs from assuming the desired conclusion as an extra rule.

A small check: try the idea

Think with the concrete example above. You can try again.

Is assuming the desired conclusion the same as proving it from the stated foundational rules?

Read the answer and reasoning

No. Changing a game’s rules changes the game. Lean’s axiom report helps distinguish the permitted foundations from an extra assumption of the desired theorem.

Build the idea in three steps

A formal proof is checked against rules and any foundational assumptions it uses.
Lean can report the axioms a theorem depends on using #print axioms. A statement in a comment is not an executed check.
The recorded FLT checkpoint lists propext, Classical.choice and Quot.sound. These are foundational axioms, not the assertion that FLT itself is true.

A small example

The owl checks a proof term and its dependencies. It does not check whether the manga’s joke is funny.

Use in Lean · original excerpt

FLT · aa2d8b3 · FinalCheck.lean

4#print axioms fermat_last_theorem

How to read this Lean

This is a diagnostic command from the pinned checkpoint. The site displays the original source; it does not execute the full FLT project.

Original source ↗ · L4–4 Open the complete saved source

Where this idea is used

17. The extremely literal judge

Axioms and proof checking

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Use in Lean · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue