when will it happen?

Freek Wiedijk University of Nijmegen

Automath Digital Archive Opening Symposium University of Eindhoven 2004 05 26, 15:10

five heirs to Automath

the first heir: Agda, the user experience

formalization = lambda term

Swedish system by Thierry & Catarina Coquand:

Alf → Half → C-Half → Alfa / Agda

serious mathematics: C-Half by Dan Synek formalization of the Hahn-Banach theorem by Jan Cederquist constructive mathematics ‘almost, but not quite, entirely unlike mathematics’ the second heir: Twelf, the logical framework

Automath ≈ λP = LF

Automath restaurant

vegetarian food is for a restaurant what constructive mathematics is for a proof checker

‘logical framework’ three very different logical frameworks: LF, Isabelle, Metamath

implementation of LF by Frank Pfenning and Carsten Schürmann used for computer science, not really used for mathematics the third heir: Metamath, the system

fully transparent & lightning fast

everything is defined in the formalization (even alpha conversion!) private system of Norman Megill implemented in C: checks its whole library in a few seconds

→ like the Automath implementation by FW various logics: ZFC set theory, quantum logic library of mathematics from ZFC up to the complex numbers

→ like Landau’s Grundlagen der Analysis the fourth heir: Mizar, the goal

let’s do real mathematics!

biggest library of formalized mathematics in the world 46,000 lemmas 1.7 million lines 60 megabytes

Polish system by Andrzej Trybulec based on ZFC set theory really looks like mathematics: mathematical mode

→ formal proof sketches the fifth heir: HOL Light, the de Bruijn criterion

the best proof checker of the world

collection of formalizations of irrationality of \sqrt{2} in sixteen systems Mizar and HOL Light: shortest formalizations & came in first

private reimplementation of HOL by John Harrison very small kernel: nine pages of ML including comments

strong automation: LCF approach

serious library of mathematics one of the three formalizations of the Fundamental Theorem of Algebra system selected for Flyspeck

it will happen

let’s formalize mathematics!

Automath Mizar QED manifesto MBase C-CoRN …

until now it just remains promises for the future

real mathematicians are not yet interested (and we ourselves don’t formalize our proofs either!)

why doesn’t it take off? what’s missing?

why are mathematicians not interested?

it just takes much too long … (the cost is too high)

de Bruijn factor = \frac{size of formalization}{size of normal text}

question: is this a constant?

experimental: around 4

de Bruijn factor in time = \frac{time to formalize}{time to understand} much larger than 4 formalizing one textbook page ≈ 1 man·week = 40 man·hours … and what’s the use? (the benefit is too low)

l’art pour l’art

Paul Libbrecht in Saarbrücken: ‘mental masturbation’

it’s not impossibly expensive formalizing all of undergraduate mathematics ≈ 140 man·years the price of about one Hollywood movie

but: after formalization one just has a big incomprehensible file we don’t have a good argument yet for spending that money

certainty that it’s fully correct?

is that important enough to pay for 140 man·years? it doesn’t resemble mathematics! (not my business)

most systems: proof = list of tactics = unreadable computer code even in ‘mathematical mode’ systems: still looks like code

even formulas: too much ‘decoding’ needed to understand what it says

  Variable J : interval.     Hypothesis pJ : proper J.
  Variable F, G : PartIR.    Hypothesis derG : Derivative J pJ G F.
  Let G_inc := Derivative_imp_inc ____derG.
  Theorem Barrow : forall a b (H : Continuous_I (Min_leEq_Max a b) F) Ha Hb,
   let Ha' := G_inc a Ha in let Hb' := G_inc b Hb in
   Integral H [=] G b Hb'[-]G a Ha'.

G′ = F ⇒ ∫_{a}^{b} F (x) dx = G(b) − G(a)

another barrier: you won’t sell intuitionism to classical mathematicians

so what is needed most?

automation • proof search: not very powerful, not very important

• decision procedures: very important, main strength of PVS computer algebra macsyma, maple, mathematica (really: computer calculus) high school mathematics should be trivial!

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