proof assistants for mathematics

Freek Wiedijk Radboud University, Nijmegen Free University, Amsterdam

OzsL Schoolweek Hotel Dennenhoeve, Nunspeet 2004 12 02, 15:30

intro

the best of two worlds formalizing proofs is like

• programming but no bugs, and not trivial

• doing mathematics

but transparent, and the computer helps (currently closer to programming than to doing mathematics)

a wonderful computer game!

systems

mathematics in the computer

• numerical calculations numbers: computer → human

• computer algebra calculations formulas: computer → human

• automated theorem provers proofs: computer → human

• proof assistants

proofs: human → computer (computer just checks whether the proof is correct) the two kinds of computer proof

• correctness of computer software and hardware (serious branch of computer science: ‘formal methods’)

statements: big proofs: shallow computer does the main part of the proof

• correctness of mathematical theorems (slow and thorough style of doing mathematics, still in its infancy)

statements: small proofs: deep human does the main part of the proof prehistory

1968 Automath

Netherlands, de Bruijn

1971 nqthm

US, Boyer & Moore

1972 LCF

UK, Milner

1973 Mizar

Poland, Trybulec the seven provers of the world

[figure: Mizar; most mathematical; LCF; HOL; Isabelle; most pure; Automath; Coq NuPRL; most logical; PVS; most popular; nqthm; ACL2; most computational]

foundations

• primitive recursive arithmetic ACL2

• type theory typed lambda calculus + inductive types, constructive Coq, NuPRL

• higher order logic typed lambda calculus + choice operator, classical HOL, Isabelle, PVS

• set theory Mizar procedural versus declarative

0  ∞

• procedural

E E S E N E S S S W W W S E E E

HOL, PVS, Coq, NuPRL

• declarative

(0,0) (1,0) (2,0) (3,0) (3,1) (2,1) (1,1) (0,1) (0,2) (0,3) (0,4) (1,4) (1,3) (2,3) (2,4) (3,4) (4,4)

Mizar, Isabelle the best prover of the world?

8

the example

a small proof

Theorem. There are irrational numbers x and y such that x^{y} is rational.

Proof. We have the following calculation

(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2}·\sqrt{2}} = \sqrt{2}^{2} = 2

which is rational. Furthermore Pythagoras showed that \sqrt{2} is irrational. Now there are two cases:

• Either \sqrt{2}^{\sqrt{2}} is rational. Then take x = y = \sqrt{2}.

• Or \sqrt{2}^{\sqrt{2}} is irrational. In that case take x = \sqrt{2}^{\sqrt{2}} and y = \sqrt{2}. And by the above calculation then x^{y} = 2, which is rational. □

HOL proof

the Pentium bug Pentium: Intel processor mid 1994: processor makes errors FDIV bug, not enough precision \frac{5505001}{294911} = 18.66665197… (mathematics) \frac{5505001}{294911} = 18.66600093… (Pentium) Intel: processor that has bug will be replaced for free estimated damage: 475 million dollars John Harrison and HOL Light

John Harrison: reimplementation of the HOL system

LCF → HOL → HOL Light

PhD in Cambridge, UK formalization of mathematics

e.g. fundamental theorems of calculus & algebra

Flyspeck project

currently works at Intel verification of the real thing

floating point algorithms in the actual Intel chips the proof: in the file

one bead on the necklace

let EXAMPLE = prove
(`?x y. ~rational x /\ ~rational y /\ rational(x^y)`,
ASM_CASES_TAC `rational(sqrt(&2)^sqrt(&2))` THENL
 [EXISTS_TAC `sqrt(&2)`; EXISTS_TAC `sqrt(&2)^sqrt(&2)`] THEN
EXISTS_TAC `sqrt(&2)` THEN
ASM_SIMP_TAC[SQRT_POW_2; GSYM REAL_POW_2; REAL_OF_NUM_LE; ARITH;
             REAL_OF_NUM_LT; REAL_POWER_POW; SQRT_POS_LT;
             REAL_POWER_POWER; SQRT_2_IRRATIONAL; RATIONAL_NUM]);;

procedural proof: shooting at subgoals

• goal ‘proof obligation’ that what is left to be proved

• tactic command that proves part of a goal reduces the goal to zero or more new ‘subgoals’

proving is a computer game!

goals are like monsters tactics are like guns

theorems are like game levels lemmas and tactics the HOL Light library consists of

• lemmas proven statements declarative knowledge basic library: 1501 lemmas from ⊢ ⊤ ⇔ λx^{𝔹}. x = λx^{𝔹}. x to ⊢ ∀x ∀y. x = y ⇔ x_{1} = y_{1} ∧ x_{2} = y_{2}

• tactics small programs that know how to prove things procedural knowledge basic library: 128 tactics

lemmas used in the proof

SQRT_2_IRRATIONAL              \sqrt{2} ∉ ℚ
RATIONAL_NUM                   n̄ ∈ ℚ
REAL_POWER_POWER  (x^{y})^{z} = x^{yz}

SQRT_POW_2               ¯0 ≤ x ⇒ (\sqrt{x})^{2} = x

REAL_POW_2  x^{2} = x · x
REAL_POWER_POW            ¯0 < x ⇒ xn̄ = x^{n}
SQRT_POS_LT                ¯0 < x ⇒ ¯0 < \sqrt{x}
REAL_OF_NUM_LE             m̄ ≤ n̄ ⇔ m ≤ n
REAL_OF_NUM_LT             m̄ < n̄ ⇔ m < n

ARITH  very long statement

the equality

 [figure: ARITH; ARITH; 0 < 2; REAL_OF_NUM_LT; ARITH; 0 ≤ 2; REAL_OF_NUM_LE; ¯0 < ¯2; SQRT_POS_LT; 0 ≤ 2; REAL_OF_NUM_LE; REAL_POWER_POWER; REAL_POW_2; ¯0 ≤ ¯2; SQRT_POW_2; ¯0 < \sqrt{¯2}; REAL_POWER_POW; ¯0 ≤ ¯2; SQRT_POW_2; (\sqrt{¯2}^{\sqrt{¯2}})^{\sqrt{¯2}}; =; \sqrt{¯2}^{\sqrt{¯2}·\sqrt{¯2}}; =; \sqrt{¯2}^{^{\sqrt{¯2}}^{2}}; =; \sqrt{¯2}^{¯2}; =; \sqrt{¯2}^{2}; =; ¯2]

tactics used in the proof

• ASM_CASES_TAC

do a case split according to whether a given statement is true or false

• EXISTS_TAC

prove an existential statement by providing a witness

• REWRITE_TAC
SIMP_TAC
ASM_REWRITE_TAC
ASM_SIMP_TAC

rewrite the goal according to a set of lemmas the proof: interactively

DEMO

commands g set the goal e execute a tactic

HOL architecture

types and terms

• types

σ ::= α | (σ_{1}, …, σ_{n}) op
σ_{1} → σ_{2} (σ_{1}, σ_{2}) fun
truth values  () bool
‘individuals’  () ind

• terms

t ::= x | c | t t′ | λx. t
equality =
choice operator @

the ten deduction rules of the HOL logic

• REFL
• TRANS
• MK_COMB
• ABS
• BETA
• ASSUME
• EQ_MP
• DEDUCT_ANTISYM_RULE
• INST
• INST_TYPE

example of a HOL rule: DEDUCT_ANTISYM_RULE

version from the manual & the implementation

\frac{Γ ⊢ p  Δ ⊢ q}{(Γ − \{q\}) ∪ (Δ − \{p\}) ⊢ p = q} DEDUCT_ANTISYM_RULE

didactic version

\frac{Γ ∪ \{q\} ⊢ p Δ ∪ \{p\} ⊢ q}{Γ ∪ Δ ⊢ p = q}

definitions

• term definition introduction of new term constant c to the signature abbreviates an existing term

• type definition introduction of new type constant op to the signature cuts out part from an existing type functional programming will save the world

spin-off technology

proof verification LCF

↓

functional programming ML meta-language

(originally: the language for programming LCF tactics)

different programming paradigm Lisp, ML, Haskell the HOL kernel HOL Light is an ML program

source of the whole system  62,642 lines of code 930 pages

75 files

source of the kernel  643 lines of code 10 pages
type.ml  135 lines of code  2 pages
term.ml  279 lines of code  4 pages
thm.ml  229 lines of code  4 pages

de Bruijn criterion the three basic HOL types

three datatypes in the implementation (all three are syntactic trees represented in the computer memory)

type hol_type = Tyvar of string
              | Tyapp of string * hol_type list
type     term = Var of string * hol_type
              | Const of string * hol_type
              | Comb of term * term
              | Abs of term * term
type      thm = Sequent of (term list * term)

implementation of DEDUCT_ANTISYM_RULE

\frac{Γ ⊢ p  Δ ⊢ q}{(Γ − \{q\}) ∪ (Δ − \{p\}) ⊢ p = q} DEDUCT_ANTISYM_RULE

let DEDUCT_ANTISYM_RULE (Sequent(asl1,c1)) (Sequent(asl2,c2)) =
let asl1' = filter (not o (aconv c2)) asl1
and asl2' = filter (not o (aconv c1)) asl2 in
Sequent(term_union asl1' asl2',mk_eq(c1,c2));;

Mizar proof

Andrzej Trybulec and Mizar

Mizar: second star in the big dipper system from Białystok, Poland

motivated from mathematics instead of from computer science

first order predicate logic + axiom schemes + ZFC set theory + arbitrarily large inaccessible cardinals

implemented in Pascal source code not freely accessible to just anyone the proof: in the file

theorem Example: ex x, y being real number st
x is irrational & y is irrational & x to_power y is rational
proof
set w = sqrt 2; w > 0 by AXIOMS:22,SQUARE_1:84;
then A1: (w to_power w) to_power w = w to_power (w * w) by POWER:38
.= w to_power (w^2) by SQUARE_1:def 3
.= w to_power 2 by SQUARE_1:def 4
.= w^2 by POWER:53
.= 2 by SQUARE_1:def 4;
per cases;
suppose A2: w to_power w is rational;
take w, w; thus thesis by A2,IRRAT_1:1,INT_2:44;
end;
suppose A3: w to_power w is irrational;
take w to_power w, w; thus thesis by A1,A3,IRRAT_1:1,INT_2:44;
end;
end;

AXIOMS:22  x ≤ y ∧ y ≤ z ⇒ x ≤ z

INT_2:44  2 is prime

IRRAT_1:1  p is prime ⇒ \sqrt{p} ∉ ℚ
POWER:38  a > 0 ⇒ (a^{b})^{c} = a^{bc}

SQUARE_1:def 3  x^{2} = x · x

SQUARE_1:def 4  0 ≤ a ⇒ (x = \sqrt{a} ⇔ 0 ≤ x ∧ x^{2} = a)

SQUARE_1:84  1 < \sqrt{2}
POWER:53                     a to_power 2 = a^2

the Mizar Mathematical Library biggest library of formalized mathematics in the world

44,711 lemmas
1,660,695 lines of ‘code’
58.8 megabytes
152 ‘authors’
834 ‘articles’

the axioms of Mizar

TARSKI:def 3  X ⊆ Y ⇔ (∀x. x ∈ X ⇒ x ∈ Y)
TARSKI:def 5  ⟨x, y⟩ = {{x, y}, {x}}
TARSKI:def 6  X ∼ Y ⇔ ∃Z. (∀x. x ∈ X. ⇒ ∃y. y ∈ Y ∧ ⟨x, y⟩ ∈ Z) ∧
(∀y. y ∈ Y. ⇒ ∃x. x ∈ X ∧ ⟨x, y⟩ ∈ Z) ∧
(∀x∀y∀z∀u. ⟨x, y⟩ ∈ Z ∧ ⟨z, u⟩ ∈ Z ⇒ (x = z ⇔ y = u))

TARSKI:def 1  x ∈ {y} ⇔ x = y

TARSKI:def 2  x ∈ {y, z} ⇔ x = y ∨ x = z
TARSKI:def 4  x ∈ ⋃ X ⇔ ∃Y. x ∈ Y ∧ Y ∈ X
TARSKI:2  (∀x. x ∈ X ⇔ x ∈ Y) ⇒ X = Y
TARSKI:7  x ∈ X ⇒ ∃Y. Y ∈ X ∧ ¬∃x. x ∈ X ∧ x ∈ Y
TARSKI:sch 1  (∀x ∀y ∀z. P [x, y] ∧ P [x, z] ⇒ y = z) ⇒
(∃X. ∀x. x ∈ X ⇔ ∃y. y ∈ A ∧ P [y, x])
TARSKI:9  ∃M. N ∈ M ∧ (∀X∀Y. X ∈ M ∧ Y ⊆ X ⇒ Y ∈ M) ∧
(∀X. X ∈ M ⇒ ∃Z. Z ∈ M ∧ ∀Y. Y ⊆ X ⇒ Y ∈ Z) ∧
(∀X. X ⊆ M ⇒ X ∼ M ∨ X ∈ M)

the proof: interactively

DEMO

utopia

‘when things changed’ the three phases in the development of mathematics

• proof Greece, fourth century BC

• rigor nineteenth century

• computer checked proof the present the QED manifesto

Boyer e.a. anonymous manifesto

let’s proof check all of mathematics!

very nice and thought-provoking document but: nobody started doing anything

why? why mathematicians are not interested (yet)

• it is much too much work one work-week for one page from an undergraduate math textbook

• it does not have any good application all you get is a big tar file

• it does not resemble mathematics it looks like program code instead of mathematics also: the reformists don’t help the three reasons for computer proof

• certainty catching all the mistakes

• clarity communicating mathematics in a totally clear way

• beauty the cultural reason mathematics is a human artifact & computers are its natural medium

… and furthermore, it’s fun!