\documentclass[a4]{seminar}
\usepackage{advi}
\usepackage{advi-graphicx}
\usepackage{color}
\usepackage{amssymb}
%\usepackage[all]{xypic}
\usepackage{alltt}
\usepackage{url}

\slideframe{none}
\definecolor{slideblue}{rgb}{0,0,.5}
\definecolor{slidegreen}{rgb}{0,.5,0}
\definecolor{slidered}{rgb}{1,0,0}
\definecolor{slidegray}{rgb}{.5,.5,.5}
\definecolor{slidedarkgray}{rgb}{.4,.4,.4}
\definecolor{slidelightgray}{rgb}{.8,.8,.8}
\def\black#1{\textcolor{black}{#1}}
\def\white#1{\textcolor{white}{#1}}
\def\blue#1{\textcolor{slideblue}{#1}}
\def\green#1{\textcolor{slidegreen}{#1}}
\def\red#1{\textcolor{slidered}{#1}}
\def\gray#1{\textcolor{slidegray}{#1}}
\def\lightgray#1{\textcolor{slidelightgray}{#1}}
\def\darkgray#1{\textcolor{slidedarkgray}{#1}}
\newpagestyle{fw}{}{\hss\vbox to 0pt{\vspace{0.25cm}\llap{\blue{\sf\thepage}\hspace{0.1cm}}\vss}\strut}
\slidepagestyle{fw}
\newcommand{\sectiontitle}[1]{\centerline{\textcolor{slideblue}{\textbf{#1}}}
\par\medskip}
\newcommand{\slidetitle}[1]{{\textcolor{slideblue}{\strut #1}}\par
\vspace{-1.2em}{\color{slideblue}\rule{\linewidth}{0.04em}}}
\newcommand{\quadskip}{{\tiny\strut}\quad}
\newcommand{\dashskip}{{\tiny\strut}\enskip{ }}
\newcommand{\enskipp}{{\tiny\strut}\enskip}
\newcommand{\exclspace}{\hspace{.45pt}}
\newcommand{\notion}[1]{$\langle$#1$\rangle$}
\newcommand{\xnotion}[1]{#1}
\newcommand{\toolong}{$\hspace{-6em}$}

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

\def\eps{eps}

\def\webad#1#2#3{\vspace{-1.4em}\vbox to 0pt{\vspace{20em}\hspace{0em}\footnotesize\rlap{\gray{google \fbox{{\tiny\strut}\blue{\advirecord{x1}{#1}}\adviplay[slideblue]{x1}} $\,\mapsto$ {\small $\langle\hspace{.5pt}$}\texttt{http://\blue{\advirecord{x2}{#2}}\adviplay[slideblue]{x2}#3}{\small $\hspace{.5pt}\rangle$}}}\vss}}

\setcounter{slide}{-1}
\begin{slide}
\slidetitle{\Large do not take natural language \textsl{too} seriously}

\green{Freek Wiedijk} \\
Radboud University Nijmegen
\smallskip

\red{Seminar Formal Mathematics} \\
University of Bonn
\smallskip

2007\hspace{2pt}04\hspace{1.5pt}17, 13\hspace{.5pt}:\hspace{.7pt}00
\end{slide}

\begin{slide}
\slidetitle{programming languages}
\strut\rlap{\textbf{C\exclspace:}}\hfill\red{\texttt{i++;}}\hfill\strut
\adviwait

\strut\rlap{\textbf{Cobol\exclspace:\hfill}}\hfill\green{\texttt{ADD 1 TO i.}}\hfill\strut

\advirecord{c1}{\textbf{HyperTalk\exclspace:}}
\begin{alltt}\footnotesize
\advirecord{c2}{function delimitedSum theList, listDelimiter
  put the itemDelimiter into storedDelim \gray{-- save itemDelimiter for restore}\toolong
  if listDelim is empty then put comma into listDelimiter \gray{-- like 'sum'}
  else set the itemDelimiter to char 1 of value(listDelimiter) \gray{-- {\scriptsize{UN}}like 'sum'}\toolong
  put 0 into sumOfItems
  repeat with i = 1 to number of items in theList
    add value(item i of theList) to sumOfItems \gray{-- try to convert to a number}\toolong
  end repeat
  set the itemDelimiter to storedDelim \gray{-- restore itemDelimiter}
  return sumOfItems
end delimitedSum}
\end{alltt}
\adviwait

\blue{\textsl{making a programming language looks like natural language is a silly idea}}\adviwait\adviplay{c1}\adviplay[slidegreen]{c2}

\vspace{-11pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formulas}

\vspace{-1.55\bigskipamount}
\vbox to 0pt{
\vspace{12em}
\hfill\hspace{.5em}\advirecord{a5}{\includegraphics[width=15em]{/home/freek/talks/bonn/cardano2.eps}}\hfill\strut
\vss
}
\vspace{-1.18\bigskipamount}
\vbox to 0pt{
\vspace{11em}
\hfill\hspace{0em}\advirecord{a2}{\includegraphics[width=28em]{/home/freek/talks/bonn/cardano1.eps}}\hfill\strut
\vspace{-8em}

\advirecord{a2a}{\hrule height 9em width 30em}
\vss
}

\gray{solutions of \advirecord{a6}{\rlap{$x^3 + px = q$\exclspace:}}\advirecord{a7}{$x^3 + 6x = 20$\exclspace:}\adviplay{a6}}

\textbf{modern style\exclspace:}
\vspace{1\bigskipamount}
$$\advirecord{a4}{{\root 3\of{\sqrt{108} + 10}} - {\root 3\of{\sqrt{108} - 10}}}$$
\vspace{-5\bigskipamount}

$$\advirecord{a1}{x = {\root 3\of{{q\over 2} \pm \sqrt{\left({q\over 2}\right)^2 + \left({p\over 3}\right)^3}}} - {\root 3\of{- {q\over 2} \pm \sqrt{\left({q\over 2}\right)^2 + \left({p\over 3}\right)^3}}}}\adviplay[slidered]{a1}$$
\vspace{-.5\bigskipamount}
\smallskip
\adviwait

\textbf{ancient style}$\;$\gray{(Gerolamo Cardano, \textsl{Ars magna}, N\"urnberg, 1545)}\textbf{\exclspace:}
\adviplay{a2}
\adviwait
\adviplay[white]{a2a}
\begin{quote}\small
\advirecord{a3}{Cube the third part of the number of unknowns, to which you add the square of
half the number of the equation, and take the root of the whole, that is, the
square root, which you will use, in the one case adding the half of the number
which you just multiplied by itself, in the other case subtracting the same half,
and you will have a binomial and apotome respecitvely; then subtract the cube
root of the apotome from the cube root of the binomial, and the remainder from
this is the value of the unknown.}\adviplay[slidegreen]{a3}
\end{quote}
\adviwait
\adviplay[white]{a1}
\adviplay[white]{a3}
\adviplay[white]{a6}
\adviplay[slidered]{a4}
\adviplay{a5}
\adviplay[slidegray]{a7}

\vspace{-16pt}
\vfill
\end{slide}

\begin{slide}
\slidetitle{formal mathematics}
\gray{Bertrand's postulate\exclspace:}

\textbf{HOL Light\exclspace:}
\begingroup
\def\\{\char`\\}
\begin{alltt}\small
\red{!n. ~(n = 0) ==> ?p. prime p /\\ n <= p /\\ p <= 2 * n}
\end{alltt}
\endgroup
\vspace{-\bigskipamount}
$$\advirecord{b}{
\forall n.\, n\ne 0 \Rightarrow \exists p.\, \mathop{\sf prime\,} p \mathrel{\land} n \le p \mathrel{\land} p \le 2 \cdot n
}$$%\adviplay[slidegray]{b}$$

\textbf{Mizar\exclspace:}
\begin{alltt}\small
\green{for n being Element of NAT st n>=1 holds
  ex p being Prime st n<p & p<=2*n}
\end{alltt}
\adviwait

\begin{flushleft}
\gray{For all $n$ being an element of the natural numbers such that $n\ge 1$ holds %\penalty-100\strut\hfill
that there exists a $p$ being prime such that $n < p$ and $p\le 2 n$.}
\end{flushleft}
\adviwait
\adviplay[slidegray]{b}

\vfill
\end{slide}

\begin{slide}
\slidetitle{submarines aren't fishes}
\strut\hfill\hspace{-5em}\includegraphics[width=31.2em]{/home/freek/talks/bonn/zonnebloem1.eps}\hspace{-5em}\hfill\strut
\vspace{-17.3em}

\leftskip=1.8em
\rightskip=2.2em
\textsl{The question of whether machines can think is about as
relevant as the question of whether submarines can swim.}

\vspace{-1em}
\vfill
\end{slide}

\end{document}