Proof assistants: a reading guide¶

Level: reference · for anyone who has run this library's model checks and asks what a proof would add, for the owner's "at this level Python is useless, we need Lean", and for placing Paulson's Isabelle's Logics: FOL and ZF

One line: A proof assistant checks a proof the way this library's programs check a model, step by step and by shape, with no idea what the symbols mean; the price is that every step must be written down, and the prize is a theorem about all sets instead of the sets in V₄, so play with sets in Python, prove about them in Lean or Isabelle, and read Paulson's manual for the axioms as a machine states them.

Every other page in this library is a lesson: one idea, backed by a program. This page is a reading guide, and what it says about the systems and the manual is opinion, except the program, which is a working proof checker for the propositional part of Isabelle's logic with Isabelle's own rule names. The Lean and Isabelle declarations quoted here were read in the systems' source files, and the manual in its LaTeX source in Isabelle's repository, which is what the owner's PDF is generated from (its title page is dated January 18, 2026, the date of the build, not of the text; the manual is rebuilt with every Isabelle release). Everything else is from memory and says so.

What a proof assistant does¶

A model checker, which is what every program in the axioms chapter is, takes a universe and a sentence and computes whether the sentence is true there: it loops over the points. A proof assistant takes a proof and computes whether it is one: it loops over the lines. A proof is a list of lines, each saying what is assumed, what is claimed, which rule produced it and which earlier lines it cites, and the checker verifies that each line has the shape its rule demands, and nothing else. It does not know what ∧ means; it knows that conjI turns a line P and a line Q into a line P ∧ Q. That is the whole idea, and the program on this page is one (section 1), with the thirteen rules printed as Isabelle's IFOL.thy and FOL.thy state them.

Three consequences follow, and the program shows each:

The checker checks shape, not truth (section 2). A proof with one line claiming too much is rejected at that line. The slip a human reader misses, an assumption discharged that was never there, is caught by bookkeeping: line 4 rests on A ∧ B, so line 5 may not pretend it rested on A.
Which logic you are in is a matter of which rules exist (section 3). Isabelle's IFOL is intuitionistic: its rules are the introduction and elimination rules of Gentzen's natural deduction, and from them A ∨ ¬A cannot be reached. FOL adds one axiom, classical: (¬P ⟹ P) ⟹ P, and the excluded middle takes seven lines with that one step marked.
A proof covers every model; a model check covers one (section 4). Pow(A ∩ B) = Pow(A) ∩ Pow(B) is checked here on all 64 pairs of subsets of {1, 2, 3}, and proved in Paulson's manual in eleven steps for all sets whatever. The false law Pow(A ∪ B) = Pow(A) ∪ Pow(B) is the other direction: a counterexample is a finite object, {1} and {2}, and a model finder is the tool that finds one; a proof assistant only fails to prove it, which is not the same thing.

What makes this trustworthy is how little is trusted. In Isabelle, a theorem is a value of an abstract type that only the kernel's rules can produce (the LCF design, from Milner's Edinburgh LCF of the 1970s), so the search procedures (blast, auto, simp, Sledgehammer) may be as clever and as buggy as they like: whatever they find still passes through the rules. Lean and Rocq keep a proof term that a small kernel re-checks, and independent re-checkers exist for Lean's. Metamath has no logic built in at all: its verifier, a few hundred lines in any language, checks that every step is a substitution into an earlier statement, and set.mm supplies the ZFC axioms and everything after. The checker on this page knows 13 rules in about a hundred lines; the systems differ from it in size, not in kind. (Sizes from memory.)

What the program prints¶

Verified output of proof_assistants.py — regenerated by tools/run_examples.py, never hand-typed.

1. THE RULES, AS ISABELLE STATES THEM, AND A PROOF THEY ACCEPT
   ⟹ is Isabelle's 'from these, this'; ⟦P; Q⟧ lists what is needed.
     assume     P ⟹ P                           an assumption may be claimed
     conjI      ⟦P; Q⟧ ⟹ P ∧ Q
     conjunct1  P ∧ Q ⟹ P
     conjunct2  P ∧ Q ⟹ Q
     disjI1     P ⟹ P ∨ Q
     disjI2     Q ⟹ P ∨ Q
     disjE      ⟦P ∨ Q; P ⟹ R; Q ⟹ R⟧ ⟹ R
     impI       (P ⟹ Q) ⟹ P ⟶ Q
     mp         ⟦P ⟶ Q; P⟧ ⟹ Q
     FalseE     False ⟹ P
     notI       (P ⟹ False) ⟹ ¬P              derived: ¬P abbreviates P ⟶ False
     notE       ⟦¬P; P⟧ ⟹ R                    derived
     classical  (¬P ⟹ P) ⟹ P                  the one axiom FOL adds to IFOL
   A proof is a list of lines: assumptions ⊢ claim, the rule, the lines it cites.
   Claim: A ∧ B ⟶ B ∧ A.
    1. A ∧ B ⊢ A ∧ B                      by assume
    2. A ∧ B ⊢ B                          by conjunct2 [1]
    3. A ∧ B ⊢ A                          by conjunct1 [1]
    4. A ∧ B ⊢ B ∧ A                      by conjI [2, 3]
    5. ⊢ A ∧ B ⟶ B ∧ A                    by impI [4]
   accepted: every line has the shape its rule demands

2. THE CHECKER CHECKS SHAPE, NOT TRUTH: TWO DOCTORED PROOFS
   The same proof with line 4 claiming B ∧ A straight from line 1:
    1. A ∧ B ⊢ A ∧ B                      by assume
    2. A ∧ B ⊢ B                          by conjunct2 [1]
    3. A ∧ B ⊢ A                          by conjunct1 [1]
    4. A ∧ B ⊢ B ∧ A                      by conjunct1 [1]
       REJECTED: conjunct1 of A ∧ B is A
   And with line 5 discharging an assumption line 4 never had:
    1. A ∧ B ⊢ A ∧ B                      by assume
    2. A ∧ B ⊢ B                          by conjunct2 [1]
    3. A ∧ B ⊢ A                          by conjunct1 [1]
    4. A ∧ B ⊢ B ∧ A                      by conjI [2, 3]
    5. ⊢ A ⟶ B ∧ A                        by impI [4]
       REJECTED: a premise rests on an assumption the conclusion does not carry
   The second is the slip a human reader misses: the conclusion is false
   (A alone does not give B ∧ A), and only the bookkeeping of assumptions
   catches it. The checker never evaluated a single formula.

3. THE EXCLUDED MIDDLE, WITH THE ONE CLASSICAL STEP MARKED
   Claim: A ∨ ¬A. IFOL has no rule that reaches it; FOL adds 'classical'.
    1. A, ¬(A ∨ ¬A) ⊢ A                   by assume
    2. A, ¬(A ∨ ¬A) ⊢ A ∨ ¬A              by disjI1 [1]
    3. A, ¬(A ∨ ¬A) ⊢ ¬(A ∨ ¬A)           by assume
    4. A, ¬(A ∨ ¬A) ⊢ False               by notE [3, 2]
    5. ¬(A ∨ ¬A) ⊢ ¬A                     by notI [4]
    6. ¬(A ∨ ¬A) ⊢ A ∨ ¬A                 by disjI2 [5]
    7. ⊢ A ∨ ¬A                           by classical [6]
   accepted: every line has the shape its rule demands
   Lines 1 to 6 are intuitionistic: from ¬(A ∨ ¬A) they reach A ∨ ¬A.
   Line 7 is the step (¬P ⟹ P) ⟹ P, which drops the assumption; without
   it the proof stops at line 6 with ¬(A ∨ ¬A) still on the left of ⊢.

4. A MODEL CHECK AND A PROOF OF THE SAME THEOREM
   Pow(A ∩ B) = Pow(A) ∩ Pow(B) on every pair A, B ⊆ {1, 2, 3}: 64 pairs, 64 true
   Pow(A ∪ B) = Pow(A) ∪ Pow(B): 64 pairs, 18 false; the smallest
   counterexample is A = {1}, B = {2}: {1, 2} ⊆ A ∪ B but ⊆ neither.
   That is what this library's programs do, and a counterexample is a finite
   object, so it is the right tool to find one. Paulson's manual proves the
   first law for all sets, in the proof of its section 'A proof about powersets':
     lemma "Pow(A Int B) = Pow(A) Int Pow(B)"     
     apply (rule equalityI)                       two inclusions, by extensionality
     apply (rule Int_greatest)                    ⊆ of an intersection: ⊆ of each part
     apply (rule Int_lower1 [THEN Pow_mono])      A ∩ B ⊆ A, and Pow is monotone
     apply (rule Int_lower2 [THEN Pow_mono])      A ∩ B ⊆ B, likewise
     apply (rule subsetI)                         the other inclusion, member by member
     apply (erule IntE)                           x ∈ Pow(A) ∩ Pow(B) is two facts
     apply (rule PowI)                            x ∈ Pow(A ∩ B) is x ⊆ A ∩ B
     apply (drule PowD)+                          and the two facts are x ⊆ A, x ⊆ B
     apply (rule Int_greatest)                    so x ⊆ A ∩ B
     apply (assumption+)                          the two subgoals are assumptions
     done                                         
   Eleven steps, each a rule applied by shape, as in sections 1 to 3; the
   manual adds that 'by blast' finds this proof by itself. 64 pairs here,
   every set there. The checker above knows 13 rules; Isabelle/ZF's
   difference is only size: more rules, quantifiers, and the seven axioms.

Isabelle/ZF: the axioms as the machine reads them¶

Isabelle is a logical framework: its core, Pure, has only ⟹ (from these, this), ⋀ (for all, at the level of rules) and ≡, and each object logic is a theory on top. FOL is classical first-order logic, built as IFOL plus classical, and ZF is FOL plus the constants ∈, 0, Pow, ⋃, Inf and PrimReplace and six axioms. They are stated in Isabelle's ZF_Base.thy, read for this page, and this is the table to hold beside the chapter's pages. Variables range over sets (type i), formulas have type o, and a class is a predicate, as the manual's section "Which version of axiomatic set theory?" explains when it chooses ZF over Bernays–Gödel.

This library's page	Isabelle/ZF, in `ZF_Base.thy`	Remark
Extensionality	`extension: A = B ⟷ A ⊆ B ∧ B ⊆ A`	with ⊆ defined as ∀x∈A. x∈B
Pairs	not an axiom: `Upair(a,b) ≡ {y . x∈Pow(Pow(0)), (x=0 ∧ y=a) ∨ (x=Pow(0) ∧ y=b)}`	a theorem: replacement over the two-member set 𝒫(𝒫(∅)); the pairs page now runs it
Unions	`Union_iff: A ∈ ⋃(C) ⟷ (∃B∈C. A∈B)`
Power set	`Pow_iff: A ∈ Pow(B) ⟷ A ⊆ B`
Comprehension	not an axiom: `Collect(A,P) ≡ {y . x∈A, x=y ∧ P(x)}`	separation is a theorem of replacement, as the replacement page says
Replacement	`replacement: (∀x∈A. ∀y z. P(x,y) ∧ P(x,z) ⟶ y = z) ⟹ b ∈ PrimReplace(A,P) ⟷ (∃x∈A. P(x,b))`	one axiom, not a scheme: P is a variable of the framework, which is why the manual says Isabelle "has no difficulty with axiom schemes"
Infinity	`infinity: 0 ∈ Inf ∧ (∀y∈Inf. succ(y) ∈ Inf)`	a set is named, Inf, though it is not unique; ω is carved out of it later
Foundation	`foundation: A = 0 ∨ (∃x∈A. ∀y∈x. y∉A)`	the ∈-minimal member, as on the page
Choice	not in `ZF_Base`; the theory `AC.thy` adds `AC: ⟦a ∈ A; ⋀x. x ∈ A ⟹ (∃y. y ∈ B(x))⟧ ⟹ ∃z. z ∈ Pi(A,B)`	a choice function as a member of the product `Pi(A,B)`: the chapter's "product of nonempty sets" form, read in `AC.thy`
the empty set	`0`, a primitive constant	Cunningham's axiom, Kunen's Axiom 0 and Cori and Lascar's derivation are the chapter page's three ways; Isabelle takes a fourth, a constant that the other axioms pin down

So the count is six axioms and a constant, with pairing and separation derived, which the manual credits to Suppes. The chapter page now carries an Isabelle/ZF column in its notation table, and so does the glossary's symbol table.

Paulson's manual, placed¶

Isabelle's Logics: FOL and ZF, by Lawrence C. Paulson with contributions by Tobias Nipkow and Markus Wenzel, is the reference manual for these two object logics. Its own abstract says what it is: part of the older Isabelle documentation, "somewhat superseded" by the Isabelle/HOL tutorial, but "the only available documentation for Isabelle's versions of first-order logic and set theory", rewritten for the Isar proof language with "evidence of the old ML orientation" remaining. It is not a textbook of set theory and does not pretend to be: it cites Halmos and Suppes for that.

Part	What it holds	Read it?
Syntax definitions	how the manual writes grammars	skip
First-Order Logic	the syntax of `FOL`, the rules with their names (the figure the program's section 1 copies), the intuitionistic and classical proof procedures, three worked examples	the rules figure and the classical example, after the program
Zermelo–Fraenkel Set Theory: "Which version", "The syntax", "Binding operators", "The axioms"	ZF against Bernays–Gödel, the constants table (`Pow`, `Union`, `Collect`, `Replace`, `Pi`, `Sigma`, `Lambda`, …), the axioms figure	yes: the four sections that match the chapter, in that order
ZF: "From basic lemmas to function spaces", "Further developments"	the derived rules for ⊆, ∪, ∩, pairs, relations, functions, `Pi` and `Sigma`, and the lemmas each has	as a dictionary, when a rule name turns up
ZF: "Automatic tools", "Natural number and integer arithmetic", "Datatype definitions", "Inductive and coinductive definitions"	what Isabelle/ZF builds on the axioms: ℕ and ℤ, lists and trees as sets, inductive definitions, codatatypes	only with Isabelle installed
ZF: "The outer reaches of set theory"	ordinals, cardinals, the axiom of choice and its equivalents, Paulson's constructible universe	the pages that match the chapter's ordinals and choice
ZF: the three worked proofs	powersets (section 4 of the program), monotonicity of ⋃, low-level reasoning about functions	yes, all three; they are the manual's best pages
ZF with Isar	the same material in the structured proof language	after the worked proofs

Verdict. For a reader of this library the manual is worth four sections and three examples, about thirty pages, and the rest is a dictionary. Its value is that it is the one place where the axioms, the derived rules and a real proof sit together in the exact notation a machine checks. Its difficulty is not the mathematics but the tactic vocabulary (rule, erule, drule, THEN, blast), which the FOL chapter introduces and which no page here replaces; the program's section 4 glosses each tactic of the powerset proof in words, and that is as far as this library goes without installing Isabelle.

Anything new for the sets pages? The owner asked, having downloaded the manual. One thing, now done: pairing is a theorem of replacement over 𝒫(𝒫(∅)), which the pairs page now runs in its section 7. Two things the chapter already has in other words: foundation as the ∈-minimal member and infinity as a named inductive set. Two things left in the inbox, because each needs a page of its own: Sigma(A,B) and Pi(A,B), the dependent product and function space, which generalise the Cartesian product to a family of second sets; and inductive definitions, lists and trees built as sets. The rest is Isabelle, not set theory.

Which language to play with sets? Python, Rust, Lean, Isabelle¶

The owner asked whether Rust has a mathematics library, how it does set operations, and which of Lean and Isabelle is the best language to play with sets. The honest split is between playing, which means computing with finite sets and trying things, and proving.

	Sets	∪ ∩ ∖ △ ⊆ ∈	𝒫(a)	Sets of sets	Plays?	Proves?
Python	`set`, `frozenset`	`\\|`, `&`, `-`, `^`, `<=`, `in`, with the precedence on reading a set expression	a loop over `itertools.combinations`, as every page here does	only a `frozenset` can be a member	yes, with the least ceremony: every program here	no
Rust	`HashSet`, `BTreeSet` in `std::collections`	the methods `union`, `intersection`, `difference`, `symmetric_difference` return iterators; `is_subset`, `is_superset`, `is_disjoint`, `contains`; and `&a \\| &b`, `&a & &b`, `&a - &b`, `&a ^ &b` on references build a new set, with C's precedence, the same ladder as Python's	not in the standard library; `powerset` in the `itertools` crate	`BTreeSet<BTreeSet<T>>` works, because a `BTreeSet` is ordered and hashable; `HashSet<HashSet<T>>` does not, because a `HashSet` is not hashable: Rust's version of `set` against `frozenset`	yes, with the types satisfied first; a `BTreeSet` prints in order, a `HashSet` in a different order each run	no
Lean 4 with Mathlib	`Finset α`, computable and finite, and `Set α`, a predicate `α → Prop`	`∪ ∩ \ ⊆ ∈`, with `\` level with `∩` as the precedence page found; `∆` for symmetric difference	`Finset.powerset`, `Set.powerset`	yes	`#eval` on a `Finset` computes, in the browser with Mathlib loaded	yes: the system most mathematicians now learn, with the Natural Number Game as the first day
Isabelle/HOL	`'a set`, a type for each element type	`∪ ∩ - ⊆ ∈`, with `-` level with `∪` as the precedence page found	`Pow`	yes	`value` evaluates a finite set expression (from memory)	yes: the notation closest to the books, and Sledgehammer, which calls automatic provers and reports which lemmas they used
Isabelle/ZF	one type `i` of untyped sets, as in the books	`Un`, `Int`, `-`, `<=`, `:` in ASCII, the symbols in the editor	`Pow`	yes, that is the point: 0, {0}, {0, {0}} are its natural numbers	no evaluation; it only proves	yes: the ZF axioms themselves, with Paulson's manual
Metamath (set.mm)	ZFC formulas, no types	the symbols of the chapter's pages, in ASCII	`~P`	yes	no	yes, by substitution alone; the proof of 2 + 2 = 4 from the axioms is famous

Rust has no mathematics library in its standard library beyond the methods on f64 and on the integer types; the crates num (big integers, rationals, complex numbers), nalgebra and ndarray (linear algebra) and itertools (combinations, power sets) fill the gap. Crate names from memory; the HashSet and BTreeSet methods and operators are from memory of the standard library's documentation, which this session could not fetch.

Verdict. Lean and Isabelle are not languages to play with sets, and neither is Rust, though all three can compute with finite ones: Python is, which is why this library is in Python. To prove things about sets, Lean 4 if you want the on-ramp (the Natural Number Game, then Mathematics in Lean) and the largest community, remembering that its foundation is type theory, with ZFC's universe available inside it as a type, so "a set" there is a predicate on a type; Isabelle/HOL if you want the books' notation and the strongest automation; Isabelle/ZF or Metamath if the point is to see the ZF axioms of the chapter run with nothing added. "At this level Python is useless, we need Lean" is half right, in the way the set theory guide says: Python checks a model, Lean proves a theorem, and section 4 shows each doing the thing the other cannot.

Where to start¶

Truth tables and the laws of logic and predicates and quantifiers, then reading a formula: the object language.
The program on this page: thirteen rules, three proofs, two rejections. Write a fourth proof, A ⟶ B ⟶ A or De Morgan's ¬(A ∨ B) ⟶ ¬A ∧ ¬B, as a list of lines and run check on it; then break it and watch which line fails.
Lean's Natural Number Game, in the browser, no installation: induction and rewriting as a game, with Lean's real tactics. For Lean itself, its books and its definitions run as a program, the Lean reading guide.
Paulson's manual, the four ZF sections and the three worked proofs, with the table above beside the chapter's pages.
Then one of: Mathematics in Lean (Avigad and Massot, free) for Lean; Concrete Semantics (Nipkow and Klein, free) or its first part, Programming and Proving in Isabelle/HOL, for Isabelle; the Metamath book (Megill) for set.mm. Titles from memory.

Flashcards¶

The page as a deck of Anki cards: proof_assistants.txt, thirteen cards on what a checker does, Isabelle's rules and axioms, the manual, and which language for what. Tags: proof_assistant, isabelle, languages.

Po polsku, w skrócie¶

Asystent dowodzenia (proof assistant) to program, który sprawdza dowód tak, jak programy tej biblioteki sprawdzają model: krok po kroku, po kształcie, nie wiedząc, co znaczą symbole. Dowód to lista wierszy; każdy mówi, co zakłada, co twierdzi, z jakiej reguły i z których wcześniejszych wierszy. Program na tej stronie jest takim sprawdzaczem dla rachunku zdań, z nazwami reguł Isabelle (conjI, impI, mp, classical…): przyjmuje poprawny dowód, odrzuca dwa sfałszowane we właściwym wierszu, dowodzi prawa wyłączonego środka z jednym krokiem klasycznym, a potem stawia obok siebie sprawdzenie modelu (64 pary zbiorów) i dowód Paulsona (11 kroków, wszystkie zbiory) tego samego twierdzenia Pow(A ∩ B) = Pow(A) ∩ Pow(B). Kontrprzykład jest skończony, więc znajduje go sprawdzanie modelu; twierdzenie o wszystkich zbiorach daje tylko dowód.

Podręcznik Paulsona Isabelle's Logics: FOL and ZF to instrukcja, nie podręcznik teorii mnogości: warto przeczytać cztery sekcje o ZF (która wersja, składnia, kwantyfikatory, aksjomaty) i trzy przykładowe dowody; reszta to słownik reguł. Tabela wyżej zestawia aksjomaty rozdziału z ich zapisem w Isabelle: para i wyróżnianie nie są tam aksjomatami, lecz twierdzeniami z zastępowania. Do zabawy ze zbiorami najlepszy jest Python (Rust też ma zbiory, HashSet i BTreeSet, z tymi samymi operatorami co Python, ale bez biblioteki matematycznej w standardzie); do dowodzenia Lean 4 (najłatwiejsze wejście, gra Natural Number Game) albo Isabelle/HOL (notacja jak w książkach, najlepsza automatyzacja); do zobaczenia samych aksjomatów ZF Isabelle/ZF albo Metamath.

Auf Deutsch: Stichwörter¶

Beweisassistenten: ein Prüfer für natürliches Schließen mit Isabelles Regelnamen, Modellprüfung gegen Beweis, die ZF-Axiome wie Isabelle/ZF sie formuliert, Paulsons Handbuch eingeordnet.

Stichwörter: Beweisassistent, Isabelle, Lean, natürliches Schließen, Schlussregel (conjI, impI, mp), Modellprüfung, Axiom, formaler Beweis, Typtheorie vs. Mengenlehre.

Run it yourself¶

From the root of your clone of this repository:

python3 reading_guides/proof_assistants/examples/proof_assistants.py