\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.4,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\newpagestyle{fw}{}{\hfil\textcolor{slideblue}{\sf\thepage}\qquad\qquad}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{#1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\dashskip}{\strut\enskip{ }}
\newcommand{\exclspace}{\hspace{.45pt}}

\begin{document}\sf
\renewcommand{\sliderightmargin}{0mm}
\renewcommand{\slideleftmargin}{20mm}
\renewcommand{\slidebottommargin}{6mm}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large formal mathematics}

Freek Wiedijk \\
Nijmegen University

Leiden University \\
2002-10-10, 16:00
\end{slide}

\begin{slide}
\sectiontitle{proof checking}
\slidetitle{the best of two worlds}
a wonderful computer game\exclspace!
\adviwait

proof checking is like
\begin{itemize}
\item[$\bullet$]
  \textbf{programming} \\ but no bugs, and not as trivial\exclspace!
\item[$\bullet$]
  \textbf{doing mathematics} \\ but completely transparent, and the computer helps\exclspace!
\end{itemize}
\adviwait
(currently closer to programming than to doing mathematics)
\vfill
\end{slide}

\begin{slide}
\slidetitle{proof checking $\;\leftrightarrow\;$ mathematical assistants}
computer can help with:
\begin{itemize}
\item[$\bullet$]
  the discovery of mathematics
\item[\advirecord{reg1}{$\bullet$}]
\advirecord{reg2}{the registration of mathematics}
\adviplay{reg1}\adviplay{reg2}
\end{itemize}
\adviwait

\adviplay[slidered]{reg1}\adviplay[slidered]{reg2}
here only interested in the formalization of already existing mathematics
\medskip
\adviwait

\textbf{analogy}
\begin{center}
\begin{tabular}{rcl}
mathematician & $\leftrightarrow$ & proof checker \\
\advirecord{h1a}{violin player}\advirecord{h2a}{\llap{music composer}} & $\leftrightarrow$ & \advirecord{h1b}{\rlap{hifi sound technician}}\advirecord{h2b}{violin player}
\adviplay{h1a}\adviplay{h1b}
\adviwait
\adviplay[white]{h1a}\adviplay[white]{h1b}
\adviplay{h2a}\adviplay{h2b}
\end{tabular}
\end{center}
\vfill
\end{slide}

\begin{slide}
\slidetitle{what does proof checking buy me as a mathematician?}
currently:
\begin{itemize}
\item[$\bullet$]
  \textbf{nothing} \\
  the gains are not worth the effort yet
\end{itemize}
\adviwait

in the (near? far?) future:
\begin{itemize}
\item[$\bullet$]
  \textbf{correctness} \\
  certainty that lemmas are correct \\
\adviwait
  certainty that a paper is correct when submitted \\
    (the referees won't need to judge correctness anymore,
    but only originality and relevance)
\adviwait
\item[$\bullet$]
  \textbf{clarity} \\
  no need to ask the author of a text for clarification \\
    everything is there\exclspace!
\end{itemize}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{philosophy of reliability I:
the de Bruijn principle}
worry about own mistakes $\;\to\;$ worry about bugs in the checker?
\adviwait

analogous to compiler bugs in programming: \\
  software problems are hardly ever caused by compiler bugs
\medskip
\adviwait

\textbf{de Bruijn principle} \\
  check mathematics using a \textbf{small} checker
\medskip
\adviwait

two approaches:
\begin{itemize}
\item[$\bullet$]
  small `proof kernel' that everything has to go through \\
  (many current systems)
\adviwait
\item[$\bullet$]
  export in a format that can be checked by a small separate checker \\
  example: the Ivy program for the Otter prover
\end{itemize}
\vfill
\end{slide}

\begin{slide}
\slidetitle{philosophy of reliability II:
are we doing what we think we are doing?}
proofs are checked, but definitions can be `wrong'

definitions often are adapted for formalization \\
how to know that they still define the intended notions?
\medskip
\adviwait

\textbf{example} \\
definition of a planar graph in the four color theorem formalization: \\
no mention of the topology of the plane\exclspace!
\medskip
\adviwait

Trybulec: \textcolor{slidegreen}{definitions are a debt, theorems pay them back} \\
trust comes from the theory that is proved about the definitions
\vfill
\end{slide}

\begin{slide}
\slidetitle{the state of the art: mathematics that already has been formalized}
examples of formalized theorems:
\begin{quote}
$\bullet$ fundamental theorem of calculus \\
$\bullet$ fundamental theorem of algebra \\
$\bullet$ Taylor's theorem \\
$\bullet$ Hahn-Banach theorem \\
$\bullet$ Urysohn's lemma \\
$\bullet$ Stone's theorem (paracompactness of metrizable spaces) \\
$\bullet$ Stone's theorem (representations of boolean algebras) \\
$\bullet$ G\"odel's first incompleteness theorem \\
$\bullet$ reducibility of the configurations for the four color theorem \\
$\bullet$ correctness of Buchberger's algorithm \\
$\bullet$ fundamental theorem of Galois theory
\end{quote}
\adviwait

full translation (half finished) of a book on continuous lattices
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{how difficult is it?}
formalizing mathematics: trivial or undoable?
\medskip
\adviwait

some metrics: \\
de Bruijn factor = ratio between formalization and informal text
\begin{quote}
  currently: \textbf{4 times as big}
\end{quote}
\medskip
\adviwait

time needed to formalize a page from a textbook
\begin{quote}
  currently: \textbf{1 week}
\end{quote}
  (estimate: `all undergraduate math' will take 140 man-year)
\vfill
\end{slide}

\begin{slide}
\slidetitle{automation $\;\leftrightarrow\;$ human control}
\hbox to 0pt{\hskip\hsize{\vbox to 0pt{\vskip-.27cm\hbox to 0pt{\hss\includegraphics[0,0][100,136]{iceberg.jpg}}\vss}}\hss}%
mathematical reasoning is like an iceberg
\vspace{.29cm}

\hspace{1.8cm} \phantom{un}conscious part of reasoning $\longrightarrow$
\vspace{.12cm}

\hspace{1.8cm} unconscious part of reasoning $\longrightarrow$
\vspace{.85cm}
\adviwait

\textcolor{slidered}{the story of the formalizations of the \\ fundamental theorem of algebra}
\medskip
\adviwait

too much automation \\
`lost in proof space':
user doesn't understand the proof anymore \\
$\to\;$ formalizing becomes much harder
\adviwait

automation should focus on the unconscious part of the reasoning \\
automation should \textbf{not} amaze the user
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{can the computer prove things that human mathematicians cannot?}
EQP, 1996:
\begin{center}
\textcolor{slidegreen}{all Robbins algebras are Boolean}
\end{center}
\adviwait

the computer is:
\begin{itemize}
\item[$\bullet$]
  strong in combinatorial search through many cases
\item[$\bullet$]
  weak in goal oriented proof \\
  surprisingly trivial steps can't be proved automatically yet
\end{itemize}
\medskip
\adviwait

Shankar: focus on decision procedures instead of proof search \\
(decision procedure $=$ algorithm to answer a specific class of questions)
\begin{itemize}
\item[$\bullet$]
general purpose proof search doesn't work well
\item[$\bullet$]
domain specific proof generation is very useful
\end{itemize}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{three systems}
\slidetitle{\textbf{Coq}}
Huet \& Coquand, Paulin \\
INRIA, France \\
1984--today

implemented in the ocaml dialect of ML \\
advantages:
\begin{itemize}
\item[$\bullet$]
  popular for mathematics
\item[$\bullet$]
  powerful logic
\end{itemize}
\medskip
\adviwait

prehistoric precursor: Automath
\vfill
\end{slide}

\begin{slide}
\slidetitle{propositions as types, proofs as objects}
Coq's logic: type theory
\adviwait

  types with objects $\;\leftrightarrow\;$ propositions with proofs \\
  `Curry-Howard isomorphism'

proofs become first class objects \\
\adviwait
$\to\;$ proofs can be used as function arguments
\medskip

division modeled as a ternary function
  $$\mbox{\it div\/}(x,y,\mbox{`proof that $y\ne 0$'})$$
\adviwait
  with this kind of division it is impossible to write $1/0$ \\
    (no `proof object' for the third argument)
\vfill
\end{slide}

%\begin{slide}
%\slidetitle{reflection}
%logic is the mathematics of reasoning \\
%$\to\;$ logic is mathematics too
%
%possible to formalize logic \textbf{inside} a formal system
%\medskip
%\adviwait
%
%useful `trick' to implement provers (decision procedures) for Coq \\
%possible to prove provers correct \\
%generated proofs don't need to be checked anymore
%\medskip
%\adviwait
%
%`the two level approach'
%\begin{itemize}
%\item[$\bullet$]
%expressions representing mathematical objects
%\item[$\bullet$]
%expressions representing terms representing mathematical objects
%\end{itemize}
%(possibility to distinguish between `$(x + y)^2$' and `$x^2 + 2xy + y^2$')
%\vfill
%\end{slide}

\begin{slide}
\slidetitle{\textbf{HOL Light}}
recent reimplementation of the HOL system

Gordon, Harrison \& Slind \\
Cambridge, UK \\
1985--1995--today

implemented in the ocaml dialect of ML \\
advantages:
\begin{itemize}
\item[$\bullet$]
  simple and elegant
\item[$\bullet$]
  strong automation
\end{itemize}
\medskip
\adviwait

prehistoric precursor: LCF
\vfill
\end{slide}

\begin{slide}
\slidetitle{the de Bruijn principle in action}
HOL Light proof kernel: \\
285 lines of ML code = 8 pages of source text \\
  possible to really understand this
\medskip
\adviwait

\begin{quote}
\begin{verbatim}
type hol_type = Tyvar of string
              | Tyapp of string * hol_type list;;
\end{verbatim}
\begin{verbatim}
type term = Var of string * hol_type
          | Const of string * hol_type
          | Comb of term * term
          | Abs of term * term;;
\end{verbatim}
\begin{verbatim}
type thm = Sequent of (term list * term);;
\end{verbatim}
\end{quote}
\medskip
\adviwait

10 primitive proof rules + 3 axioms
\vfill
\end{slide}

\begin{slide}
\slidetitle{taking mathematical objects in your hands}
HOL proofs = programs in the ML programming language

variables hold `mathematical objects' and `proved theorems' \\
  (really: variables hold \textbf{terms} describing mathematical objects)
\begin{quote}
\verb|#|\adviwait\textcolor{slidered}{\tt let s = `\char`{x | x * x = \&2\char`}`;;} \\
\verb/s : term = `{x | x * x = &2}`/ \\
\verb|#|\adviwait\textcolor{slidered}{\tt let t = prove(`?x. x * x = \&2`,} \\
\textcolor{slidered}{\tt\ \ EXISTS\char`_TAC `sqrt(\&2)` THEN REWRITE\char`_TAC} \\
\textcolor{slidered}{\tt\ \ [GSYM POW\char`_2; SQRT\char`_POW2] THEN ARITH\char`_TAC);;} \\
\verb/t : thm = |- ?x. x * x = &2/ \\
\verb|#|
\end{quote}
\adviwait
  programming with mathematical objects instead of integers and reals
\vfill
\end{slide}

\begin{slide}
\slidetitle{\textbf{Mizar}}
Trybulec \& Bylinski \\
Bialystok, Poland \\
1973--1989--today

implemented in the Delphi dialect of Pascal \\
advantages:
\begin{itemize}
\item[$\bullet$]
  mathematics oriented
\item[$\bullet$]
  large library
\end{itemize}
\medskip
\adviwait

prehistoric precursor: Mizar
\vfill
\end{slide}

\begin{slide}
\slidetitle{readable proofs}
Mizar proofs can be read as text
\begin{quote}
\begin{verbatim}
per cases; suppose ex x st not P[x];
 then consider a such that A1: not P[a];
 take a; assume P[a]; hence thesis by A1;
suppose A2: for x holds P[x];
 consider a; take a; thus thesis by A2;
\end{verbatim}
\end{quote}
\medskip
\adviwait

proofs in most other systems are unreadable `code'
\begin{quote}
\begin{verbatim}
ASM_CASES_TAC `?x:A. ~P x` THEN
RULE_ASSUM_TAC (REWRITE_RULE[NOT_EXISTS_THM]) THENL
[POP_ASSUM (X_CHOOSE_TAC `a:A`); ALL_TAC] THEN
EXISTS_TAC `a:A` THEN ASM_REWRITE_TAC[]
\end{verbatim}
\end{quote}
\vfill
\end{slide}

\begin{slide}
\slidetitle{taking ZFC seriously}
\rlap{Bourbaki:}\phantom{de Bruijn: }ZFC = foundations in theory \\
\phantom{de Bruijn: }ZFC = foundations in practice\advirecord{?}{\rlap{?}}\advirecord{!}{\exclspace!}\adviplay{?}
\medskip

de Bruijn: ZFC doesn't match mathematical practice \\
  what is the meaning of the ${}\cap{}$ of a triangle and a number?
\medskip
\adviwait
\adviplay[white]{?}\adviplay{!}

Mizar shows: Bourbaki propaganda is true \\
  \textbf{it is practical to formalize real mathematics on a ZFC foundation}
\adviwait

\medskip
\begin{quote}
\begin{tabular}{lcr}
Mizar axioms (ZFC + inaccessibles) &$\to$& 28 lines \\
Mizar library &$\to$& 1,400,000 lines
\end{tabular}
\end{quote}
\medskip
(everything in the Mizar library is fully proved from the axioms)
\vfill
\end{slide}

\begin{slide}
\sectiontitle{an example in Mizar}
\slidetitle{Pythagorean triples}
a solution of
$$a^2 + b^2 = c^2$$
with no common divisors always has the form
$$a = m^2 - n^2 \qquad b = 2mn \qquad c = m^2 + n^2\medskip$$
\adviwait
\textbf{examples}
$$\begin{array}{ccrcrcr}
m = 2 \qquad n = 1 & \quad\to\quad & 3^2 & + & 4^2 & = & 5^2 \\
m = 3 \qquad n = 2 & \to & 5^2 & + & 12^2 & = & 13^2 \\
m = 4 \qquad n = 1 & \to & 15^2 & + & 8^2 & = & 17^2 \\
m = 4 \qquad n = 3 & \to & 7^2 & + & 24^2 & = & 25^2
\end{array}$$
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch}
\begin{flushleft}
\verb|reserve a,b,c,m,n for Nat;|
\end{flushleft}
\begin{flushleft}
\verb|let a,b,c; assume a^2 + b^2 = c^2;|\\
\verb|assume a,b are_relative_prime;|\\
\adviwait
\verb|then a is odd or b is odd;|\adviwait\verb| assume a is odd;|
\adviwait
\end{flushleft}
\begin{flushleft}
\verb|ex m,n st a = m^2 - n^2 & b = 2*m*n & c = m^2 + n^2|\\
\verb|proof|\\
\adviwait
\verb| b is even; c is odd;|\\
\adviwait
\verb|X: (c + a)/2,(c - a)/2 are_relative_prime;|\\
\adviwait
\verb| ((c + a)/2)*((c - a)/2) = (c^2 - a^2)/4 .= (b/2)^2;|\\
\verb| then ((c + a)/2)*((c - a)/2) is square;|\\
\adviwait
\verb| then (c + a)/2 is square & (c - a)/2 is square by X;|\\
\verb| consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;|
\verb| take m,n;|\\
\end{flushleft}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal proof sketch (continued)}
\begin{flushleft}
\begin{color}{slidegray}
\verb| consider m,n such that m^2 = (c + a)/2 & n^2 = (c - a)/2;|\\
\verb| take m,n;|\\
\end{color}
\verb| thus a = (c + a)/2 - (c - a)/2 .= m^2 - n^2;|\\
\verb| b^2 = (c + a)*(c - a) .= 4*m^2*n^2 .= (2*m*n)^2;|\\
\verb| hence b = 2*m*n;|\\
\verb| thus c = (c + a)/2 + (c - a)/2 .= m^2 + n^2;|\\
\verb|end;|
\end{flushleft}
\adviwait
%\medskip
syntactically correct Mizar \\
semantically correct Mizar \\
too high level: Mizar cannot check the correctness
\adviwait
\begin{itemize}
\item[$\bullet$]
   steps are too big for Mizar
\item[$\bullet$]
   links between steps are missing
\end{itemize}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{a fragment of the full proof}
\begin{flushleft}
\advirecord{x1}{\tt\ then}\\
\advirecord{x2}{\tt X: (c + a)/2,(c - a)/2 are\char`_relative\char`_prime}\advirecord{x3}{\tt\ by Lm3}\advirecord{x4}{;}\\
\advirecord{x5}{\tt\ ((c + a)/2)*((c - a)/2) =}\advirecord{x6}{\tt\ ((c + a)*(c - a))/(2*2)}\\
\advirecord{x7}{\ \ \ by }\advirecord{x7a}{REAL\char`_1:35}\\
\advirecord{x8}{\ \ .= }\advirecord{x9}{\tt (c\^{}2 - a\^{}2)/4}\advirecord{x10}{\tt\ by }\advirecord{x10a}{SQUARE\char`_1:67}\\
\advirecord{x11}{\tt\ \ .= (b\^{}2)/(2*2)}\advirecord{x12}{\tt\ by H1,}\advirecord{x12a}{INT\char`_1:3}\\
\advirecord{x13}{\tt\ \ .= (b\^{}2)/(2\^{}2)}\advirecord{x14}{\tt\ by }\advirecord{x14a}{SQUARE\char`_1:def 3}\\
\advirecord{x15}{\tt\ \ .= (b/2)\^{}2}\advirecord{x16}{\tt\ by }\advirecord{x16a}{SQUARE\char`_1:69}\advirecord{x17}{\tt;}\\
\advirecord{x18}{\tt\ then ((c + a)/2)*((c - a)/2) is square}\advirecord{x19}{\tt\ by A1,Def1}\advirecord{x20}{\tt ;}\\
\advirecord{x21}{\tt\ then (c + a)/2 is square \& (c - a)/2 is square by X}\advirecord{x22}{\tt ,Lm4}\advirecord{x23}{\tt ;}\\
\advirecord{x24}{\tt\ then (ex m st m\^{}2 = (c + a)/2) \&}\\
\advirecord{x25}{\tt\ \ (ex n st n\^{}2 = (c - a)/2)}\advirecord{x26}{\tt\ by Def1}\advirecord{x27}{\tt ;}\\
\advirecord{x28}{\tt\ then }\advirecord{x29}{\tt consider m,n such that}\\
\advirecord{x30}{\tt A9:}\advirecord{x31}{\tt\ m\^{}2 = (c + a)/2 \& n\^{}2 = (c - a)/2;}
\end{flushleft}
\adviplay{x2}
\adviplay{x4}
\adviplay{x5}
\adviplay{x9}
\adviplay{x15}
\adviplay{x17}
\adviplay{x18}
\adviplay{x20}
\adviplay{x21}
\adviplay{x23}
\adviplay{x29}
\adviplay{x31}
\adviwait
\adviplay[slidered]{x6}
\adviplay[slidered]{x8}
\adviplay[slidered]{x11}
\adviplay[slidered]{x13}
\adviplay[slidered]{x24}
\adviplay[slidered]{x25}
\adviplay[slidered]{x27}
\adviwait
\adviplay[slidered]{x1}
\adviplay[slidered]{x3}
\adviplay[slidered]{x7}
\adviplay[slidered]{x7a}
\adviplay[slidered]{x10}
\adviplay[slidered]{x10a}
\adviplay[slidered]{x12}
\adviplay[slidered]{x12a}
\adviplay[slidered]{x14}
\adviplay[slidered]{x14a}
\adviplay[slidered]{x16}
\adviplay[slidered]{x16a}
\adviplay[slidered]{x19}
\adviplay[slidered]{x22}
\adviplay[slidered]{x26}
\adviplay[slidered]{x28}
\adviplay[slidered]{x30}
\adviwait
\adviplay{x6}
\adviplay{x8}
\adviplay{x11}
\adviplay{x13}
\adviplay{x24}
\adviplay{x25}
\adviplay{x27}
\adviplay{x1}
\adviplay{x3}
\adviplay{x7}
\adviplay{x7a}
\adviplay{x10}
\adviplay{x10a}
\adviplay{x12}
\adviplay{x12a}
\adviplay{x14}
\adviplay{x14a}
\adviplay{x16}
\adviplay{x16a}
\adviplay{x19}
\adviplay{x22}
\adviplay{x26}
\adviplay{x28}
\adviplay{x30}
\adviwait
\adviplay[slidered]{x7a}
\adviplay[slidered]{x10a}
\adviplay[slidered]{x12a}
\adviplay[slidered]{x14a}
\adviplay[slidered]{x16a}
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal mathematics can talk about `higher' objects}
claim: \textbf{any} mathematics can be formalized

not only about basic objects like numbers and numeric functions \\
objects can be abstract and `large'
\medskip
\adviwait

example: Yoneda lemma
\begin{quote}
\verb|definition let A be |\advirecord{y1}{\tt Category}\adviplay{y1}\verb|;|\\
\verb| func Yoneda(A) ->|\\
\verb|   |\advirecord{y2}{\tt Contravariant\char`_Functor}\adviplay{y2}\verb| of A,Functors(A,EnsHom(A))|\\
\verb|  means|\\
\verb|   for f being Morphism of A holds|\\
\verb/    it.f = [[<|cod f,?>,<|dom f,?>],<|f,?>];/\\
\verb|end;|
\end{quote}
\medskip
\adviwait
\adviplay[slidered]{y1}\adviplay[slidered]{y2}
\adviwait

observation: abstract math is easier to formalize than basic math
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\sectiontitle{conclusion}
\slidetitle{isn't this all just engineering?}
this talk: the user's point of view
\medskip
\adviwait

\textbf{research topics}

\begin{itemize}
\item[$\bullet$]
the theory of logical foundations

logics: paradoxes, consistency, conservativity  \\
\adviwait
type systems: confluence, termination, subject reduction
\adviwait

\item[$\bullet$]
the theory of proof search
\adviwait

\item[$\bullet$]
the theory of decision procedures

interaction between decision procedures \\
\adviwait
moving the decision procedures \textbf{inside} the logic: reflection

\end{itemize}
\medskip
\adviwait
but: `just engineering' is also important to get a usable system
\vspace{-2em}
\vfill
\end{slide}

\begin{slide}
\slidetitle{it might not be for you yet, but it's serious\exclspace!}
\begin{itemize}
\item[$\bullet$]
  not yet practical
\item[$\bullet$]
  interesting developments
\item[$\bullet$]
  it might change the (mathematical) world
\end{itemize}
\bigskip
\adviwait

\begin{itemize}
\item[$\bullet$]
  ancient Greeks: invention of proof
\item[$\bullet$]
  nineteenth century: invention of rigor
\item[$\bullet$]
  \textbf{today?}
\end{itemize}
\vfill
\end{slide}

\end{document}