curry-howard

Slides of a (very) informal lecture of mine on the Curry-Howard correspondence

git clone: git://git.pablopie.xyz/curry-howard
Log
Files
Refs
README
LICENSE

Commit: 859cde5e5eff96ca86d48fac5d9f75d6f937b7c8
Parent: bf83f0cc399d06d28392ec263254b548e9b3b839
Author: Pablo <pablo-escobar@riseup.net>
Date: Sun, 9 Oct 2022 20:48:20 +0000

Moved the slides to the main file

Also removed un-used slides

Diffstat

4 files changed, 383 insertions, 544 deletions

Status	File Name	N° Changes	Insertions	Deletions
Modified	main.tex	387	383	4
Deleted	sections/curry.tex	349	0	349
Deleted	sections/exploratory.tex	115	0	115
Deleted	sections/numeric.tex	76	0	76

diff --git a/main.tex b/main.tex
@@ -3,7 +3,7 @@
 
 \definecolor{hacker}{RGB}{4,165,90}
 
-\title{Como fazer matemática com um computador?}
+\title{Como provar teoremas um computador?}
 \author{Pablo \\ \texttt{pablopie.xyz}}
 \date{Outubro de 2022}
 
@@ -68,11 +68,390 @@
   \end{itemize}
 \end{frame}
 
-\input{sections/numeric}
+\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]{Métodos Não-Numéricos?}
+  \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}
+
+  \pause
+
+  \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]{Métodos Não-Numéricos?}
+  \begin{itemize}
+    \item Objection!
+  \end{itemize}
+
+  \pause
+
+  \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}
+
+\subsection{A Correspondência de Curry-Howard}
+
+\begin{frame}{A Correspondência de Curry-Howard}
+  \begin{center}
+    \begin{tabular}{rcl}
+      Provar que vale \(A\) 
+        & \(\leftrightsquigarrow\) 
+        & Encontrar \(a \in \{ \text{provas de}\ A\}\)
+    \end{tabular}
+  \end{center}
+  
+  \pause
+
+  \begin{itemize}
+    \item Proposições como tipos 
+      \begin{center}
+        \begin{tabular}{rcl}
+          \(A\) 
+            & \(\leftrightsquigarrow\) 
+            & \(\{\text{provas de}\ A \}\) \\
+          \(A\ \text{e}\ B\) 
+            & \(\leftrightsquigarrow\) 
+            & \(\{\text{provas de}\ A \} \times \{\text{provas de}\ B \}\) \\
+          \(A\ \text{ou}\ B\) 
+            & \(\leftrightsquigarrow\) 
+            & \(\{\text{provas de}\ A \} \cup \{\text{provas de}\ B \}\) \\
+          \(A \implies B\)
+            & \(\leftrightsquigarrow\) 
+            & \(\{\text{provas de}\ A \} \to \{\text{provas de}\ B \}\) \\
+        \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}
+
+    \item Linguagens estaticamente tipadas
+  \end{itemize}
+
+  \begin{center}
+    \begin{tabular}{rcl}
+      Provar que vale \(A\) 
+        & \(\leftrightsquigarrow\) 
+        & Construir \(a : \{ \text{provas de}\ A\}\) \\
+      Checar a prova
+        & \(\leftrightsquigarrow\) 
+        & Checar os tipos
+    \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 Aximas!
+      \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}
+
+        \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\)
+
+      \pause
+
+    \item Tipos dependentes!
+
+    \item Fixo alguns tipos primitivos
+
+        \begin{figure}
+          \centering
+          \inputminted{lean}{examples/nat.lean}
+        \end{figure}
+  \end{itemize}
+\end{frame}
+
+\begin{frame}{Provadores de Teoremas}
+  \begin{itemize}
+    \item Provadores de Teoremas!
+      \begin{itemize}
+        \item Coq (\url{https://coq.inria.fr/})
+
+        \item Idris (\url{https://www.idris-lang.org/})
+
+        \item Lean (\url{https://leanprover.github.io/})
+
+        \item Isabelle (\url{https://isabelle.in.tum.de/})
+      \end{itemize}
+  \end{itemize}
+
+  \begin{columns}
+    \begin{column}{.2\linewidth}
+      \begin{figure}
+        \centering
+        \includegraphics[scale=.6]{images/coq.png}
+      \end{figure}
+    \end{column}
+    \begin{column}{.2\linewidth}
+      \begin{figure}
+        \centering
+        \includegraphics[scale=.095]{images/idris.eps}
+      \end{figure}
+    \end{column}
+    \begin{column}{.2\linewidth}
+      \begin{figure}
+        \centering
+        \includegraphics[scale=.15]{images/lean.eps}
+      \end{figure}
+    \end{column}
+    \begin{column}{.2\linewidth}
+      \begin{figure}
+        \centering
+        \includegraphics[scale=.4]{images/isabelle.png}
+      \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 Algebra linear
+
+            \item Algebra abstrata
+
+            \item Topologia
+
+            \item Análise
+
+            \item Geometria diferencial
+
+            \item Teoria dos números
+
+            \item Combinatória
+
+            \item \dots
+          \end{itemize}
+      \end{itemize}
+    \end{column}
+  \end{columns}
+
+  \pause
+
+  \begin{itemize}
+    \item A \emph{mathlib} ainda não tem suporte para tudo na matemática\dots
+
+      \pause
+
+    \item A \emph{mathlib} ``nunca foi usada para provar algo novo''\dots
+
+      \pause
+
+    \item Pra que tudo isso então?
+  \end{itemize}
+\end{frame}
+
+\subsection{Aplicações}
+
+\begin{frame}{Pra que tudo isso?}
+  \begin{columns}
+    \begin{column}[t]{.65\linewidth}
+      \begin{itemize}
+        \item<1-> Verificação formal de software e hardware \pause
+          \begin{itemize}
+            \item<2-> O bug do Pentium de 1994
+
+            \item<3-> A queda do voo 302 da Ethiopian Airlines em 2019
+          \end{itemize}
 
-\input{sections/curry}
+        \item<4-> Provas de alta complexidade
+          \begin{itemize}
+            \item<4-> Classificação dos grupos simples finitos
 
-%\input{sections/exploratory}
+            \item<5-> A prova de Mochizuki da conjetura abc
 
+            \item<6-> A prova de Hales da conjectura de Kepler de 2015
+
+            \item<7->
+              \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
+              Tensor Experiment}}
+          \end{itemize}
+
+        \item<8-> \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}
 \end{document}

diff --git a/sections/curry.tex b/sections/curry.tex
@@ -1,349 +0,0 @@
-\begin{frame}[fragile]{Métodos Não-Numéricos?}
-  \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}
-
-  \pause
-
-  \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]{Métodos Não-Numéricos?}
-  \begin{itemize}
-    \item Objection!
-  \end{itemize}
-
-  \pause
-
-  \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}
-
-\subsection{A Correspondência de Curry-Howard}
-
-\begin{frame}{A Correspondência de Curry-Howard}
-  \begin{center}
-    \begin{tabular}{rcl}
-      Provar que vale \(A\) 
-        & \(\leftrightsquigarrow\) 
-        & Encontrar \(a \in \{ \text{provas de}\ A\}\)
-    \end{tabular}
-  \end{center}
-  
-  \pause
-
-  \begin{itemize}
-    \item Proposições como tipos 
-      \begin{center}
-        \begin{tabular}{rcl}
-          \(A\) 
-            & \(\leftrightsquigarrow\) 
-            & \(\{\text{provas de}\ A \}\) \\
-          \(A\ \text{e}\ B\) 
-            & \(\leftrightsquigarrow\) 
-            & \(\{\text{provas de}\ A \} \times \{\text{provas de}\ B \}\) \\
-          \(A\ \text{ou}\ B\) 
-            & \(\leftrightsquigarrow\) 
-            & \(\{\text{provas de}\ A \} \cup \{\text{provas de}\ B \}\) \\
-          \(A \implies B\)
-            & \(\leftrightsquigarrow\) 
-            & \(\{\text{provas de}\ A \} \to \{\text{provas de}\ B \}\) \\
-        \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}
-
-    \item Linguagens estaticamente tipadas
-  \end{itemize}
-
-  \begin{center}
-    \begin{tabular}{rcl}
-      Provar que vale \(A\) 
-        & \(\leftrightsquigarrow\) 
-        & Construir \(a : \{ \text{provas de}\ A\}\) \\
-      Checar a prova
-        & \(\leftrightsquigarrow\) 
-        & Checar os tipos
-    \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 Aximas!
-      \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}
-
-        \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\)
-
-      \pause
-
-    \item Tipos dependentes!
-
-    \item Fixo alguns tipos primitivos
-
-        \begin{figure}
-          \centering
-          \inputminted{lean}{examples/nat.lean}
-        \end{figure}
-  \end{itemize}
-\end{frame}
-
-\begin{frame}{Provadores de Teoremas}
-  \begin{itemize}
-    \item Provadores de Teoremas!
-      \begin{itemize}
-        \item Coq (\url{https://coq.inria.fr/})
-
-        \item Idris (\url{https://www.idris-lang.org/})
-
-        \item Lean (\url{https://leanprover.github.io/})
-
-        \item Isabelle (\url{https://isabelle.in.tum.de/})
-      \end{itemize}
-  \end{itemize}
-
-  \begin{columns}
-    \begin{column}{.2\linewidth}
-      \begin{figure}
-        \centering
-        \includegraphics[scale=.6]{images/coq.png}
-      \end{figure}
-    \end{column}
-    \begin{column}{.2\linewidth}
-      \begin{figure}
-        \centering
-        \includegraphics[scale=.095]{images/idris.eps}
-      \end{figure}
-    \end{column}
-    \begin{column}{.2\linewidth}
-      \begin{figure}
-        \centering
-        \includegraphics[scale=.15]{images/lean.eps}
-      \end{figure}
-    \end{column}
-    \begin{column}{.2\linewidth}
-      \begin{figure}
-        \centering
-        \includegraphics[scale=.4]{images/isabelle.png}
-      \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 Algebra linear
-
-            \item Algebra abstrata
-
-            \item Topologia
-
-            \item Análise
-
-            \item Geometria diferencial
-
-            \item Teoria dos números
-
-            \item Combinatória
-
-            \item \dots
-          \end{itemize}
-      \end{itemize}
-    \end{column}
-  \end{columns}
-
-  \pause
-
-  \begin{itemize}
-    \item A \emph{mathlib} ainda não tem suporte para tudo na matemática\dots
-
-      \pause
-
-    \item A \emph{mathlib} ``nunca foi usada para provar algo novo''\dots
-
-      \pause
-
-    \item Pra que tudo isso então?
-  \end{itemize}
-\end{frame}
-
-\subsection{Aplicações}
-
-\begin{frame}{Pra que tudo isso?}
-  \begin{columns}
-    \begin{column}[t]{.65\linewidth}
-      \begin{itemize}
-        \item<1-> Verificação formal de software e hardware \pause
-          \begin{itemize}
-            \item<2-> O bug do Pentium de 1994
-
-            \item<3-> A queda do voo 302 da Ethiopian Airlines em 2019
-          \end{itemize}
-
-        \item<4-> Provas de alta complexidade
-          \begin{itemize}
-            \item<4-> 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<7->
-              \emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
-              Tensor Experiment}}
-          \end{itemize}
-
-        \item<8-> \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}

diff --git a/sections/exploratory.tex b/sections/exploratory.tex
@@ -1,115 +0,0 @@
-\section{Uso Exploratório}
-
-\begin{frame}{Uso Exploratório}
-  \begin{itemize}
-    \item Plotar coisas \pause
-    \begin{align*}
-      \frac{\dx}{\dt} & = x + y & \frac{\dy}{\dt} & = -x + y
-    \end{align*}
-
-      \pause
-
-    \begin{figure}
-      \centering
-      \includegraphics[width=.8\linewidth]{images/ode.eps}
-    \end{figure}
-  \end{itemize}
-\end{frame}
-
-\begin{frame}{Uso Exploratório}
-  \begin{itemize}
-    \item<1-> Continhas bobas 
-      \begin{columns}
-        \begin{column}{.5\linewidth}
-          \begin{align*}
-            \onslide<1->{
-              \int_0^\pi \sin t \cdot \cos^2 t \; \dt & = \frac{2}{3}
-            }  \\
-            \onslide<2->{
-              \int_0^\pi \sin t \cdot \cos^2 t \; \dt & \approx 0.66667
-            }
-          \end{align*}
-        \end{column}
-        \begin{column}{.5\linewidth}
-          \begin{figure}
-            \centering
-            \includegraphics[scale=2]{images/wolfram.eps}
-          \end{figure}
-        \end{column}
-      \end{columns}
-
-    \item<3-> Como o Wolfram resolve essa integral?
-      \onslide<4->{
-        \begin{align*}
-          \int_0^\pi \sin t \cdot \cos^2 t \; \dt 
-          & = \left. \left( - \cos^3 t \right) \right|_{t = 0}^\pi 
-            - 2 \int_0^\pi \sin t \cdot \cos^2 t \; \dt \\
-          \int_0^\pi \sin t \cdot \cos^2 t \; \dt 
-          & = \frac{\left. \left( - \cos^3 t \right) \right|_{t = 0}^\pi}{3} \\
-          \int_0^\pi \sin t \cdot \cos^2 t \; \dt 
-          & = \frac{2}{3}
-        \end{align*}
-      }
-  \end{itemize}
-\end{frame}
-
-\begin{frame}{Computação Simbólica}
-  \begin{columns}
-    \begin{column}{.7\linewidth}
-      \begin{itemize}
-        \item<1-> Calculadora \emph{simbólica}
-          \begin{itemize}
-            \item<1-> Abre as mesmas contas que abrimos na mão
-            \item<2-> Usa todos os truques do baralho
-            \item<3-> Deixa \emph{coisas indeterminadas} expressas
-              \begin{figure}
-                \centering
-                \inputminted{python}{examples/sqrt.py}
-              \end{figure}
-          \end{itemize}
-
-        \item<4-> Computer Algebra System (CAS)
-          \begin{itemize}
-            \item Sage (\url{https://www.sagemath.org/})
-            \item GAP (\url{https://www.gap-system.org/})
-            \item Mathics (\url{https://mathics.org/})
-            \item GeoGebra (\url{https://geogebra.org/})
-          \end{itemize}
-      \end{itemize}
-    \end{column}
-      \begin{column}{.22\linewidth}
-        \begin{figure}
-          \includegraphics[width=\linewidth]{images/calculator.jpg}
-        \end{figure}
-      \end{column}
-  \end{columns}
-
-  \onslide<4->{
-    \begin{columns}
-      \begin{column}{.2\linewidth}
-        \begin{figure}
-          \centering
-          \includegraphics[scale=.12]{images/sage.eps}
-        \end{figure}
-      \end{column}
-      \begin{column}{.2\linewidth}
-        \begin{figure}
-          \centering
-          \includegraphics[scale=.2]{images/gap.png}
-        \end{figure}
-      \end{column}
-      \begin{column}{.2\linewidth}
-        \begin{figure}
-          \centering
-          \includegraphics[scale=.2]{images/mathics.eps}
-        \end{figure}
-      \end{column}
-      \begin{column}{.2\linewidth}
-        \begin{figure}
-          \centering
-          \includegraphics[scale=2]{images/geogebra.eps}
-        \end{figure}
-      \end{column}
-    \end{columns}
-  }
-\end{frame}

diff --git a/sections/numeric.tex b/sections/numeric.tex
@@ -1,76 +0,0 @@
-\begin{frame}{Como fazer matemática com um computador?}
-  \begin{itemize}
-    \item Será que um computador pode nos ajudar a provar teoremas?
-      
-      \pause
-
-    \item As vezes provar teoremas acaba caindo em continhas
-      
-    \item As vezes são \emph{muitas} continhas
-      \begin{figure}
-        \centering
-        \includegraphics[scale=.3]{images/pet.jpg}
-      \end{figure}
-      
-      \pause
-
-    \item Será que um computador não consegue fazer as continhas pra mim?
-  \end{itemize}
-\end{frame}
-
-\begin{frame}{Métodos Numéricos}
-  \begin{theorem}[Teorema das Quatro Cores]
-    Todo mapa pode ser pintado de quatro cores distintas de modo dois países
-    adjacentes não compartilham a mesma cor.
-  \end{theorem}
-
-  \begin{figure}
-    \centering
-    \includegraphics[width=.8\linewidth]{images/4-colors.eps}
-  \end{figure}
-  
-  \pause
-
-  \begin{itemize}
-    \item Provado em 1976 por Kenneth Appel e Wolfgang Haken usando o método 
-      \emph{discharging}
-  \end{itemize}
-\end{frame}
-
-\subsection{Provas Por Exaustão}
-
-\begin{frame}{Provar Por Exaustão}
-  \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}