formal mathematics

Freek Wiedijk Nijmegen University

Leiden University 2002-10-10, 16:00

proof checking

the best of two worlds a wonderful computer game! proof checking is like

• programming but no bugs, and not as trivial!

• doing mathematics

but completely transparent, and the computer helps! (currently closer to programming than to doing mathematics) proof checking ↔ mathematical assistants computer can help with:

• the discovery of mathematics

• the registration of mathematics here only interested in the formalization of already existing mathematics analogy

mathematician ↔ proof checker
violin player music composer ↔ hifi sound technician violin player

what does proof checking buy me as a mathematician?

currently:

• nothing the gains are not worth the effort yet

in the (near? far?) future:

• correctness certainty that lemmas are correct certainty that a paper is correct when submitted (the referees won’t need to judge correctness anymore, but only originality and relevance)

• clarity no need to ask the author of a text for clarification everything is there! philosophy of reliability I: the de Bruijn principle

worry about own mistakes → worry about bugs in the checker?

analogous to compiler bugs in programming: software problems are hardly ever caused by compiler bugs

de Bruijn principle check mathematics using a small checker

two approaches:

• small ‘proof kernel’ that everything has to go through (many current systems)

• export in a format that can be checked by a small separate checker example: the Ivy program for the Otter prover philosophy of reliability II: are we doing what we think we are doing?

proofs are checked, but definitions can be ‘wrong’

definitions often are adapted for formalization how to know that they still define the intended notions?

example definition of a planar graph in the four color theorem formalization: no mention of the topology of the plane!

Trybulec: definitions are a debt, theorems pay them back trust comes from the theory that is proved about the definitions the state of the art: mathematics that already has been formalized

examples of formalized theorems:

• fundamental theorem of calculus

• fundamental theorem of algebra

• Taylor’s theorem

• Hahn-Banach theorem

• Urysohn’s lemma

• Stone’s theorem (paracompactness of metrizable spaces)

• Stone’s theorem (representations of boolean algebras)

• Gödel’s first incompleteness theorem

• reducibility of the configurations for the four color theorem • correctness of Buchberger’s algorithm

• fundamental theorem of Galois theory

full translation (half finished) of a book on continuous lattices how difficult is it? formalizing mathematics: trivial or undoable? some metrics: de Bruijn factor = ratio between formalization and informal text

currently: 4 times as big time needed to formalize a page from a textbook

currently: 1 week (estimate: ‘all undergraduate math’ will take 140 man-year) automation ↔ human control

mathematical reasoning is like an iceberg

conscious part of reasoning ⟶

unconscious part of reasoning ⟶

the story of the formalizations of the fundamental theorem of algebra

too much automation ‘lost in proof space’: user doesn’t understand the proof anymore → formalizing becomes much harder

automation should focus on the unconscious part of the reasoning automation should not amaze the user can the computer prove things that human mathematicians cannot? EQP, 1996:

all Robbins algebras are Boolean

the computer is:

• strong in combinatorial search through many cases

• weak in goal oriented proof

surprisingly trivial steps can’t be proved automatically yet Shankar: focus on decision procedures instead of proof search (decision procedure = algorithm to answer a specific class of questions)

• general purpose proof search doesn’t work well

• domain specific proof generation is very useful

three systems

Coq

Huet & Coquand, Paulin INRIA, France 1984–today

implemented in the ocaml dialect of ML advantages:

• popular for mathematics

• powerful logic

prehistoric precursor: Automath propositions as types, proofs as objects

Coq’s logic: type theory

types with objects ↔ propositions with proofs ‘Curry-Howard isomorphism’

proofs become first class objects → proofs can be used as function arguments

division modeled as a ternary function

div(x, y, ‘proof that y ≠ 0’)

with this kind of division it is impossible to write 1/0 (no ‘proof object’ for the third argument)

HOL Light

recent reimplementation of the HOL system

Gordon, Harrison & Slind Cambridge, UK 1985–1995–today

implemented in the ocaml dialect of ML advantages:

• simple and elegant

• strong automation

prehistoric precursor: LCF the de Bruijn principle in action

HOL Light proof kernel: 285 lines of ML code = 8 pages of source text possible to really understand this

   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);;

10 primitive proof rules + 3 axioms taking mathematical objects in your hands

HOL proofs = programs in the ML programming language

variables hold ‘mathematical objects’ and ‘proved theorems’ (really: variables hold terms describing mathematical objects)

   #let s = `{x | x * x = &2}`;;
   s : term = `{x | x * x = &2}`
   #let t = prove(`?x.  x * x = &2`,
     EXISTS_TAC `sqrt(&2)` THEN REWRITE_TAC
     [GSYM POW_2; SQRT_POW2] THEN ARITH_TAC);;
   t : thm = |- ?x. x * x = &2
   #

programming with mathematical objects instead of integers and reals Mizar

Trybulec & Bylinski Bialystok, Poland 1973–1989–today

implemented in the Delphi dialect of Pascal advantages:

• mathematics oriented

• large library

prehistoric precursor: Mizar readable proofs

Mizar proofs can be read as text

per cases; suppose ex x st not P[x];
 then consider a such that A1: not P[a];
 take a; assume P[a]; hence thesis by A1;
suppose A2: for x holds P[x];
 consider a; take a; thus thesis by A2;

proofs in most other systems are unreadable ‘code’

ASM_CASES_TAC `?x:A. ~P x` THEN
RULE_ASSUM_TAC (REWRITE_RULE[NOT_EXISTS_THM]) THENL
[POP_ASSUM (X_CHOOSE_TAC `a:A`); ALL_TAC] THEN
EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]

taking ZFC seriously

Bourbaki: ZFC = foundations in theory ZFC = foundations in practice?!

de Bruijn: ZFC doesn’t match mathematical practice what is the meaning of the ∩ of a triangle and a number?

Mizar shows: Bourbaki propaganda is true it is practical to formalize real mathematics on a ZFC foundation

Mizar axioms (ZFC + inaccessibles) →  28 lines
Mizar library  → 1,400,000 lines

(everything in the Mizar library is fully proved from the axioms)

an example in Mizar

Pythagorean triples a solution of

a^{2} + b^{2} = c^{2}

with no common divisors always has the form

a = m^{2} − n^{2} b = 2mn c = m^{2} + n^{2}

examples

\begin{aligned}m = 2  n = 1 & → & 3^{2} & + & 4^{2} & = & 5^{2} \\ m = 3  n = 2 & → & 5^{2} & + & 12^{2} & = & 13^{2} \\ m = 4  n = 1 & → & 15^{2} & + & 8^{2} & = & 17^{2} \\ m = 4  n = 3 & → & 7^{2} & + & 24^{2} & = & 25^{2} \end{aligned}

formal proof sketch

reserve a,b,c,m,n for Nat;
let a,b,c; assume a^2 + b^2 = c^2;
assume a,b are_relative_prime;
then a is odd or b is odd; assume a is odd;
ex m,n st a = m^2 - n^2 & b = 2*m*n & c = m^2 + n^2
proof
 b is even; c is odd;
X: (c + a)/2,(c - a)/2 are_relative_prime;
 ((c + a)/2)*((c - a)/2) = (c^2 - a^2)/4 .= (b/2)^2;
 then ((c + a)/2)*((c - a)/2) is square;
 then (c + a)/2 is square & (c - a)/2 is square by X;
 consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;
 take m,n;

formal proof sketch (continued)

consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;
take m,n;
thus a = (c + a)/2 - (c - a)/2 .= m^2 - n^2;
b^2 = (c + a)*(c - a) .= 4*m^2*n^2 .= (2*m*n)^2;
hence b = 2*m*n;
thus c = (c + a)/2 + (c - a)/2 .= m^2 + n^2;
end;

syntactically correct Mizar semantically correct Mizar too high level: Mizar cannot check the correctness

• steps are too big for Mizar

• links between steps are missing a fragment of the full proof

then
X: (c + a)/2,(c - a)/2 are_relative_prime by Lm3;
((c + a)/2)*((c - a)/2) = ((c + a)*(c - a))/(2*2)
  by REAL_1:35
 .= (c^2 - a^2)/4 by SQUARE_1:67
 .= (b^2)/(2*2) by H1,INT_1:3
 .= (b^2)/(2^2) by SQUARE_1:def 3
 .= (b/2)^2 by SQUARE_1:69;
then ((c + a)/2)*((c - a)/2) is square by A1,Def1;
then (c + a)/2 is square & (c - a)/2 is square by X,Lm4;
then (ex m st m^2 = (c + a)/2) &
 (ex n st n^2 = (c - a)/2) by Def1;
then consider m,n such that
A9: m^2 = (c + a)/2 & n^2 = (c - a)/2;

formal mathematics can talk about ‘higher’ objects

claim: any mathematics can be formalized

not only about basic objects like numbers and numeric functions objects can be abstract and ‘large’

example: Yoneda lemma

   definition let A be Category;
    func Yoneda(A) ->
      Contravariant_Functor of A,Functors(A,EnsHom(A))
     means
      for f being Morphism of A holds
       it.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];
   end;

observation: abstract math is easier to formalize than basic math

conclusion

isn’t this all just engineering? this talk: the user’s point of view research topics

• the theory of logical foundations logics: paradoxes, consistency, conservativity type systems: confluence, termination, subject reduction

• the theory of proof search

• the theory of decision procedures interaction between decision procedures moving the decision procedures inside the logic: reflection

but: ‘just engineering’ is also important to get a usable system it might not be for you yet, but it’s serious!

• not yet practical

• interesting developments

• it might change the (mathematical) world

• ancient Greeks: invention of proof

• nineteenth century: invention of rigor • today?