formalization & decision procedures

Freek Wiedijk Radboud University Nijmegen

‘Diamant’ day Radboud University Nijmegen 2005 10 28, 11:15

intro

structure of the talk

• formalization of mathematics

Brouwer institute:

– lambda calculus

– formalization of mathematics

– intuitionistic mathematics

• decision procedures procedures for automatically solving a well-defined class of problems

⟶ talk by Jeremy Avigad

formalization of mathematics

‘formalization’

writing mathematics in a ‘computer language’ computer checks the correctness

keeps track of everything

bridges small gaps in the proofs

a very short history • 1910–1913 Russell & Whitehead, Principia Mathematica

formalization of mathematics

‘formalization’

writing mathematics in a ‘computer language’ computer checks the correctness

keeps track of everything

bridges small gaps in the proofs

a very short history • 1910–1913 Russell & Whitehead, Principia Mathematica • 1967–1976 N.G. de Bruijn, Automath four kinds of mathematics in the computer

• numerical mathematics experimentation, visualization

\frac{1}{3} = 0.3333333333

• computer algebra systems CAS \sqrt{x^{2}} = x

• automated theorem proving ATP currently mainly about solving logical puzzles

• proof formalization state of the art: the most impressive that we can currently do Fundamental Theorem of Algebra

Mizar  Robert Milewski, 2000
HOL Light  John Harrison, 2000
Coq  Herman Geuvers e.a., 2000

Jordan Curve Theorem

HOL Light  Tom Hales, 2005
Mizar  many people, 2005

Prime Number Theorem

Isabelle  Jeremy Avigad, 2004

Four Color Theorem

Coq  Georges Gonthier, 2004

de Bruijn criterion can we trust formalized mathematics? de Bruijn criterion = correctness of small part of the program (‘kernel’) guarantees the correctness of all the mathematics HOL Light kernel

643 lines of program code
10 pages of program source listing (including comments)

essential parts of this kernel proved correct using HOL Light itself philosophical objections

• irrelevant: bugs in the checker inconsistency of the logic hardware malfunction

• relevant: correctness of the definitions

Isabelle’s former definition of prime number

−p and −1 are also divisors of p with the former definition there were no prime numbers six systems for formalizing mathematics

HOL Light  the most effective system of the moment
Mizar  the most mathematical system of the moment
Isabelle  the best of HOL and Mizar combined
Coq  the most expressive system of the moment
Nuprl  the US counterpart of Coq
PVS  what most computer scientists use

higher order logic type theory three kinds of foundations

• set theory Mizar full ZFC set theory (‘everything is a set’) objects are untyped

• higher order logic HOL, Isabelle, PVS weak version of set theory (only finitely many times a power set from the natural numbers) objects are typed

• type theory Coq, Nuprl as expressive as full ZFC set theory, but intuitionistic objects are typed inductive types (‘free algebra’ is a primitive) intuitionism! intuitionism encodes computability in the logic

∃ x … means there is an algorithm to compute x such that …

intermediate value theorem is not provable provable if the function is sufficiently often ≠ 0 provable if the function is a polynomial provable that the value gets arbitrarily close to 0

a very short history • 1907 L.E.J. Brouwer: intuitionism

• 1967 Errett Bishop: Bishop-style constructivism state of the art: top 100 of theorems

1. The Irrationality of the Square Root of 2 ← all systems
2. Fundamental Theorem of Algebra ← HOL, Mizar, Coq
3. The Denumerability of the Rational Numbers ← HOL, Mizar, Isabelle
4. Pythagorean Theorem ← HOL, Mizar, Coq
5. Prime Number Theorem ← Isabelle
6. Gödel’s Incompleteness Theorem ← HOL, Coq, nqthm
7. Law of Quadratic Reciprocity ← Isabelle, nqthm
8. The Impossibility of Trisecting the Angle and Doubling the Cube ← HOL
9. The Area of a Circle The Area of a Circle
10. Euler’s Generalization of Fermat’s Little Theorem ← HOL, Mizar, Isabelle
. . . . . .

64% formalized

            http://www.cs.ru.nl/~freek/100/

state of the art: what does it look like?

formalization = human-computer symbiosis

two main proof styles

• procedural style HOL, Coq, Nuprl, PVS HOL, Coq, Nuprl, PVS computer is doing the proof under the direction of the human proofs can be terse proof looks like unreadable computer code

• declarative style Mizar, Isabelle Mizar, Isabelle the human is writing the proof checked by the computer proofs more verbose more writing from the human needed example of a Coq formalization

Lemma sqrt_mult:
forall x y:R, 0 <= x -> 0 <= y -> sqrt (x * y) = sqrt x * sqrt y.
Proof.
intros x y H1 H2;
apply
 (Rsqr_inj (sqrt (x * y)) (sqrt x * sqrt y)
   (sqrt_positivity (x * y) (Rmult_le_pos x y H1 H2))
   (Rmult_le_pos (sqrt x) (sqrt y) (sqrt_positivity x H1)
     (sqrt_positivity y H2)));
rewrite Rsqr_mult;
repeat rewrite Rsqr_sqrt;
[ ring | assumption | assumption | apply (Rmult_le_pos x y H1 H2) ].
Qed.

example of a Mizar formalization

theorem Th97:
0 <= x & 0 <= y implies sqrt (x*y) = sqrt x * sqrt y
proof
assume A1: 0 <= x & 0 <= y;
then A2: 0 <= x*y by Th19;
then A3: (sqrt(x*y))^2 = x*y by Def4
  .= (sqrt x)^2*y by A1,Def4
  .= (sqrt x)^2*(sqrt y)^2 by A1,Def4
  .= (sqrt x*sqrt y)^2 by Th68;
0 <= sqrt x & 0 <= sqrt y by A1,Def4;
then A4: 0 <= sqrt(x*y) & 0 <= sqrt x*sqrt y by A2,Def4,Th19;
thus sqrt(x*y) = sqrt((sqrt x*sqrt y)^2) by A2,A3,Def4
  .= sqrt x*sqrt y by A4,Lm5;
end;

state of the art: how difficult is it?

N.G. de Bruijn:

A very important thing that can be concluded from all writing experiments is the constancy of the loss factor. The loss factor expresses what we loose in shortness when translating very meticulous ‘ordinary’ mathematics into Automath.

the de Bruijn factor in space: about 4 times as long

the de Bruijn factor in time: about 1 week/textbook page why isn’t formalization of mathematics bigger?

• it does not have a good application

• it does not look like mathematics

• formalizing trivialities is just too much work

x = i/n , n = m + 1 ⊢ n! · x = i · m!
\frac{k}{n} ≥ 0 ⊢ |\frac{n − k}{n} − 1| = \frac{k}{n}
n ≥ 2 , x = \frac{1}{n + 1} ⊢ \frac{x}{1 − x} < 1
0 ≤ n ≤ (\frac{K}{2} ) x , C > 0 , 0 < ε < 1 ⊢ (1 + \frac{ε}{3(C + 3)}) n < Kx

decision procedures

don’t expect intelligent questions from computers Paul J. Cohen, Arnold Neumaier, and probably many mathematicians:

‘just have the computer read normal L^{A}TEX it can ask questions if it does not understand’

‘also use this for ambiguities in formulas’

wrong mental model, computers do not work like that so what is it that computers can ‘understand’? three types of proof automation

• basic automation

• proof search automated theorem proving general, rather weak

• decision procedures specific, very useful a first kind of automation: basic automation systems often keep a database of lemmas with rules of a specific shape

• rewrite rules simp ∀x⃗. (t_{1}(x⃗) = t_{2}(x⃗))

• generalized implications (for backward chaining) auto

∀x⃗. (ϕ_{1}(x⃗) ∧ … ∧ ϕ_{n}(x⃗) → ψ(x⃗))

and have a command that ‘applies’ those as much as possible implementations in proof assistants

Isabelle  simp

                      Coq  auto

a second kind of automation: proof search two search strategies

• resolution work from the assumptions towards the conclusion

• tableaux methods work from the conclusion back to the assumptions

implementations in proof assistants

                  HOL Light  MESON_TAC

Isabelle  blast

a third kind of automation: decision procedures well-defined class of statements (explicit list of functions and predicates that can be used) decidable whether a statement in the class is provable or not decision procedure: command in the system that implements this

example

f(f(x) − f(y)) ≠ f(z) ∧ y ≤ x ∧ y ≥ x + z ⇒ z < 0 proved at the push of a button decision procedures 1: arithmetic in the real numbers

first order statements involving + − · ÷ = ≤ <

theory of real-closed fields complete & decidable theory

first proved decidable by Alfred Tarski ⟶ decidability of geometry cylindrical algebraic decomposition CAD complexity: doubly exponential

kissing problem: how many spheres fit around a sphere in n dimensions?

\begin{matrix}n = 2 & 6 \\ n = 3 & 12 \\ n = 4 & 24 or 25? \end{matrix}

quantifier elimination

∀x ∈ ℝ . a x^{2} + b x + c > 0
⇔

a > 0 ∧ b^{2} − 4ac < 0 ∨ a = 0 ∧ b = 0 ∧ c > 0

eliminates the ∀ quantifier and its variable from the formula this kind of quantifier elimination is systematically possible

iterated quantifier elimination leads to formula without variables ⟶ just comparisons of numbers decision procedures 2: linear arithmetic

first order statements involving + − = ≤ < and

multiplication by rational constants

no arbitrary multiplication only linear equalities and inequalities

example

∃ x, y ∈ ℝ . 0 ≤ x ≤ y − 3 ∧ x + y ≤ 5 ∧ 2y − 3x ≤ 5

implementations in proof assistants

                  HOL Light  ARITH_TAC

Isabelle  arith

                  Coq  omega

real numbers versus integers

ℝ  ℕ
real-closed fields  Peano arithmetic
full theory decidable undecidable

CAD

Presburger arithmetic

linear arithmetic decidable decidable

Fourier-Motzkin Fourier-Motzkin, by example quantifier elimination of

∃ y. 0 ≤ x ∧ x ≤ y − 3 ∧ x + y ≤ 5 ∧ 2y − 3x ≤ 5 put variable y everywhere all by itself on right or left hand side

∃ y. 0 ≤ x ∧ x + 3 ≤ y ∧ y ≤ 5 − x ∧ y ≤ \frac{5}{2} + \frac{3}{2}x

compare all lower bounds with all upper bounds

0 ≤ x ∧ x + 3 ≤ 5 − x ∧ x + 3 ≤ \frac{5}{2} + \frac{3}{2}x

we now have eliminated the variable y decision procedures 3: the universal formulas of real arithmetic sum of squares decomposition

∀x_{1} … x_{n}. f(x_{1}, …, x_{n}) ≥ 0

follows from

f(x_{1}, …, x_{n}) = ∑_{k} (g_{k}(x_{1}, …, x_{n}))^{2}

such decompositions can be found by semidefinite programming ⟶ decision procedure

implementations in proof assistants

                  HOL Light  REAL_SOS

decision procedures 4: combining decision procedures

separate decision procedures for universal statements about

arithmetic arrays bit-vectors uninterpreted functions …

integrate all of them in one master decision procedure

• Nelson-Oppen

• Shostak

the story of PVS and ICS Craig’s interpolation theorem

ϕ_{1} ⊢ ϕ_{2}

implies that there is an interpolant ψ with only symbols both in ϕ_{1} and ϕ_{2} such that

ϕ_{1} ⊢ ψ and ψ ⊢ ϕ_{2}

Craig-Robinson variant

ϕ_{1}, ϕ_{2} ⊢ ⊥

implies that there is a ψ with only symbols both in ϕ_{1} and ϕ_{2} such that

ϕ_{1} ⊢ ψ and ϕ_{2} ⊢ ¬ψ

Nelson-Oppen, by example

f(v − 1) − 1 = v + 1 ∧ f(u) + 1 = u − 1 ∧ u + 1 = v ⇒ ⊥

combines decision procedures of arithmetic and uninterpreted functions

1. introduce new variables plus equalities such that all conjuncts only involve one of the component theories

\begin{matrix}v_{1} = v − 1 ∧ v_{2} = f(v_{1}) ∧ v_{3} = f(u) ∧ \\ v_{2} = v + 1 ∧ v_{3} + 1 = u − 1 ∧ u + 1 = v \end{matrix}

2. repeatedly infer equalities in each of the separate component theories and add them to the set of conjuncts

\begin{matrix}v_{1} = v − 1 ∧ v_{2} = v + 1 ∧ v_{3} + 1 = u − 1 ∧ u + 1 = v \\ ⇒ u = v_{1} \end{matrix}

Nelson-Oppen, by example (continued)

\begin{matrix}v_{2} = f(v_{1}) ∧ v_{3} = f(u) ∧ u = v_{1} \\ ⇒ v_{2} = v_{3} \end{matrix}

v_{1} = v − 1 ∧ v_{2} = v + 1 ∧ v_{3} + 1 = u − 1 ∧ u + 1 = v ∧ u = v_{1} ∧ v_{2} = v_{3}

⇒ ⊥

(v_{2} = v + 1 = u + 2 and v_{3} = u − 2, so they cannot be equal)

3. if we manage to derive a contradiction in one of the theories then the original conjunction was contradictory; if not then it is satisfiable

extro

so when will mathematicians start formalizing their mathematics? ‘killer app’ for formalization has not yet been found

• the mathematics will be guaranteed to be fully correct

• the mathematics will be guaranteed to be fully explicit

Jeremy Avigad:

things become interesting when time for formalization < time for referee checking