diff --git a/main.tex b/main.tex
@@ -14,12 +14,6 @@
\begin{frame}{Disclaimer}
\begin{itemize}
- \item Baseado em
- \href{https://www.youtube.com/watch?v=T9ZqbQh-t9E}{Machine-Assisted
- Proofs}
-
- \pause
-
\item Hacker\dots
\begin{figure}
\centering
@@ -315,7 +309,7 @@
\item Tipos dependentes!
- \item Fixo alguns tipos primitivos
+ \item Codifico meus objetos como tipos
\begin{figure}
\centering
@@ -326,41 +320,34 @@
\begin{frame}{Provadores de Teoremas}
\begin{itemize}
- \item Provadores de Teoremas!
- \begin{itemize}
- \item Coq (\url{https://coq.inria.fr/})
+ \item Coq (\url{https://coq.inria.fr/})
- \item Idris (\url{https://www.idris-lang.org/})
+ \item Agda (\url{https://wiki.portal.chalmers.se/agda/pmwiki.php})
- \item Lean (\url{https://leanprover.github.io/})
+ \item Lean (\url{https://leanprover.github.io/})
- \item Isabelle (\url{https://isabelle.in.tum.de/})
- \end{itemize}
+ \item Idris (\url{https://www.idris-lang.org/})
+
+ \item Isabelle (\url{https://isabelle.in.tum.de/})
\end{itemize}
\begin{columns}
- \begin{column}{.2\linewidth}
+ \begin{column}{.1\linewidth}
\begin{figure}
\centering
- \includegraphics[scale=.6]{images/coq.png}
+ \includegraphics[width=\linewidth]{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{column}{.45\linewidth}
\begin{figure}
\centering
- \includegraphics[scale=.15]{images/lean.eps}
+ \includegraphics[width=\linewidth]{images/agda.eps}
\end{figure}
\end{column}
- \begin{column}{.2\linewidth}
+ \begin{column}{.25\linewidth}
\begin{figure}
\centering
- \includegraphics[scale=.4]{images/isabelle.png}
+ \includegraphics[width=\linewidth]{images/lean.eps}
\end{figure}
\end{column}
\end{columns}
@@ -379,19 +366,15 @@
\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 Análise funcional
\item \dots
\end{itemize}
@@ -401,17 +384,10 @@
\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}
+ \begin{figure}
+ \centering
+ \inputminted{lean}{examples/liquid.lean}
+ \end{figure}
\end{frame}
\begin{frame}{Pra que tudo isso?}
@@ -431,11 +407,12 @@
\item<5-> A prova de Mochizuki da conjetura abc
- \item<6-> A prova de Hales da conjectura de Kepler de 2015
+ \item<6-> A prova de Hales da conjectura de Kepler de 2015!
\item<7->
+ A conclusão do
\emph{\href{https://leanprover-community.github.io/liquid/}{Liquid
- Tensor Experiment}}
+ Tensor Experiment}} em julho de 2022!
\end{itemize}
\item<8-> \emph{Who watches the Watchmen?}
@@ -449,5 +426,28 @@
\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.hedonisticlearning.com/posts/understanding-typing-judgments.html}
+ {Understanding typing judgments}
+ \end{enumerate}
+\end{frame}
\end{document}