\def\hidepauses{yes}
\input{preamble}

\definecolor{hacker}{RGB}{4,165,90}

\title{Como provar teoremas em um computador?}
\author{Pablo \\ \texttt{pablopie.xyz}}
\date{Outubro de 2022}

\begin{document}
\begin{frame}
  \maketitle
\end{frame}

\begin{frame}{Disclaimer}
  \begin{itemize}
    \item Hacker\dots
      \begin{figure}
        \centering
        \BVerbatimInput[formatcom=\color{hacker}]{examples/hacker.txt}
      \end{figure}

      \pause

    \item Dedução natural\dots
      \[
        \begin{array}{cc}
          \displaystyle{
            \frac
            {\Gamma \vdash_\Sigma h_1 : P \quad \Gamma \vdash_\Sigma h_2 : Q}
            {\Gamma \vdash_\Sigma \operatorname{intro} h_1 \ h_2 : P \wedge Q}
            \rightarrow C
          } &
          \displaystyle{
            \frac{
              \Gamma \vdash_\Sigma h : P \quad
              \Gamma \vdash_\Sigma f : P \supset Q
            }{\Gamma \vdash_\Sigma f \ h : Q}
            \rightarrow E
          } \\ \\
          \displaystyle{
            \frac{\Gamma \vdash_\Sigma h : P}
                 {\Gamma \vdash_\Sigma \operatorname{inl} h : P \vee Q}
            \rightarrow D_1
          } &
          \displaystyle{
            \frac{\Gamma \vdash_\Sigma h : Q}
                 {\Gamma \vdash_\Sigma \operatorname{inr} h : P \vee Q}
            \rightarrow D_2
          }
        \end{array}
     \]

      \pause

    \item Não precisa entender o código!

      \pause

    \item Me interrompa!
  \end{itemize}
\end{frame}

\begin{frame}{Como provar teoremas em um computador?}
  \begin{columns}
    \begin{column}{.35\linewidth}
      \begin{figure}
        \centering
        \includegraphics[width=\linewidth]{images/kepler.eps}
      \end{figure}
    \end{column}
    \begin{column}{.65\linewidth}
      \begin{itemize}
        \item Se eu tenho um número finito de casos\dots\ posso testar todos os
          casos!
          \begin{figure}
            \centering
            \inputminted{python}{examples/exhaustion.py}
          \end{figure}
      \end{itemize}

      \pause

      \begin{theorem}[Conjectura de Kepler]
        Nenhum arranjo de esferas em três dimensões tem uma densidade média
        maior do que o arranjo cúbico.
      \end{theorem}

      \begin{itemize}
        \item Provado em 1998 por Thomas Hales via exaustão

          \pause

        \item E se o número de casos não for finito???
      \end{itemize}
    \end{column}
  \end{columns}
\end{frame}

\begin{frame}[fragile]{Como provar teoremas em um computador?}
  \begin{itemize}
    \item Antes de tentar provar meu teorema, eu preciso enunciar ele\dots
  \end{itemize}

  \pause

  \begin{columns}
    \begin{column}{.5\linewidth}
      \[
        n! =
        \begin{cases}
          1 & \text{se}\ n = 0 \\
          n \cdot (n - 1)! & \text{se}\  n > 0
        \end{cases}
      \]
    \end{column}
    \begin{column}{.5\linewidth}
      \inputminted{python}{examples/factorial.py}
    \end{column}
  \end{columns}

  \pause

  \begin{columns}
    \begin{column}{.5\linewidth}
      \[
        n! \cdot m! \mid (n + m)!
      \]
    \end{column}
    \begin{column}{.5\linewidth}
      \begin{minted}{python}
        # ???
      \end{minted}
    \end{column}
  \end{columns}

  \pause

  \begin{itemize}
    \item Temos termos, mas não temos formulas!
  \end{itemize}

  \begin{figure}
    \centering
    \begin{tabular}{|l|l|}
      \hline
      Termos
        & Fórmulas \\
      \hline
      Um número \(n\)
        & ``\(n > m\)'' \\
      \hline
      Um conjunto \(X\)
        & ``\(x \in X\)'' \\
      \hline
      Pontos, retas, planos, \dots
        & O quinto postulado de Euclides \\
      \hline
    \end{tabular}
  \end{figure}
\end{frame}

\begin{frame}[fragile]{Como provar teoremas um computador?}
  \begin{itemize}
    \item Objection!
  \end{itemize}

  \begin{columns}
    \begin{column}{.3\linewidth}
      \[
        n! \cdot m! \mid (n + m)!
      \]
    \end{column}
    \begin{column}{.5\linewidth}
      \inputminted{python}{examples/fake-theorem.py}
    \end{column}
  \end{columns}

  \pause

  \begin{align*}
    p : \mathbb{N} \times \mathbb{N} & \to \{0, 1\} \\
    (n, m) & \mapsto
    \begin{cases}
      1 & \text{se}\ n! \cdot m! \mid (n + m) ! \\
      0 & \text{caso contrário} \\
    \end{cases}
  \end{align*}

  \pause

  \begin{itemize}
    \item Nenhum computador é capaz de checar que \(p(n, m) = 1\) para todos
      \(n, m\)
      \begin{figure}
        \centering
        \inputminted{python}{examples/exhaustion-naive.py}
      \end{figure}
  \end{itemize}
\end{frame}

\begin{frame}{A Correspondência de Curry-Howard}
  \begin{center}
    \begin{tabular}{rcl}
      Provar que vale \(P\)
        & \(\leftrightsquigarrow\)
        & Encontrar \(h \in \{ \text{provas de}\ P\}\)
    \end{tabular}
  \end{center}

  \pause

  \begin{itemize}
    \item Proposições como tipos
      \begin{center}
        \begin{tabular}{rcl}
          \(P\)
            & \(\leftrightsquigarrow\)
            & \(\{\text{provas de}\ P \}\) \\
          \(P\ \text{e}\ Q\)
            & \(\leftrightsquigarrow\)
            & \(\{\text{provas de}\ P \} \times \{\text{provas de}\ Q \}\) \\
          \(P\ \text{ou}\ Q\)
            & \(\leftrightsquigarrow\)
            & \(\{\text{provas de}\ P \} \cup \{\text{provas de}\ Q \}\) \\
          \(P \implies Q\)
            & \(\leftrightsquigarrow\)
            & \(\{\text{provas de}\ P \} \to \{\text{provas de}\ Q \}\) \\
        \end{tabular}
      \end{center}

      \pause

    \item Mas como eu represento isso num computador? \pause Tipos!
      \begin{figure}
        \centering
        \inputminted{python}{examples/types.py}
      \end{figure}
  \end{itemize}
\end{frame}

\begin{frame}[fragile]{A Correspondência de Curry-Howard}
  \begin{itemize}
    \item Computadores são muito bons em checar tipos!
      \begin{figure}
        \centering
        \inputminted{c}{examples/typechecking.c}
      \end{figure}

      \pause

    \item Linguagens estaticamente tipadas
  \end{itemize}

  \begin{center}
    \begin{tabular}{rcl}
      Provar que vale \(P\)
        & \(\leftrightsquigarrow\)
        & Construir \(h : \{ \text{provas de}\ P\}\) \\
      Checar a prova
        & \(\leftrightsquigarrow\)
        & Checar os tipos \\
      Inconsistência na prova
        & \(\leftrightsquigarrow\)
        & Tipos não batem
    \end{tabular}
  \end{center}
\end{frame}

\begin{frame}{A Correspondência de Curry-Howard}
  \begin{itemize}
    \item Mas como isso funciona na prática?
        \begin{figure}
          \centering
          \inputminted{python}{examples/types.py}
        \end{figure}

        \pause

        \begin{figure}
          \centering
          \inputminted{lean}{examples/types.lean}
        \end{figure}

    \item Tipos algébricos!
  \end{itemize}
\end{frame}

\begin{frame}{A Correspondência de Curry-Howard}
  \begin{itemize}
    \item Axiomas!
      \begin{itemize}
        \item Dados \(x\) e \(y\), existe o tipo \texttt{x = y} das provas de
          que \(x = y\)

          \begin{figure}
            \centering
            \inputminted{lean}{examples/eq.lean}
          \end{figure}

          \pause

        \item O tipo \texttt{x = x} tem um único elemento \texttt{rfl}
      \end{itemize}

      \pause

    \item O tipo \texttt{x = y} varia com \(x\) e \(y\)

    \item Tipos dependentes!

      \pause

    \item Codifico meus objetos como tipos
        \begin{figure}
          \centering
          \inputminted{lean}{examples/nat.lean}
        \end{figure}
  \end{itemize}
\end{frame}

\begin{frame}{Proof Checkers}
  \begin{itemize}
    \item Coq (\url{https://coq.inria.fr/})

    \item Agda (\url{https://wiki.portal.chalmers.se/agda/pmwiki.php})

    \item Lean (\url{https://leanprover.github.io/})

    \item Idris (\url{https://www.idris-lang.org/})

    \item Isabelle (\url{https://isabelle.in.tum.de/})
  \end{itemize}

  \begin{columns}
    \begin{column}{.1\linewidth}
      \begin{figure}
        \centering
        \includegraphics[width=\linewidth]{images/coq.png}
      \end{figure}
    \end{column}
    \begin{column}{.45\linewidth}
      \begin{figure}
        \centering
        \includegraphics[width=\linewidth]{images/agda.eps}
      \end{figure}
    \end{column}
    \begin{column}{.25\linewidth}
      \begin{figure}
        \centering
        \includegraphics[width=\linewidth]{images/lean.eps}
      \end{figure}
    \end{column}
  \end{columns}
\end{frame}

\begin{frame}[fragile]{Lean}
  \begin{columns}
    \begin{column}{.45\linewidth}
      \begin{figure}[t]
        \centering
        \inputminted{lean}{examples/example.lean}
      \end{figure}
    \end{column} \pause
    \begin{column}{.40\linewidth}
      \begin{itemize}
        \item
          \href{https://leanprover-community.github.io/mathlib-overview.html}{mathlib}
          \begin{itemize}
            \item Álgebra abstrata

            \item Topologia

            \item Geometria diferencial

            \item Teoria dos números

            \item Análise funcional

            \item \dots
          \end{itemize}
      \end{itemize}
    \end{column}
  \end{columns}

  \pause

  \begin{figure}
    \centering
    \inputminted{lean}{examples/liquid.lean}
  \end{figure}
\end{frame}

\begin{frame}{Pra que tudo isso?}
  \begin{columns}
    \begin{column}[t]{.65\linewidth}
      \begin{itemize}
        \item<2-> Verificação formal de software e hardware \pause
          \begin{itemize}
            \item<3-> O bug do Pentium de 1994

            \item<4-> A queda do voo 302 da Ethiopian Airlines em 2019
          \end{itemize}

        \item<5-> Provas de alta complexidade
          \begin{itemize}
            \item<5-> Classificação dos grupos simples finitos

            \item<5-> A prova de Mochizuki da conjetura abc

            \item<6-> A prova de Hales da conjectura de Kepler de 2015!

            \item<6->
              A conclusão do
              \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
              Tensor Experiment}} em julho de 2022!
          \end{itemize}

        \item<7-> \emph{Who watches the Watchmen?}
          \includegraphics[height=1em]{images/watchmen.eps}
      \end{itemize}
    \end{column}
    \begin{column}[t]{.25\linewidth}
      \begin{figure}[t]
        \includegraphics[width=\linewidth]{images/pentium.png}
      \end{figure}
    \end{column}
  \end{columns}
\end{frame}

\begin{frame}{Links}
  \begin{enumerate}
    \item
      \href{https://www.ma.imperial.ac.uk/~buzzard/xena/natural_number_game/}
           {The Natural Number Game}
    \item
      \href{https://leanprover-community.github.io/blog/posts/lte-final/}
           {Completion of the Liquid Tensor Experiment}

    \item
      \href{https://www.youtube.com/watch?v=T9ZqbQh-t9E}
           {Machine-Assisted Proofs}

    \item
      \href{https://www.nature.com/articles/s41586-021-04086-x}
           {Advancing mathematics by guiding human intuition with AI}

    \item
      \href{https://www.youtube.com/watch?v=IOiZatlZtGU}
           {Propositions as Types}

    \item
      \href{https://www.hedonisticlearning.com/posts/understanding-typing-judgments.html}
           {Understanding typing judgments}
  \end{enumerate}
  \begin{align*}
    \frac{\Gamma \vdash_\Sigma h : P}
         {\Gamma \vdash_\Sigma \operatorname{inl} h : P \vee Q}
    \rightarrow D_1
    & &
    \frac{\Gamma \vdash_\Sigma h : P}
         {\Gamma \vdash_\Sigma \operatorname{inr} h : P \vee Q}
    \rightarrow D_2
  \end{align*}
\end{frame}
\end{document}
