formalization of mathematics

Freek Wiedijk Radboud University Nijmegen

TYPES Summer School 2005 Göteborg, Sweden 2005 08 23, 11:10

intro

the best of two worlds

formalization of mathematics is like:

• computer programming

concrete, explicit

a formalization is much like a computer program

• doing mathematics

abstract, non-trivial

a formalization is much like a mathematical textbook

you will like it only if you like both programming and mathematics but in that case you will like it very very much! table of contents: the two parts of this talk

first hour: an overview of the current state of the art in formalization of mathematics

in the reader: QED manifesto

second hour: an overview of Mizar, the most ‘mathematical’ proof assistant

in the reader: Mizar tutorial

first hour: state of the art in formalization of mathematics

mathematics in the computer

four ways to do mathematics in the computer

• numerical mathematics, experimentation, visualisation calculations numbers: computer → human

• computer algebra calculations formulas: computer → human

• automated theorem provers proofs: computer → human

• proof assistants proofs: human → computer numerical mathematics: Merten’s conjecture Möbius function:

μ(n) = \{ \begin{matrix}0 & when n has duplicate prime factors \\ 1 & when n has an even number of different prime factors \\ −1 & when n has an odd number of different prime factors \end{matrix}

Mertens, 1897:  | ∑_{k=1}^{n} μ(n)| < \sqrt{n} ?

Merten’s conjecture (continued)

Odlyzko & te Riele, 1985: Mertens conjecture is false! 50 uur computer time

first n where it fails has tens of digits indirect proof!

2000 zeroes of the Riemann zeta function to 100 decimals precision

14.1347251417346937904572519835624702707842571156992431756855674601499634298092567649490103931715610127… 21.0220396387715549926284795938969027773343405249027817546295204035875985860688907997136585141801514195… 25.0108575801456887632137909925628218186595496725579966724965420067450920984416442778402382245580624407… 30.4248761258595132103118975305840913201815600237154401809621460369933293893332779202905842939020891106… 32.9350615877391896906623689640749034888127156035170390092800034407848156086305510059388484961353487245… 37.5861781588256712572177634807053328214055973508307932183330011136221490896185372647303291049458238034… 40.9187190121474951873981269146332543957261659627772795361613036672532805287200712829960037198895468755… 43.3270732809149995194961221654068057826456683718368714468788936855210883223050536264563493710631909335… 48.0051508811671597279424727494275160416868440011444251177753125198140902164163082813303353723054009977… 49.7738324776723021819167846785637240577231782996766621007819557504335116115157392787327075074009313300… 52.9703214777144606441472966088809900638250178888212247799007481403175649503041880541375878270943992988… 56.4462476970633948043677594767061275527822644717166318454509698439584752802745056669030113142748523874… 59.3470440026023530796536486749922190310987728064666696981224517547468001526996298118381024870746335484… 60.8317785246098098442599018245240038029100904512191782571013488248084936672949205384308416703943433565… 65.1125440480816066608750542531837050293481492951667224059665010866753432326686853844167747844386594714… 67.0798105294941737144788288965222167701071449517455588741966695516949012189561969835302939750858330343… 69.5464017111739792529268575265547384430124742096025101573245399996633876722749104195333449331783403563… 72.0671576744819075825221079698261683904809066214566970866833061514884073723996083483635253304121745329… 75.7046906990839331683269167620303459228119035306974003016477753015741970277063236083840370218346527980… 77.1448400688748053726826648563046370157960324492344610417652314531511391642537150894082886946997377597… 79.3373750202493679227635928771162281906132467431200308784387204971015419326770909746774519946121241090… 82.9103808540860301831648374947706094975088805937821491465713062832359290863566190755125631923348968187… …

6

computer algebra: symbolic integration of ∫_{0}^{∞} \frac{e^{−(x−1)^{2}}}{\sqrt{x}} dx

> int(exp(-(x-t)^2)/sqrt(x), x=0..infinity);

\frac{1}{2} \frac{e^{−t^{2}}(−^{\frac{3(t^{2})^{\frac{1}{4}} π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{t^{2}}{2}} K_{\frac{3}{4}} ( \frac{t^{2}}{2} )}{t^{2}}} + (t^{2})^{\frac{1}{4}} π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{t^{2}}{2}} K_{\frac{7}{4}} (\frac{t^{2}}{2} ))}{π^{\frac{1}{2}}}

> subs(t=1,%);

\frac{1}{2} \frac{e^{−1}(−3π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{1}{2}} K_{\frac{3}{4}} (\frac{1}{2}) + π^{\frac{1}{2}} 2^{\frac{1}{2}} e^{\frac{1}{2}} K_{\frac{7}{4}} (\frac{1}{2}))}{π^{\frac{1}{2}}}

> evalf(%);

0.4118623312

> evalf(int(exp(-(x-1)^2)/sqrt(x), x=0..infinity));

1.973732150 automated theorem proving: Robbins’ conjecture

computers … can in the near future play chess better than a human … can in the near future do mathematics better than a human?

Robbins, 1933: is every Robbins algebra a Boolean algebra?
EQP, 1996: yes!

eight days of computer time

one of the very few proofs that has first been found by a computer not very conceptual: just searches through very many possibilities

interesting research, but currently not relevant for mathematics

the QED manifesto

let’s formalize all of mathematics!

QED manifesto, 1994:

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

pamphlet by anonymous group, led by Bob Boyer utopian vision

proposed many times never got very far (yet) the two kinds of computer proof

• correctness of computer software and hardware (serious branch of computer science: ‘formal methods’)

statements: big proofs: shallow computer does the main part of the proof

• correctness of mathematical theorems (slow and thorough style of doing mathematics, still in its infancy)

statements: small proofs: deep human does the main part of the proof

a brief overview of proof assistants for mathematics four prehistorical systems

1968 Automath

Netherlands, de Bruijn

1971 nqthm

US, Boyer & Moore

1972 LCF

UK, Milner

1973 Mizar

Poland, Trybulec seven current systems for mathematics

[figure: Mizar; most mathematical; LCF; HOL; Isabelle; most pure; Automath; Coq NuPRL; most logical; PVS; most popular; nqthm; ACL2; most computational]

a ‘top 100’ of mathematical theorems

1. The Irrationality of the Square Root of 2 ← all systems
2. Fundamental Theorem of Algebra ← Mizar, HOL, Coq
3. The Denumerability of the Rational Numbers ← Mizar, HOL, Isabelle
4. Pythagorean Theorem ← Mizar, HOL, 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 ← Mizar, HOL, Isabelle
. . . . . .

63% formalized

            http://www.cs.ru.nl/^{∼}freek/100/

(advertisement) the seventeen provers of the world

LNAI 3600

one theorem seventeen formalisations + explanations about the systems

HOL, Mizar, PVS, Coq, Otter, Isabelle, Agda, ACL2, PhoX, IMPS, Metamath, Theorema, Lego, NuPRL, Ωmega, B method, Minlog

          http://www.cs.ru.nl/^{∼}freek/comparison/

state of the art: recent big formalizations

Prime Number Theorem

Bob Solovay’s challenge:

I suspect that fully formalizing the usual proof of the prime usual proof of the prime number theorem […] is beyond the current capacities of the [formalization] community. Say within the next ten years.

Jeremy Avigad e.a.:

   "pi(x) == real(card(y. y<=x & y:prime))"
   "(%x. pi x * ln (real x) / (real x)) ----> 1"

1 megabyte = 30,000 lines = 42 files of Isabelle/HOL the elementary proof by Selberg from 1948 Four Color Theorem

Georges Gonthier:

   (m : map) (simple_map m) -> (map_colorable (4) m)

2.5 megabytes = 60,000 lines = 132 files of Coq 7.3.1 streamlined proof by Robertson, Sanders, Seymour & Thomas from 1996

• contains interesting mathematics as well ‘planar hypermaps’

• very interesting ‘own’ proof language on top of Coq

    Move=> x' p'; Elim: p' x' => [|y' p' Hrec] x' //=; Rewrite: ~Hrec.
    By Congr andb; Congr orb; Rewrite: /eqdf (monic2F_eqd (f_finv (Inode g'))).

• heavily relies on reflection ‘this formalization really needs Coq’ Jordan Curve Theorem

Tom Hales:

    `!C. simple_closed_curve top2 C ==>
       (?A B.  top2 A /\ top2 B /\
         connected top2 A /\ connected top2 B /\
       ~(A = EMPTY) /\ ~(B = EMPTY) /\
        (A INTER B = EMPTY) /\ (A INTER C = EMPTY) /\
            (B INTER C = EMPTY) /\
           (A UNION B UNION C = euclid 2))`

2.1 megabytes = 75,000 lines = 15 files of HOL Light proof through the Kuratowski characterization of planarity

• ‘warming up exercise’ for the Flyspeck project

• beat the Mizar project at formalizing this first

• also uses an ‘own’ proof style

state of the art: current big projects

the continuous lattices formalization

formalize a complete ‘advanced’ mathematics textbook

A Compendium of Continuous Lattices

by Gierz, Hofmann, Keimel, Lawson, Mislove & Scott

[…] For if not, then V ⊆ ⋃{L \ ↓v : v ∈ V }; and by quasicompactness and the fact that the L \ ↓v form a directed family, there would be a v ∈ V with V ⊆ L \ ↓v, notably v ∉ V, which is impossible. […]

project led by Grzegorz Bancerek

about 70% formalized 4.4 megabytes = 127,000 lines = 58 files of Mizar the Flyspeck project

Kepler in strena sue de nive sexangula, 1661:

is the way one customarily stacks oranges the most efficient way to stack spheres?

Tom Hales, 1998: yes !

proof: depends on computer checking 3 gigabytes programs & data, couple of months of computer time

referees say to be 99% certain that everything is correct

FlysPecK project ‘Formal Proof of Kepler’

so why did the qed project not take off?

reason one: differences between systems

foundations differ very much

set theory ⟷ type theory ⟷ higher order logic ⟷ PRA classical ⟷ constructive extensional ⟷ intensional impredicative ⟷ predicative choice ⟷ only countable choice ⟷ no choice

two utopias simultaneously?

• formalization of mathematics

• doing mathematics in weak logics (advertisement) a questionnaire about intuitionism

               http://www.intuitionism.org/

ten questions about intuitionism currently: seventeen sets of answers by various people

3. Do you agree that there are only three infinite cardinalities?

7. Do you agree that for any two statements the first implies the second or the second implies the first?

putting systems together

OMDoc XML standard for encoding of mathematical documents developed by Michael Kohlhase can be used both for natural language documents and for formalizations modularized language architecture supports both OpenMath and Content MathML encoding of formulas does not really address semantical differences between systems Logosphere converting between the foundations of various systems project led by Carsten Schürmann formalize foundations of each system in the Twelf logical framework translate all formalizations into Twelf use Twelf to relate those formalizations systems that are currently supported:

• first order resolution provers

• HOL

• NuPRL

• PVS

reason two: why mathematicians are not interested (yet) 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 the gain is too little

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 we just have 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? and it does not look like mathematics

most systems: ‘proof’ = list of tactics = unreadable computer code even in Mizar and Isar: 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)

so what is needed most to promote formalization of mathematics?

• decision procedures very important, main strength of PVS

• in particular: 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

second hour: a tour of Mizar, a proof assistant for mathematics

why is Mizar interesting?

• a system for mathematicians

• the proof language only other system with similar language: Isabelle/Isar

• many other interesting ideas

– type system soft typing ‘attributes’ multiple inheritance between structure types

– expression syntax type directed overloading bracket-like operators arbitrary ASCII strings for operators

example formalizations

example: Coq version

Definition ge (n m : nat) : Prop :=
  exists x : nat, n = m + x.
Infix ">=" := ge : nat_scope.
Lemma ge_trans :
  forall n m p : nat, n >= m -> m >= p -> n >= p.
Proof.
 unfold ge. intros n m p H H0.
 elim H. clear H. intros x H1.
 elim H0. clear H0. intros x0 H2.
 exists (x0 + x).
 rewrite plus_assoc. rewrite <- H2. auto.
Qed.

example: Mizar version

reserve n,m,p,x,x0 for natural number;
definition let n,m;
 pred n >= m means :ge: ex x st n = m + x;
end;
theorem ge_trans: n >= m & m >= p implies n >= p
proof
 assume that H: n >= m and H0: m >= p;
 consider x such that H1: n = m + x by H,ge;
 consider x0 such that H2: m = p + x0 by H0,ge;
 n = p + (x + x0) by H1,H2;
 hence n >= p by ge;
end;

procedural versus declarative

0  ∞

• procedural

E E S E N E S S S W W W S E E E

HOL, Isabelle, Coq, NuPRL, PVS

• declarative

(0,0) (1,0) (2,0) (3,0) (3,1) (2,1) (1,1) (0,1) (0,2) (0,3) (0,4) (1,4) (1,3) (2,3) (2,4) (3,4) (4,4)

Mizar, Isabelle another small example

If every poor person has a rich father,

then there is a rich person with a rich grandfather.

assume that
A1: for x st x is poor holds father(x) is rich and
A2: not ex x st x is rich & father(father(x)) is rich;
consider p being person;
now let x;
 x is poor or father(father(x)) is poor by A2;
 hence father(x) is rich by A1;
end;
then father(p) is rich & father(father(father(p))) is rich;
hence contradiction by A2;

demo example

Theorem. There are irrational numbers x and y such that x^{y} is rational.

Proof. We have the following calculation

(\sqrt{2}^{\sqrt{2}})^{\sqrt{2}} = \sqrt{2}^{\sqrt{2}·\sqrt{2}} = \sqrt{2}^{2} = 2

which is rational. Furthermore Pythagoras showed that \sqrt{2} is irrational. Now there are two cases:

• Either \sqrt{2}^{\sqrt{2}} is rational. Then take x = y = \sqrt{2}.

• Or \sqrt{2}^{\sqrt{2}} is irrational. In that case take x = \sqrt{2}^{\sqrt{2}} and y = \sqrt{2}. And by the above calculation then x^{y} = 2, which is rational. □ lemmas used in the proof

AXIOMS:22  x ≤ y ∧ y ≤ z ⇒ x ≤ z

INT_2:44  2 is prime

IRRAT_1:1  p is prime ⇒ \sqrt{p} ∉ ℚ
POWER:38  a > 0 ⇒ (a^{b})^{c} = a^{bc}

SQUARE_1:def 3  x^{2} = x · x

SQUARE_1:def 4  0 ≤ a ⇒ (x = \sqrt{a} ⇔ 0 ≤ x ∧ x^{2} = a)

SQUARE_1:84  1 < \sqrt{2}
POWER:53  ‘ a to_power 2 = a^2 ’

DEMO

example of how Mizar is like English

Hardy & Wright, An Introduction to the Theory of Numbers

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. □

Mizar language approximation of this text

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 Mizar

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;

some explanations about Mizar

the proof language forward reasoning ⟨statement⟩ by ⟨references⟩ ⟨statement⟩ proof ⟨steps⟩ end natural deduction

thus ⟨statement⟩  → closes the proof
assume ⟨statement⟩  → →-introduction
let ⟨variable⟩  → ∀-introduction
thus ⟨statement⟩  → ∧-introduction
consider ⟨variable⟩ such that ⟨statement⟩ → ∃-elimination
take ⟨term⟩  → ∃-introduction
per cases; suppose ⟨statement⟩; …  → ∨-elimination

‘semantics’?

Mizar is just first order predicate logic + set theory Mizar proofs are just Fitch-style natural deduction

but:

• Mizar variables have types… … and these types are quite powerful!

• Mizar has ‘second-order theorems’ called schemes

• Mizar defines function symbols using something like Church’s ι operator (‘unique choice’)

Tarski-Grothendieck set theory

TARSKI:def 3  X ⊆ Y ⇔ (∀x. x ∈ X ⇒ x ∈ Y)
TARSKI:def 5  ⟨x, y⟩ = {{x, y}, {x}}
TARSKI:def 6  X ∼ Y ⇔ ∃Z. (∀x. x ∈ X. ⇒ ∃y. y ∈ Y ∧ ⟨x, y⟩ ∈ Z) ∧
(∀y. y ∈ Y. ⇒ ∃x. x ∈ X ∧ ⟨x, y⟩ ∈ Z) ∧
(∀x∀y∀z∀u. ⟨x, y⟩ ∈ Z ∧ ⟨z, u⟩ ∈ Z ⇒ (x = z ⇔ y = u))

TARSKI:def 1  x ∈ {y} ⇔ x = y

TARSKI:def 2  x ∈ {y, z} ⇔ x = y ∨ x = z
TARSKI:def 4  x ∈ ⋃ X ⇔ ∃Y. x ∈ Y ∧ Y ∈ X
TARSKI:2  (∀x. x ∈ X ⇔ x ∈ Y) ⇒ X = Y
TARSKI:7  x ∈ X ⇒ ∃Y. Y ∈ X ∧ ¬∃x. x ∈ X ∧ x ∈ Y
TARSKI:sch 1  (∀x ∀y ∀z. P [x, y] ∧ P [x, z] ⇒ y = z) ⇒
(∃X. ∀x. x ∈ X ⇔ ∃y. y ∈ A ∧ P [y, x])
TARSKI:9  ∃M. N ∈ M ∧ (∀X∀Y. X ∈ M ∧ Y ⊆ X ⇒ Y ∈ M) ∧
(∀X. X ∈ M ⇒ ∃Z. Z ∈ M ∧ ∀Y. Y ⊆ X ⇒ Y ∈ Z) ∧
(∀X. X ⊆ M ⇒ X ∼ M ∨ X ∈ M)

types! Mizar is based on set theory but it is a typed system Mizar types are soft types:

M : N(t_{1}, …, t_{n})

should really be read as a predicate N(t_{1}, …, t_{n}, M)

This means that:

• one Mizar term can have many different types at the same time • a Mizar typing can be used as a logical formula!

        let x be Real;  ⟷  assume not x is Nat;

types! (continued) think of Mizar types as predicates that the system keeps track of for you Mizar types are used for three things:

• type based overloading

x + y sum of two numbers
X + Y adding the elements of two sets
X + y mixing these two things
v + w sum of two elements of a vector space
I + J sum of two ideals in a ring
x + y ‘join’ of two elements of a lattice
p + i adding an offset to a pointer

• inferring implicit arguments

• automatic inference of propositions types! (continued)

• Mizar has dependent types (much like in all the other dependent type systems)

• Mizar has a subtype relation every type except the type ‘set’ has a supertype

• Mizar has ‘type modifiers’ called attributes a type can be prefixed with one or more adjectives an adjective is either an attribute or the negation of an attribute (behaves like intersection types)

         non empty  finite

                              \underline{Subset} of NAT

notation

any ASCII string can be used for a Mizar operator

func ].a,b.] -> Subset of REAL means
:: MEASURE5:def 3
 for x being R_eal holds
  x in it iff (a <' x & x <=' b & x in REAL);
pred a,b are_convergent<=1_wrt R means
:: REWRITE1:def 9
 ex c being set st ([a,c] in R or a = c) & ([b,c] in R or b = c);

Mizar in the world

Mizar Mathematical Library the biggest library of formalized mathematics

49,588 lemmas
1,820,879 lines of ‘code’
64 megabytes
165 ‘authors’
912 ‘articles’

Mizar, the program

• implemented in Delphi Pascal/Free Pascal

• source not freely available, but

write Mizar ‘article’ ↓ become member of Association of Mizar Users ↓ get source

• no small proof checking ‘kernel’ correctness of Mizar check depends on correctness of whole program

• users can not automate proofs inside the system publishing formalizations: MML and FM

Mizar Mathematical Library

    theorem :: RUSUB_2:35
    for V being RealUnitarySpace, W being Subspace of V,
     L being Linear_Compl of W holds
      V is_the_direct_sum_of L,W & V is_the_direct_sum_of W,L;

Formalized Mathematics

(35) Let V be a real unitary space, W be a subspace of V, and L be a linear complement of W. Then V is the direct sum of L and W and the direct sum of W and L.

Mizar versus Isar some reasons to prefer Mizar over Isar

• the set theory of Mizar is much more powerful and expressive than the HOL logic of Isabelle/HOL

• Mizar is much more able to talk about abstract mathematics, and in particular about algebraic structures, with nice notation

• dependent types are way cool some reasons to prefer Isar over Mizar

• Isabelle gives you an interactive system

• Isabelle allows you to mix declarative and procedural proof

• Isabelle has much more possibilities of automation

• Isabelle allows you to define binders is Mizar a difficult system?

no, not difficult at all!

Mizar is about as complex as the Pascal programming language (proof assistants tend to resemble their implementation language)

reasons that people sometimes think Mizar is a complex language • lack of proper documentation

• natural language-like syntax

extro

gazing into the crystal ball Henk’s futuristic QED questions

• will proof assistants ever become common among mathematicians?

• if so: when will this happen?

– the most optimistic answer: it already is here!

– the experienced user’s answer: fifty years

but what do you expect?