two automation challenges

Freek Wiedijk Radboud University Nijmegen

Dagstuhl seminar: interaction versus automation

2009 10 06, 17 : 00

automation

program verification versus mathematics assistant versus word processor

2

formal proof sketches

textbook proof from Hardy & Wright

Theorem 43 (Pythagoras’ theorem). \sqrt{2} is irrational.

The traditional proof ascribed to Pythagoras runs as follows. If \sqrt{2} is rational, then the equation

a^{2} = 2b^{2}  (4.3.1)

is soluble in integers a, b with (a, b) = 1. Hence a^{2} is even, and therefore a is even. If a = 2c, then 4c^{2} = 2b^{2}, 2c^{2} = b^{2}, and b is also even, contrary to the hypothesis that (a, b) = 1. □ formal proof sketch of the textbook proof

theorem Th43: sqrt 2 is irrational proof

assume sqrt 2 is rational;

consider a, b such that 4 3 1: aˆ 2 = 2 ∗ bˆ 2 and

a,b are relative prime; aˆ 2 is even; a is even; consider c such that a = 2 ∗ c; 4 ∗ cˆ 2 = 2 ∗ bˆ 2; 2 ∗ cˆ 2 = bˆ 2; b is even; thus contradiction;

end;

theorem Th43: sqrt 2 is irrational :: Pythagoras’ theorem

proof assume sqrt 2 is rational; consider a, b such that

4 3 1:  aˆ 2 = 2 ∗ bˆ 2

and a, b are relative prime; aˆ 2 is even; a is even; consider c such that a = 2 ∗ c; 4 ∗ cˆ 2 = 2 ∗ bˆ 2; 2 ∗ cˆ 2 = bˆ 2; b is even; thus contradiction; end; full declarative formalization

theorem Th43: sqrt 2 is irrational proof

assume sqrt 2 is rational;

then consider a, b such that A1: b ^{<>} 0 and A2: sqrt 2 = a/b and A3: a, b are relative prime by Def1; A4: bˆ 2 ^{<>} 0 by A1, SQUARE 1:73;

2 = (a/b)ˆ 2 by A2, SQUARE 1:def 4

.= aˆ 2/bˆ 2 by SQUARE 1:69; then

4 3 1: aˆ 2 = 2 ∗ bˆ 2 by A4, REAL 1:43; aˆ 2 is even by 4 3 1, ABIAN:def 1; then

A5: a is even by PYTHTRIP:2; :: continue in next column

then consider c such that A6: a = 2 ∗ c by ABIAN:def 1; A7: 4 ∗ cˆ 2 = (2 ∗ 2) ∗ cˆ 2

.= 2ˆ 2 ∗ cˆ 2 by SQUARE 1:def 3

.= 2 ∗ bˆ 2 by A6, 4 3 1, SQUARE 1:68; 2 ∗ (2 ∗ cˆ 2) = (2 ∗ 2) ∗ cˆ 2 by AXIOMS:16

.= 2 ∗ bˆ 2 by A7; then 2 ∗ cˆ 2 = bˆ 2 by REAL 1:9; then bˆ 2 is even by ABIAN:def 1; then b is even by PYTHTRIP:2; then 2 divides a & 2 divides b by A5, Def2; then

A8: 2 divides a gcd b by INT 2:33; a gcd b = 1 by A3, INT 2:def 4; hence contradiction by A8, INT 2:17;

end;

first challenge: automate elementary reasoning steps Larry Wos:

• experience with formal proof sketches:

computers routinely proving non-trivial steps is far away

• focus should be on making manual math formalization efficient

luxury mathmode

procedural proof using tactics

# g `!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2`;;
val it : goalstack = 1 subgoal (1 total)
`!n. nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2`
# e INDUCT_TAC;;
val it : goalstack = 2 subgoals (2 total)
  0 [`nsum (1..n) (\i. i) = (n * (n + 1)) DIV 2`]
`nsum (1..SUC n) (\i. i) = (SUC n * (SUC n + 1)) DIV 2`
`nsum (1..0) (\i. i) = (0 * (0 + 1)) DIV 2`
# e (ASM_REWRITE_TAC[NSUM_CLAUSES_NUMSEG]);;
val it : goalstack = 1 subgoal (2 total)
`(if 1 = 0 then 0 else 0) = (0 * (0 + 1)) DIV 2`
#

batch checked declarative proof

!n. nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2
proof
nsum(1..0) (\i. i) = 0 by NSUM_CLAUSES_NUMSEG;
... = (0*(0 + 1)) DIV 2 [1];
now let n be num;
assume nsum(1..n) (\i. i) = (n*(n + 1)) DIV 2 [2];
1 <= SUC n;
nsum(1..SUC n) (\i. i) = (n*(n + 1)) DIV 2 + SUC n
  by NSUM_CLAUSES_NUMSEG,2;
thus ... = ((SUC n)*(SUC n + 1)) DIV 2;
end;
qed by INDUCT_TAC,1;

integrating the two worlds

Mizar Light = ‘luxury mathmode’ (Henk) = proof language/interface on top of HOL Light

demo

computer algebra with assumptions

two flavors of computer algebra

\xymatrix{ & mathematical computation by computer \ar[dl] \ar[dr] \\ numerical computation &  & symbolic computation \ar[dl] \ar[dr] \\  & computer algebra &  & computer calculus \\  & \frac{1}{X} ∈ ℂ (X) &  & λX. \frac{1}{X} ∈ ℂ^{ℂ _{≠0}} \\  & \frac{X}{X} = 1 as algebraic objects &  & \frac{X}{X} ≠ 1 when X = 0}

the Content MathML signature 147 XML elements, like: −1 λ ∘ ! ÷ max min − + · √ gcd ∧ ∨ ¬ ⇒ ∀ ∃ | · | \overline{·} arg

ℜ ℑ ⌊·⌋ ⌈·⌉ = ≠ > < ≥ ≤ ⇔ ≈ | ∫ \frac{d}{dx} \frac{∂}{∂x} ∇ ∪ ∩ ∈ ⊆

⊂ \ # × ∑ ∏ lim ln log sin cos tan sec csc cot sinh cosh tanh coth arcsin arccos arctan μ σ det ^{T} ⊗ ℤ ℝ ℚ ℕ ℂ e i ⊤ ⊥ ∅ π γ ∞

MathML  L^{A}TEX  HOL

 p ⇒ q  implies             \Rightarrow     ==>
 A × B  cartesianproduct    \times          prod , CROSS
   0  cn                                  NUMERAL
 ∑_{i=1}^{n} a_{i}  sum                 \sum            nsum , sum
   ∞  infinity            \infty

sample problem

x ≠ 0 ∧ | ln(x^{2})| > 1 ∧ ∫_{0}^{x} t dt ≤ 1 ⇒ −\frac{1}{\sqrt{e}} < x < \frac{1}{\sqrt{e}}

• this is not about first order proof search first order proof search cannot easily calculate integrals first order proof search cannot easily do numerical approximations

• this is not about decision procedures decision procedures generally work over specific small signatures

• this is not about systems like Maple and Mathematica current computer algebra systems generally do not use assumptions second challenge: take next step in mathematics automation progress:

• automation of formalized primary school math = ‘arithmetic’ • automation of formalized high school math = ‘calculus’

• automation of formalized university math

should run in less than a second

should run without any arguments should implicitly use:

• assumptions in the goal = local labels in the proof

• theorems from the formal library

the plan

creating a collection of mathematical problems

• take proofs from Proofs from The Book \overline{}

• create formal proof sketches of those proofs • calculate the proof obligations of the steps in

those formal proof sketches

• select proof obligations in the Content MathML signature

benchmark for math automation

the proof obligations for the Hardy & Wright example

\sqrt{2} ∈ ℚ ⊢ ∃ a, b ∈ ℤ (a^{2} = 2b^{2} ∧ gcd(a, b) = 1)
b ∈ ℤ ∧ a^{2} = 2b^{2} ⊢ 2 | a^{2}
a ∈ ℤ ∧ 2 | a^{2} ⊢ 2 | a
2 | a ⊢ ∃ c ∈ ℤ (a = 2c)
a^{2} = 2b^{2} ∧ a = 2c ⊢ 4c^{2} = 2b^{2}
4c^{2} = 2b^{2} ⊢ 2c^{2} = b^{2}
b ∈ ℤ ∧ c ∈ ℤ ∧ 2c^{2} = b^{2} ⊢ 2 | b
gcd(a, b) = 1 ∧ 2 | a ∧ 2 | b ⊢ ⊥

Content MathML signature only relevant subset of the assumptions shown here

each should be proved automatically in less than a second!