comparing mathematical provers

Freek Wiedijk University of Nijmegen

MKM 2003 University of Bologna Bertinoro

2003 02 18, 11:30

the project

it’s like collecting stamps

comparison book: same program in many programming languages comparison of provers: same small proof in many systems

concept ask ‘native speakers’ of each system for a ‘natural’ proof question & answer section about each system

main goal: show how different these systems can be

current state: 118 page report

  • web page: http://www.cs.kun.nl/~freek/comparison/

• will be: local Nijmegen report; maybe LNAI the lemma two canonical examples to explain the concept of ‘proof’

• infinity of primes (Euclid)

• irrationality of \sqrt{2} (Pythagoras) second is more interesting: real number library!

the two variants of the theorem full result: \sqrt{2} ∉ ℚ basic lemma: m^{2} = 2n^{2} ⟺ m = n = 0

the systems

ICT versus math

QED manifesto (1994): proof checking for mathematics

QED is the very tentative title of a project to build a computer system that effectively represents all important mathematical knowledge and techniques.

current proof assistants mostly designed and used for verification of hardware/software focus here: suitability for formalization of mathematics

systems one should seriously consider for the QED dream the 15 provers

HOL John Harrison Mizar Andrzej Trybulec PVS Bart Jacobs Coq Laurent Théry Otter/Ivy Michael Beeson Isabelle/Isar Markus Wenzel Alfa/Agda Thierry Coquand ACL2 Ruben Gamboa PhoX Christophe Raffalli IMPS William Farmer Metamath Norman Megill Theorema Markus Rosenkranz Lego Conor McBride NuPRL Paul Jackson Ωmega Christoph Benzmüller systems that didn’t make the list only one system from each evolutionary path

ALF, Half → Agda
Nqthm → ACL2
IMPS → MathScheme
Lego → Oleg, Plastic
NuPRL → MetaPRL

other systems

KIV, B method (more for ICT than for math)
Twelf, Typelab (more for logic than for math)
TPS  (not for a structured body of math)

the proofs

files

different kinds

input files definitions & statements proof scripts

output files pretty printed with mathematical symbols generated natural language proof objects (λ-terms)

comparison focuses on the files that the user interacts with comparison presents relevant fragments of the other files three examples

otter.in hol.ml mizar.miz 15 statements

• ~rational(sqrt(&2))
• sqrt 2 is irrational
• NOT Rational?(sqrt(2))
• (irrational (sqrt (S (S O))))
• m(a,a) = m(2,m(b,b))

• sqrt (real (2::nat)) ∉ ℚ

• prime p → noether A (multiple p) → isNotSquare p

• (implies (equal (* x x) 2) (and (realp x) (not (rationalp x))))
• /\m,n : N (m^N2 = N2 * n^N2 -> m = N0 & n = N0)
• not #(sqrt(2),qq)
• $p |- ( sqr ` 2_10 ) e/ QQ

• ¬rat[\sqrt{p}]

• {b|nat}{a|nat}(Eq (times two (times a a)) (times b b))->
                (Eq a zero /\ Eq b zero)
• ¬(∃u:ℚ. u *_{q} u = 2 / 1)
• (not (rat (sqrt 2)))

the diagram

three important dimensions

1. size of the library

2. mathematical nature, abstractness 3. level of automation size of the library development of library is much more work than development of system → should be main activity of the project! the only way to get a good system: exercise it in developing a library!

(strong player: Mizar) mathematical

• de Bruijn criterion = small kernel

• logical framework

• constructive versus classical

• first order, higher order, set/type theory • dependent types

(strong player: Coq) automation

• batch checker, LCF style tactic prover, automated theorem prover • Poincaré principle = user automation of calculations

• open architecture

• decision procedures

• proof search

(strong player: PVS) a Herzsprung-Russell diagram of proof checking

[figure: more automation; more mathematical; ACL2; PVS; Isabelle; HOL; Ωmega; Otter; Theorema; IMPS; NuPRL; Coq; PhoX; Lego; Mizar; Agda; Metamath]