slides-ai2025.tex

\documentclass[12pt,utf8,notheorems,compress,t,aspectratio=169]{beamer}
\usepackage{etex}

\usepackage{pgfpages}
\usepackage[export]{adjustbox}

% Workaround for the issue described at
% https://tex.stackexchange.com/questions/164406/beamer-using-href-in-notes.
\newcommand{\fixedhref}[2]{\parbox[t][0pt][t]{0pt}{\vspace*{-\paperheight}\vspace*{-0.6em}\href{#1}{#2}}\href{#1}{#2}}

\usepackage[english]{babel}

\usepackage{mathtools}
\usepackage{xspace}
\usepackage{booktabs}
\usepackage{stmaryrd}
\usepackage{amssymb}
\usepackage{manfnt}
\usepackage{array}
\usepackage{ragged2e}
\usepackage{multicol}
\usepackage{tabto}
\usepackage{xstring}
\usepackage{environ}
\usepackage{proof}
\usepackage{agda}
\usepackage[all]{xy}
\xyoption{rotate}
\usepackage{tikz}
\usetikzlibrary{calc,shapes,shapes.callouts,shapes.arrows,patterns,fit,backgrounds,decorations.pathmorphing,positioning,svg.path}
\hypersetup{colorlinks=true}
\usepackage[dvipsnames]{xcolor}
\usepackage{fontawesome5}

\DeclareFontFamily{U}{bbm}{}
\DeclareFontShape{U}{bbm}{m}{n}
   {  <5> <6> <7> <8> <9> <10> <12> gen * bbm
      <10.95> bbm10%
      <14.4>  bbm12%
      <17.28><20.74><24.88> bbm17}{}
\DeclareFontShape{U}{bbm}{m}{sl}
   {  <5> <6> <7> bbmsl8%
      <8> <9> <10> <12> gen * bbmsl
      <10.95> bbmsl10%
      <14.4> <17.28> <20.74> <24.88> bbmsl12}{}
\DeclareFontShape{U}{bbm}{bx}{n}
   {  <5> <6> <7> <8> <9> <10> <12> gen * bbmbx
      <10.95> bbmbx10%
      <14.4> <17.28> <20.74> <24.88> bbmbx12}{}
\DeclareFontShape{U}{bbm}{bx}{sl}
   {  <5> <6> <7> <8> <9> <10> <10.95> <12> <14.4> <17.28>%
      <20.74> <24.88> bbmbxsl10}{}
\DeclareFontShape{U}{bbm}{b}{n}
   {  <5> <6> <7> <8> <9> <10> <10.95> <12> <14.4> <17.28>%
      <20.74> <24.88> bbmb10}{}
\DeclareMathAlphabet{\mathbbm}{U}{bbm}{m}{n}
\SetMathAlphabet\mathbbm{bold}{U}{bbm}{bx}{n}

\usepackage{pifont}
\newcommand{\cmark}{\ding{51}}
\newcommand{\xmark}{\ding{55}}
\DeclareSymbolFont{extraup}{U}{zavm}{m}{n}
\DeclareMathSymbol{\varheart}{\mathalpha}{extraup}{86}

\graphicspath{{images/}}

\usepackage[protrusion=true,expansion=true]{microtype}

\setlength\parskip{\medskipamount}
\setlength\parindent{0pt}

\title{Towards topological type theory for decrypting transfinite methods in classical mathematics}

\author{Ingo Blechschmidt}
\date{June 9th, 2025}

%\setbeameroption{show notes on second screen=bottom}
\newcommand{\jnote}[2]{\only<#1>{\note{\setlength\parskip{\medskipamount}\footnotesize\justifying#2\par}}}
\makeatletter
\setbeamertemplate{note page}
{%
  {%
    \scriptsize
    \insertvrule{.25\paperheight}{white!90!black}
    \vskip-.25\paperheight
    \nointerlineskip
    \vbox{
      %\hfill\insertslideintonotes{0.25}\hskip-\Gm@rmargin\hskip0pt%
      %\vskip-0.25\paperheight%
      %\nointerlineskip
      \begin{pgfpicture}{0cm}{0cm}{0cm}{0cm}
        \begin{pgflowlevelscope}{\pgftransformrotate{90}}
          {\pgftransformshift{\pgfpoint{-2cm}{0.2cm}}%
          \pgftext[base,left]{\footnotesize\the\year-\ifnum\month<10\relax0\fi\the\month-\ifnum\day<10\relax0\fi\the\day}}
        \end{pgflowlevelscope}
      \end{pgfpicture}}
    \nointerlineskip
    \vbox to .25\paperheight{\vskip0.5em
      \hbox{\insertshorttitle[width=8cm]}%
      \setbox\beamer@tempbox=\hbox{\insertsection}%
      \hbox{\ifdim\wd\beamer@tempbox>1pt{\hskip4pt\raise3pt\hbox{\vrule
            width0.4pt height7pt\vrule width 9pt
            height0.4pt}}\hskip1pt\hbox{\begin{minipage}[t]{7.5cm}\def\breakhere{}\insertsection\end{minipage}}\fi%
      }%
      \setbox\beamer@tempbox=\hbox{\insertsubsection}%
      \hbox{\ifdim\wd\beamer@tempbox>1pt{\hskip17.4pt\raise3pt\hbox{\vrule
            width0.4pt height7pt\vrule width 9pt
            height0.4pt}}\hskip1pt\hbox{\begin{minipage}[t]{7.5cm}\def\breakhere{}\insertsubsection\end{minipage}}\fi%
      }%
      \setbox\beamer@tempbox=\hbox{\insertshortframetitle}%
      \hbox{\ifdim\wd\beamer@tempbox>1pt{\hskip30.8pt\raise3pt\hbox{\vrule
            width0.4pt height7pt\vrule width 9pt
            height0.4pt}}\hskip1pt\hbox{\insertshortframetitle[width=7cm]}\fi%
      }%
      \vfil}%
  }%
  \vskip.25em
  \nointerlineskip
  \insertnote
}
\makeatother

%\useinnertheme[shadow=true]
\setbeamerfont{block title}{size={}}

\useinnertheme{rectangles}

\usecolortheme{orchid}
\usecolortheme{seahorse}
\definecolor{mypurple}{RGB}{253,73,34}
\definecolor{mypurpledark}{RGB}{100,0,150}
\setbeamercolor{structure}{fg=mypurple}
\setbeamercolor*{title}{bg=mypurple,fg=white}
\setbeamercolor*{titlelike}{bg=mypurple,fg=white}
\setbeamercolor{frame}{bg=black}

\usefonttheme{serif}
\usepackage[T1]{fontenc}
\usepackage{libertine}

% lifted from https://arxiv.org/abs/1506.08870
\DeclareFontFamily{U}{min}{}
\DeclareFontShape{U}{min}{m}{n}{<-> udmj30}{}
\newcommand\yon{\!\text{\usefont{U}{min}{m}{n}\symbol{'210}}\!}

\newcommand{\A}{\mathcal{A}}
\newcommand{\B}{\mathcal{B}}
\newcommand{\C}{\mathcal{C}}
\newcommand{\M}{\mathcal{M}}
\renewcommand{\AA}{\mathbb{A}}
\newcommand{\BB}{\mathbb{B}}
\newcommand{\pp}{\mathbbm{p}}
\newcommand{\MM}{\mathbb{M}}
\newcommand{\E}{\mathcal{E}}
\newcommand{\F}{\mathcal{F}}
\newcommand{\FF}{\mathbb{F}}
\newcommand{\G}{\mathcal{G}}
\newcommand{\J}{\mathcal{J}}
\newcommand{\GG}{\mathbb{G}}
\renewcommand{\O}{\mathcal{O}}
\newcommand{\K}{\mathcal{K}}
\newcommand{\NN}{\mathbb{N}}
\newcommand{\QQ}{\mathbb{Q}}
\newcommand{\RR}{\mathbb{R}}
\newcommand{\TT}{\mathbb{T}}
\newcommand{\PP}{\mathbb{P}}
\newcommand{\ZZ}{\mathbb{Z}}
\newcommand{\CC}{\mathbb{C}}
\renewcommand{\P}{\mathcal{P}}
\newcommand{\aaa}{\mathfrak{a}}
\newcommand{\bbb}{\mathfrak{b}}
\newcommand{\ccc}{\mathfrak{c}}
\newcommand{\ppp}{\mathfrak{p}}
\newcommand{\fff}{\mathfrak{f}}
\newcommand{\mmm}{\mathfrak{m}}
\newcommand{\defeq}{\vcentcolon=}
\newcommand{\defeqv}{\vcentcolon\equiv}
\newcommand{\Cov}{\mathrm{Cov}}
\renewcommand{\_}{\mathpunct{.}}
\newcommand{\?}{\,{:}\,}
\newcommand{\speak}[1]{\ulcorner\text{\textnormal{#1}}\urcorner}
\newcommand{\inv}{inv.\@}
\newcommand{\forces}{\vDash}
\newcommand{\ind}{\ensuremath{_\text{ind}}\xspace}
\newcommand{\sinf}{\ensuremath{_\infty}}
\newcommand{\impl}{\ensuremath{_\text{impl}}\xspace}
\newcommand{\formalized}{{\color{NavyBlue!75!White}{\raisebox{-0.5pt}{\scalebox{0.8}{\faCog}}}}}

\setbeamertemplate{blocks}[shadow=false]

\newenvironment{indentblock}{%
  \list{}{\leftmargin\leftmargin}%
  \item\relax
}{%
  \endlist
}

% Adapted from https://latex.org/forum/viewtopic.php?t=2251 (Stefan Kottwitz)
\newenvironment<>{hilblock}{
  \begin{center}
    \begin{minipage}{9.05cm}
      \setlength{\textwidth}{9.05cm}
      \begin{actionenv}#1
        \def\insertblocktitle{}
        \par
        \usebeamertemplate{block begin}}{
        \par
        \usebeamertemplate{block end}
      \end{actionenv}
    \end{minipage}
  \end{center}}

\newenvironment{changemargin}[2]{%
  \begin{list}{}{%
    \setlength{\topsep}{0pt}%
    \setlength{\leftmargin}{#1}%
    \setlength{\rightmargin}{#2}%
    \setlength{\listparindent}{\parindent}%
    \setlength{\itemindent}{\parindent}%
    \setlength{\parsep}{\parskip}%
  }%
  \item[]}{\end{list}}

\tikzset{
  invisible/.style={opacity=0,text opacity=0},
  visible on/.style={alt={#1{}{invisible}}},
  alt/.code args={<#1>#2#3}{%
    \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}}
}

% https://tex.stackexchange.com/questions/172336/drawing-roman-laurel-leaves-spqr-in-tikz
\tikzset{
  laurel-wreath/.pic = {
    \fill svg{M14.4-24.6c-1.5-1.5-2.6-3.3-3.1-5.3l-.4-1.7c-.2-1.1-.2-4.1 .2-5.7 .2-.9 .3-1.3 .5-1.3l1.4 1.1 2.5 2.4c2.7 2.5 5.2 6 5.8 8 .2 .6-.5 .3-2.2-.9-1.6-1.3-3.3-2.6-5-3.8l.1 1.4c.2 1.4 .5 2.7 1.1 4.6s.8 2.5 .5 2.5l-1.4-1.3zm69.6 1.1 .3-1.2c.8-2.3 1.3-4.8 1.6-7.3l-1.5 1.1c-1.3 .9-2.6 1.9-3.7 3-1.6 1.1-2 1.3-2.1 1 .7-1.8 1.6-3.4 2.8-4.9 1.3-1.7 6.5-6.8 7-6.8 .2 0 .3 .2 .3 .5l.3 1.6c.3 2.2 .2 5.7-.5 7.4-.8 1.9-1.6 3.1-3 4.7-1.1 1.1-1.4 1.3-1.5 .9z};
    \fill svg{M10-29.4c-.8-1.1-1.4-2.2-2-4.1l-.7-3.5c-.2-3 .2-4.4 1.4-8.3l.5-1.4c.2-1.3 .3-1.9 .6-1.9 .3-.2 .6 .3 .7 .8s.9 2.2 1.9 3.6c1.4 2.2 2.7 4.4 3.9 6.6l.9 2.7c0 .6 0 .6-.3 .6-.6 0-4.9-4.4-5.8-6l-.2-.6-.1 1.7-.3 2.8c-.3 2.7-.3 3.8 0 5.5 .6 2 .5 2.4-.5 1.5zm79.2 .3 .4-2.4c.2-1.3 .2-2.7-.1-4.9l-.3-2.8v-1.6l-.7 1c-.8 1.3-5 5.5-5.5 5.5s-.5-.3 .2-1.9c.5-1.7 1.4-3.3 3.3-6.5 2.4-3.6 2.7-3.9 2.8-4.7 .5-1.3 .5-1.4 .8-1.2 .3 0 .6 .8 .6 1.5l.7 2.4c.9 2.7 1.1 3.6 1.2 6 .2 3.1-.5 6-2 8.2-.8 1.3-1.3 1.7-1.4 1.5z};
    \fill svg{M5-40c-.4-3.2-.1-6.5 .9-9.6 .5-1.1 1.6-2.8 2.2-3.4l1.3-1.6 2-2.7 .2 .6c.1 1.3 .4 2.6 .9 3.8l.3 1c.8 1.7 1.1 2.7 1.6 5.3 .6 2.5 .6 4.6 .2 4.6-.3 0-.9-.8-1-1.1l-.5-.8c-1.4-2-3-5.2-2.9-6.5-.9 2.7-2 5.4-3.5 7.9l-.3 .8-.3 .8c0 .5-.6 1.6-.8 1.6l-.3-.7zm89.2 .2-.2-.5-.3-.9-1.1-2.7-1.1-2.4c-.6-1.4-1.2-2.8-1.6-4.2l-.3 .9c-.3 1.3-1.6 3.9-3 6-1.3 2-1.6 2-1.5 0s1.1-6.3 2.2-9c.8-1.7 1.1-3.1 .9-4.1-.2-1.1 .5-.8 2.2 1.8 3.3 4.4 3.8 5.4 4.4 7.8 .6 2.4 .5 7.7-.3 7.8l-.3-.5z};
    \fill svg{M13.9-50.1c-.5-1.9-.8-3.9-.9-5.8-.2-1.6-.1-3.3 .1-4.9-.3 .8-1.7 2.5-4.2 5.1l-3 4.9-.3 .1c-.3 0-.3-2.2 0-3.3 .8-3 1.4-4.6 2.5-6.1 .9-1.3 1.7-1.9 2.5-2.5 1.1-.6 2.7-1.9 3.5-2.7 .9-.9 1.9-1.4 2.2-1.4v1.1l-.3 6.6c0 6.8 .2 6.3-1 8.9-.5 1.1-.8 1.1-1.1 0zm70.8-.4c-.8-2.2-.8-2.5-.7-6.3-.1-2.7-.1-5.5-.2-8.2-.3-1.6-.3-1.9 .5-1.6l.6 .5c1.4 1.4 3 2.5 3.9 3.1 1.3 .9 1.9 1.6 2.7 2.6l.6 .7 .2 .4 .2 .3c.8 .9 2 4.9 2 6.9 .2 1.9-.2 1.9-.9 .5-.7-1.4-1.5-2.7-2.6-4-1.6-1.5-3-3.2-4.2-5 .4 3 .3 6-.5 9 0 .8-.5 2.2-.8 2.3-.2 0-.5-.3-.8-1.2z};
    \fill svg{M16.4-58.5l.2-1.5 .3-3.7c.2-2.8 .3-3.5 1.1-5.4l.7-1.3-.5 .4-1 .7c-.5 .4-1.1 .8-1.5 1.3l-.5 .3-1.9 1.6c-2.2 1.6-2.7 2-3.9 3.6-.5 .8-1.1 1.3-1.3 1.3-.5 0 0-2.4 1.1-4.7 1.5-3.4 4.3-6 7.7-7.4l1.3-.4 1.9-.4 2-.5c1.4 0 1.4 0 1 1.1-.5 .8-.8 2-1.1 4.2-.3 2.3-1.1 4.5-2.2 6.5l-.4 .6c-.6 1.1-1.3 2.1-2 3.2-.5 .6-.8 .8-1 .5zm66.3-.2c-.8-.9-2.8-4.4-3.5-6.1-.6-1.3-.9-2.5-1.1-3.5-.2-2.1-.7-4.1-1.5-6 0-.3 0-.3 1.2-.3l2.1 .5 1.9 .4 1.2 .4 .6 .1 1 .6c3 1.4 5.7 4.6 6.8 8.5l.7 2.6c-.2 .6-.5 .5-1.4-.7-2.2-2.7-4.8-5-7.7-6.9l-1.7-1.3 .6 1.3c.3 .6 .6 1.2 .8 1.9l.3 2.5 .3 3.9c.3 2.4 .2 2.8-.6};
    \fill svg{M21.6-66.1l.4-1.1 .9-3.2c.3-1.9 1.1-3.3 2.4-4.7l.4-.8-1.2 .2-2.2 .3c-2.7 .3-5.3 1.2-7.7 2.5-.6 .5-1.3 .6-1.3 .3 0-.5 .9-1.9 2-2.9 .8-.9 2-1.9 3.2-2.6l.9-.4 2.2-1c.3-.2 1.3-.3 3.2-.1 3 0 4.1 .2 6.3 .7l1.1 .4c.5 .2 .6 .6 .3 .6-.5 0-1.4 .9-1.9 1.7l-1.2 1.8c-1.7 2.8-2.2 3.5-4.6 5.9l-3 2.7-.2-.3zm53.9-2c-2.7-2.8-3.5-3.8-5.4-6.8-.9-1.6-1.4-2.4-1.9-2.5l-.8-.5c-.3 0-.2-.5 .4-.6l1.1-.4c1.9-.6 3-.8 5.6-.9l3.3 .2c2 .6 3.8 1.5 5.4 2.8 .3 0 1.9 1.6 2.5 2.4l.9 1.8c0 .3-.3 .2-1.9-.6-2.8-1.4-4.4-1.9-7.7-2.2l-2.2-.5c-.9-.2-.9-.2-.6 .2 .6 .5 1.7 2 2.1 2.8l.9 2.5c.3 1.5 .6 3 .9 4.6l-2.6-2.3z};
    \fill svg{M34.1-78.7c-3.4-1.3-6.9-2.1-10.6-2.5-.9 0-1.4 0-2.3 .3-2 .5-2 0 0-1.3l2.8-1.2c1.4-.5 1.9-.5 3.8-.6 3.8-.2 6.1 .3 9.3 1.7l3.6 1.1 2.2 .3c1.3 0 1.7 0 2.7-.3 1.1-.3 2.8-1.1 2.8-1.3l-1.3-.9c-1.9-1.4-3.1-2.7-3.1-3.2l.8-.6c.9-.3 1.3-.2 2 .8 .5 .8 1.1 1.4 2.9 2.7 .2 .3 .3 .2 1.1-.3 .9-.8 2.4-2 2.6-2.7 .5-.6 .9-.8 1.8-.5l.8 .6c0 .5-1.4 1.7-3.2 3.2l-1.3 .9c0 .2 1.7 .9 2.9 1.3 .9 .3 1.4 .3 2.7 .3l2.2-.3c1.7-.4 3.4-1 5-1.7 2-.8 4.4-1.3 7.7-1.1 2 .2 2.5 .2 3.8 .6 .9 .3 2.2 .8 2.8 1.2 2 1.1 2 1.6 .2 1.3-1.6-.3-1.9-.3-4.4 0-2.4 .3-4.7 .8-7 1.6l-1.5 .6c-2.9 .3-5.9 .2-8.8-.3-1.7-.3-3.6-.9-6-2.1l-1.1-.4-1.3 .6c-4.5 2.2-9.6 3-14.6 2.2zm-6.3-9.1c};
  }
}

\newcommand{\pointthis}[3]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=0,outer sep=0] (#2) {#2};
    \node[visible on=#1,overlay,rectangle callout,rounded corners,callout relative pointer={(0.3cm,0.5cm)},fill=blue!20] at ($(#2.north)+(-0.1cm,-1.1cm)$) {#3};
  }%
}

\tikzset{
  invisible/.style={opacity=0,text opacity=0},
  visible on/.style={alt={#1{}{invisible}}},
  alt/.code args={<#1>#2#3}{%
    \alt<#1>{\pgfkeysalso{#2}}{\pgfkeysalso{#3}}}
}

\newcommand{\hcancel}[5]{%
  \tikz[baseline=(tocancel.base)]{
    \node[inner sep=0pt,outer sep=0pt] (tocancel) {#1};
    \draw[red!80, line width=0.4mm] ($(tocancel.south west)+(#2,#3)$) -- ($(tocancel.north east)+(#4,#5)$);
  }%
}

\newcommand{\explain}[7]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=2pt,outer sep=0,fill=#3,rounded corners] (label) {#1};
    \node[anchor=north,visible on=<#2>,overlay,rectangle callout,rounded corners,callout
    relative pointer={(0.0cm,0.5cm)+(0.0cm,#6)},fill=#3] at ($(label.south)+(0,-0.3cm)+(#4,#5)$) {#7};
  }%
}

\newcommand{\explainstub}[2]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=2pt,outer sep=0,fill=#2,rounded corners] (label) {#1};
  }%
}

\newcommand{\squiggly}[1]{%
  \tikz[remember picture,baseline]{
    \node[anchor=base,inner sep=0,outer sep=0] (label) {#1};
    \draw[thick,color=red!80,decoration={snake,amplitude=0.5pt,segment
    length=3pt},decorate] ($(label.south west) + (0,-2pt)$) -- ($(label.south east) + (0,-2pt)$);
  }%
}

% Adapted from https://latex.org/forum/viewtopic.php?t=2251 (Stefan Kottwitz)
\newenvironment<>{varblock}[2]{\begin{varblockextra}{#1}{#2}{}}{\end{varblockextra}}
\newenvironment<>{varblockextra}[3]{
  \begin{center}
    \begin{minipage}{#1}
      \begin{actionenv}#4
        {\centering \hil{#2}\par}
	\def\insertblocktitle{}%\centering #2}
        \def\varblockextraend{#3}
	\usebeamertemplate{block begin}}{
        \par
        \usebeamertemplate{block end}
        \varblockextraend
      \end{actionenv}
    \end{minipage}
  \end{center}}

\setbeamertemplate{headline}{}

\setbeamertemplate{frametitle}{%
  \leavevmode%
  \vskip-1.6em%
  \begin{beamercolorbox}[dp=1ex,center,wd=\paperwidth,ht=2.25ex]{title}%
    \vskip0.5em%
    \bf\insertframetitle
  \end{beamercolorbox}%

  \vskip-0.77em\hspace*{-2em}%
  \textcolor{mypurpledark}{\rule[0em]{1.1\paperwidth}{2.4pt}}

  \vskip-0.4em%
}

\setbeamertemplate{navigation symbols}{}

\newcounter{framenumberpreappendix}
\newcommand{\backupstart}{
  \setcounter{framenumberpreappendix}{\value{framenumber}}
}
\newcommand{\backupend}{
  \addtocounter{framenumberpreappendix}{-\value{framenumber}}
  \addtocounter{framenumber}{\value{framenumberpreappendix}}
}

\newcommand{\insertframeextra}{}
\setbeamertemplate{footline}{%
  \begin{beamercolorbox}[wd=\paperwidth,ht=2.25ex,dp=1ex,right,rightskip=1mm,leftskip=1mm]{}%
    % \inserttitle
    \hfill
    \insertframenumber\insertframeextra\,/\,\inserttotalframenumber
  \end{beamercolorbox}%
  \vskip0pt%
}

\newcommand{\hil}[1]{{\usebeamercolor[fg]{item}{\textbf{#1}}}}
\newcommand{\hill}[1]{{\usebeamercolor[fg]{item}{#1}}}
\newcommand{\bad}[1]{\textcolor{red!90}{\textnormal{#1}}}
\newcommand{\good}[1]{\textcolor{mypurple}{\textnormal{#1}}}

\newcommand{\bignumber}[1]{%
  \renewcommand{\insertenumlabel}{#1}\scalebox{1.2}{\!\usebeamertemplate{enumerate item}\!}
}
\newcommand{\normalnumber}[1]{%
  {\renewcommand{\insertenumlabel}{#1}\!\usebeamertemplate{enumerate item}\!}
}
\newcommand{\bigheart}{\includegraphics{heart}}

\newcommand{\subhead}[1]{{\centering\textcolor{gray}{\hrulefill}\quad\textnormal{#1}\quad\textcolor{gray}{\hrulefill}\par}}

\newcommand{\badbox}[1]{\colorbox{red!30}{#1}}
\newcommand{\infobox}[1]{\colorbox{yellow!70}{\color{black}#1}}

% taken from JDH "The modal logic of arithmetic potentialism and the universal algorithm"
\DeclareMathOperator{\possible}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,rotate=45,line width=.1ex]{\draw (-1,-1) rectangle (1,1);}}}
\DeclareMathOperator{\necessary}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,line width=.1ex]{\draw (-1,-1) rectangle (1,1);}}}
\DeclareMathOperator{\xpossible}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,rotate=45,line width=.1ex]{\draw (-1,-1) rectangle (1,1); \draw[very thin] (-.6,-.6) rectangle (.6,.6);}}}
\DeclareMathOperator{\xnecessary}{\text{\tikz[scale=.6ex/1cm,baseline=-.6ex,line width=.1ex]{\draw (-1,-1) rectangle (1,1); \draw[very thin] (-.6,-.6) rectangle (.6,.6);}}}

\input{images/primes.tex}

\newcommand{\triang}{\hil{$\blacktriangleright$}}
\newcommand{\concat}{\mathbin{{+}\mspace{-8mu}{+}}}

\newcommand{\astikznode}[2]{\tikz[baseline,remember picture]{\node[anchor=base,inner sep=0,outer sep=0.1em] (#1) {#2};}}
\newcommand{\astikznodecircled}[3]{\tikz[baseline,remember picture]{\node[anchor=base,circle,draw=#2,thick,inner sep=0.05em,outer sep=0.05em] (#1) {#3};}}
\newcommand{\astikznodetransparentlycircled}[2]{\tikz[baseline,remember picture]{\node[anchor=base,circle,opacity=0,draw=white,text opacity=1,thick,inner sep=0.05em,outer sep=0.05em] (#1) {#2};}}

\setbeamersize{text margin left=1.60em,text margin right=1.60em}

\newlength\stextwidth
\newcommand\makesamewidth[3][c]{%
  \settowidth{\stextwidth}{#2}%
  \makebox[\stextwidth][#1]{#3}%
}

\newcommand{\dnote}[1]{%
  \begin{tabular}{@{}m{2em}@{}m{0.83\textwidth}@{}}%
    \textdbend &#1%
  \end{tabular}%
  \par
}

\newcommand{\genalpha}{\mbox{$\hspace{0.12em}\shortmid\hspace{-0.62em}\alpha$}}

\usepackage{newunicodechar}

\newunicodechar{∇}{\ensuremath{\nabla}}
\newunicodechar{λ}{\ensuremath{\lambda}}
\newunicodechar{σ}{\ensuremath{\sigma}}
\newunicodechar{τ}{\ensuremath{\tau}}
\newunicodechar{∷}{\ensuremath{\dblcolon}}
\newunicodechar{⧺}{\ensuremath{\!\!\!}}
\newunicodechar{₁}{\ensuremath{_1}}
\newunicodechar{₂}{\ensuremath{_2}}
\newunicodechar{∈}{\ensuremath{\in}}
\newunicodechar{ℕ}{\ensuremath{\NN}}
\newunicodechar{↠}{\ensuremath{\twoheadrightarrow}}
\newunicodechar{ʳ}{\ensuremath{^r}}

\begin{document}

\addtocounter{framenumber}{-1}

\definecolor{mypurpleblack}{RGB}{30,0,50}
\setbeamercolor{structure}{fg=black}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\centering\vspace*{-0em}\includegraphics[width=\paperwidth]{lost-melody-2}\end{minipage}}
\begin{frame}[c]
  \centering
  \color{white}

  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bigskip

  \scriptsize

  \setbeamercolor{block body}{bg=black!100}
  \begin{minipage}{0.40\textwidth}
    \begin{block}{}
      \centering\normalsize\color{white}
      \hil{\color{white} Proofs as programs?} \\[-0.4em]
      \
    \end{block}
  \end{minipage}

  \bigskip
  \bigskip
  \bigskip
  \bigskip
  \bf
  \colorbox{black}{\begin{minipage}{0.3\textwidth}
    \centering
    AI Transforms Math Research \\
    University of Augsburg \\
    August 26th, 2025
  \end{minipage}}
  \bigskip

  \colorbox{black}{\begin{minipage}{0.3\textwidth}
    \centering
    Ingo Blechschmidt \\
    University of Antwerp
  \end{minipage}}
\end{frame}}

\definecolor{mypurple}{RGB}{150,0,255}
\setbeamercolor{structure}{fg=mypurple}

\begin{frame}{In this talk}
  \bigskip
  \bigskip
  \begin{columns}
    \begin{column}{0.25\textwidth}
      \centering\footnotesize
      \includegraphics[height=2cm]{calabi-yau} \mbox{commutative algebra and}
      \\
      \mbox{number theory}
    \end{column}
    \begin{column}{0.2\textwidth}
      \centering\footnotesize
      \includegraphics[height=2cm]{turing-machine} \\ \mbox{numerical content}
    \end{column}
    \begin{column}{0.4\textheight}
      \centering\footnotesize
      \includegraphics[height=2cm]{3-adic-numbers} \\
      \mbox{a fractal} \mbox{without points}
    \end{column}
    \begin{column}{0.45\textheight}
      \centering\footnotesize
      \includegraphics[height=2cm]{cracks} \mbox{foundational crisis}
    \end{column}
  \end{columns}

  \medskip
  \medskip
  \medskip
  \medskip

  \begin{columns}
    \begin{column}{0.4\textheight}
      \centering\footnotesize
      \includegraphics[height=2cm]{multiverse} \mbox{traveling} \\
      the \mbox{multiverse}
    \end{column}
    \begin{column}{0.4\textheight}
      \centering\footnotesize
      \includegraphics[height=2cm]{monad} monadic side effects
    \end{column}
    \begin{column}{0.4\textheight}
      \centering\footnotesize
      \includegraphics[height=2cm]{hen-2} \\ proof assistants
    \end{column}
    \begin{column}{0.4\textheight}
      \centering\footnotesize
      \includegraphics[height=2cm]{alien} \\ alien algorithms
    \end{column}
  \end{columns}
\end{frame}

\NewEnviron{mining}[1][0.6\textwidth]{
  \includegraphics[height=2em,valign=c]{hammer-and-pick}\quad
  \colorbox{mypurple!10}{\begin{minipage}{#1}
    \BODY
  \end{minipage}}
}

\NewEnviron{simpleblock}{
  \colorbox{mypurple!10}{\begin{minipage}{\textwidth}
    \BODY
  \end{minipage}}
}

\renewcommand{\insertframeextra}{a}
{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\vspace*{4.3cm}\includegraphics[width=\paperwidth]{fr1-lighter}\end{minipage}}
\begin{frame}{A first glimpse of proof mining}
  \textbf{Theorem.} For every natural number~$n$, there is a prime number
  larger than~$n$.~\fixedhref{https://unimath.github.io/agda-unimath/elementary-number-theory.infinitude-of-primes.html}{\formalized}

  \emph{Proof (Euclid).} Every prime factor of~$n! + 1$ will do. \qed
  \pause

  \begin{mining}
    Let~$p_0, p_1, p_2, \ldots$ be the sequence of prime numbers.

    \textbf{Scholium.} $p_{n+1} \leq p_n! + 1$.

    \textbf{Scholium.} $p_n \leq 2^{2^n}$.
  \end{mining}
  \pause
  \bigskip

  \emph{Proof (Euler).} If there were only finitely many primes,
  the identity
  \[ \prod_p \frac{1}{1-1/p} = \sum_{n \geq 1} \frac{1}{n} \]
  would imply that the harmonic series converges. \qed

  \begin{mining}
    \textbf{Scholium.} $p_n \leq \lceil e^{n+1-\gamma} \rceil$.
  \end{mining}
\end{frame}}

% 1995: conjecture
% 2003: solution
% 2018: rate of convergence
\addtocounter{framenumber}{-1}
\renewcommand{\insertframeextra}{b}
\begin{frame}{Proof mining in convex analysis}
  \textbf{Theorem (zero displacement conjecture).}
  Let~$H$ be a Hilbert space. \newline
  Let~\mbox{$C_1, \ldots, C_N \subseteq H$} be nonempty
  closed convex subsets with orthogonal projections~$P_{C_i}$. Let~$T = P_{C_N}
  \circ \ldots \circ P_{C_1}$. Then for every~$x \in H$,
  \[ \| T^{n+1}x - T^nx \| \xrightarrow{n \to \infty} 0. \]

  \emph{Proof.} See
  \fixedhref{https://www.ams.org/journals/proc/2003-131-01/S0002-9939-02-06528-0/S0002-9939-02-06528-0.pdf}{[Bauschke
  2003]}, employing Minty's theorem, the Brézis--Haraux
  theorem, Rockafellar's maximal monotonicity and sum theorems, strongly
  nonexpansive mappings, conjugate functions, normal cones, \ldots \qed
  \pause

  \begin{mining}[0.85\textwidth]
    \textbf{Scholium
    \fixedhref{https://www2.mathematik.tu-darmstadt.de/~kohlenbach/inconsistentfeasibility.pdf}{[Kohlenbach
    2018]}.} In this situation, let~$b$ be an upper bound on the norm of~$x$ and let~$K$ be an
    upper bound on the norm of~$N$ arbitrary points $c_i \in C_i$. Then
    \[ \forall \varepsilon > 0\_
      \forall n \geq \phi(\varepsilon,N,b,K)\_
      \|T^{n+1}x - T^nx\| < \varepsilon, \]
    where~$\phi(\varepsilon,N,b,K)$ is given by a certain explicit formula.
  \end{mining}
\end{frame}

\addtocounter{framenumber}{-1}
\renewcommand{\insertframeextra}{c}
\begin{frame}{Proof mining in approximation theory}
  Let~$n \in \NN$. Let~$P_n$ be the space of polynomials of degree at most~$n$. \\
  Let~$f \in C[0,1]$ be a continuous function.

  \textbf{Theorem.} There is a \hil{unique} best~$L^1$-approximation of~$f$ in~$P_n$.
  \pause

  Let~$\omega$ be a \hil{modulus of uniform continuity} for~$f$,
  i.e. a function~$\mathbb{R}^+ \to \mathbb{R}^+$ such that
  \[ \forall x,\tilde x \in [0,1]\_ \forall \varepsilon > 0\_
    \bigl(|x-\tilde x| < \omega(\varepsilon) \Longrightarrow |f(x)-f(\tilde x)| <
    \varepsilon\bigr). \]

  \begin{mining}[0.85\textwidth]
    \textbf{Scholium
    \fixedhref{https://www2.mathematik.tu-darmstadt.de/~kohlenbach/Keele.pdf}{[Kohlenbach
    1990]}.} $\forall \varepsilon > 0\_ \forall p_1,p_2 \in P_n\_$
    \[
      \bigwedge_{i=1}^2 \bigl(\|f - p_i\|_1 - \operatorname{dist}_1(f, P_n) <
      \phi(\omega,n,\varepsilon)\bigr) \Longrightarrow \|p_1 - p_2\|_1 \leq
      \varepsilon, \]
    where~$\phi(\omega,n,\varepsilon)$ is given by a certain explicit formula.
  \end{mining}
\end{frame}
\renewcommand{\insertframeextra}{}

\begin{frame}{Backed by logical metatheorems?}
  \hil{Metatheorems} for backing proof mining have been and are being developed which \ldots
  \begin{enumerate}
    \small
    \item[{\includegraphics[height=1em,valign=c]{emoji-abacus}}] guarantee the
    \hil{extractability} of suitable numerical information in principle \\
    (bounds, convergence rates, moduli of uniqueness, rates of asymptotic
    regularity, \ldots),
    \item[{\includegraphics[height=1em,valign=c]{emoji-robot}}] describe an \hil{algorithm} for carrying out the extraction and
    \item[{\includegraphics[height=1em,valign=c]{emoji-package}}] support \hil{modular treatments} of auxiliary lemmas,
  \end{enumerate}
  \bad{\textbf{provided}} the input proof is \hil{formally} supplied in a
  \hil{certain system}.
  \fixedhref{https://www2.mathematik.tu-darmstadt.de/~kohlenbach/novikov.pdf}{[Kohlenbach--Oliva 2002]}
  \pause

  \bad{\textbf{In practice (2025):}} Algorithms \bad{\textbf{not}} used, only followed
  as \bad{\textbf{rough guidelines}}, combined with hand-rolled optimizations.
  \hil{Let us explore tool support!}
  \pause

  NB: The \hil{quality} of the extracted data depends on the
  \hil{sophistication} of the \hil{logical~principles} used in the proof
  (Heine--Borel, Bolzano--Weierstraß, \ldots).
\end{frame}

{\usebackgroundtemplate{\begin{minipage}{\paperwidth}\centering\vspace*{-0em}\includegraphics[width=\paperwidth]{curry-howard-faded}\end{minipage}}
\newcommand{\connection}[1]{$\cdots\includegraphics[height=1em]{#1}\cdots$}
\begin{frame}{Curry--Howard's Rosetta stone}
  \bigskip
  \centering
  \renewcommand{\arraystretch}{1.3}
  \begin{tabular}{r@{}c@{}l}
    \hil{mathematics} & & \hil{programming} \\
    proving a claim & \connection{emoji-thinking} & implementing a function \\
    stating a claim & \connection{emoji-megaphone} & writing down a type signature \\
    using a lemma & \connection{emoji-link} & calling a function \\
    {\ \ \ \ \,}coming up with an auxiliary lemma & \connection{emoji-lightbulb} & coming up with an auxiliary function \\
    committing a logical error & \connection{emoji-cross} & committing a type error \\
    reasoning circularly & \connection{emoji-cyclone} & getting stuck in an infinite loop \\
    \pause
    --- & \connection{emoji-explosion} & encountering a runtime bug
  \end{tabular}
  \pause

  \begin{hilblock}
    \centering
    To extract numerical data from a proof, \\
    \hil{run the proof}.
  \end{hilblock}
\end{frame}}

\newcommand{\laterbad}[1]{\only<1>{#1}\only<2->{\bad{#1}}}
\begin{frame}{Three case studies}
  \bigskip
  \begin{columns}[c]
    \begin{column}{0.15\textwidth}
      \scalebox{0.23}{\sieve{7}{7}}
    \end{column}
    \begin{column}{0.85\textwidth}
      \begin{simpleblock}
        \justifying
        \textbf{Theorem.}
        For every natural number~$n$, there is a prime larger than~$n$.
        \fixedhref{https://unimath.github.io/agda-unimath/elementary-number-theory.infinitude-of-primes.html}{\formalized}
      \end{simpleblock}
      \\[0.3em]

      \emph{Proof.} Every prime factor of~$n! + 1$ will do. \qed
    \end{column}
  \end{columns}
  \bigskip

  \begin{columns}[c]
    \begin{column}{0.15\textwidth}
      \includegraphics[width=\textwidth,valign=t]{monad}
    \end{column}
    \begin{column}{0.85\textwidth}
      \begin{simpleblock}
        \textbf{Theorem.}
        Every infinite sequence~$f : \NN \to \NN$ is \emph{good}
        in that there are numbers $i < j$ such that~$f(i) \leq f(j)$.
        \fixedhref{https://lets-play-agda.quasicoherent.io/Padova2025.ComputationalContent.Dickson.html}{\formalized}
      \end{simpleblock}
      \\[0.3em]

      \emph{Proof.} There is a \laterbad{minimal value}~$f(i)$. Set~$j \defeq i+1$. \qed
    \end{column}
  \end{columns}
  \bigskip

  \begin{columns}[c]
    \begin{column}{0.15\textwidth}
      \includegraphics[width=\textwidth,valign=t]{calabi-yau}
    \end{column}
    \begin{column}{0.85\textwidth}
      \begin{simpleblock}
        \justifying
        \textbf{Theorem.}
        Let~$M$ be a surjective matrix with more rows than columns over a
        commutative ring~$A$. Then~$1 = 0$ in~$A$.
        \fixedhref{https://iblech.github.io/constructive-maximal-ideals/Krull.Dynamical.html\#example}{\formalized}
      \end{simpleblock}
      \\[0.3em]

      \justifying\emph{Proof.}
      \laterbad{Assume not.} Then there is a \laterbad{maximal ideal}~$\mmm$.
      The matrix is still surjective over~$A/\mmm$. Since~$A/\mmm$ is a field, this
      is a contradiction to basic linear algebra. \qed
    \end{column}
  \end{columns}
\end{frame}

\renewcommand{\insertframeextra}{a}
\begin{frame}{A case study in commutative algebra}
  \begin{simpleblock}
    \textbf{Theorem.}
    Let~$M$ be a surjective matrix with more rows than columns over a
    commutative ring~$A$. Then~$1 = 0$ in~$A$.
    \fixedhref{https://iblech.github.io/constructive-maximal-ideals/Krull.Dynamical.html\#example}{\formalized}
  \end{simpleblock}
  \\[0.3em]

  \justifying\emph{Proof.}
  \bad{Assume not.} Then there is a \bad{maximal ideal}~$\mmm$.
  The matrix is still surjective over~$A/\mmm$. Since~$A/\mmm$ is a field, this
  is a contradiction to basic linear algebra. \qed

  {\centering\scalebox{0.9}{\begin{tikzpicture}
    \node (0) at (0,1) {$(0) = \{0\}$};
    \node (1) at (0,5) {$(1) = \ZZ$};
    \node (2) at (-2,4) {$(2)$};
    \node [right of=2] (3) {$(3)$};
    \node [below of=2] (4) {$(4)$};
    \node [below of=2, xshift=0.7cm] (6) {$(6)$};
    \node [right of=3] (5) {$(5)$};
    \node [right of=5] (7) {$(7)$};
    \node [right of=7] (7d) {$\ldots$\phantom{(}};
    \node [right of=7d, xshift=1cm, yshift=-1cm] (max)
    {\small\it maximal among the proper ideals};
    \node [below of=4] (8) {$(8)$};
    \node [right of=8, xshift=3cm] (8d) {$\ldots$};
    \draw (0) -- (8);
    \draw (0) -- (8d);
    \draw (0) -- (6);
    \draw (2) -- (1);
    \draw (3) -- (1);
    \draw (5) -- (1);
    \draw (7) -- (1);
    \draw (7d) -- (1);
    \draw (4) -- (2);
    \draw (8) -- (4);
    \draw (6) -- (2);
    \draw (6) -- (3);
    \draw [mypurple!30, thick, shorten <=-2pt, shorten >=-2pt, ->] (max) to [out=120, in=-30] (7d);
    \begin{pgfonlayer}{background}
      \draw[decorate, very thick, draw=mypurple!30]
        ($(2.south west) + (8pt, 0)$) arc(270:180:8pt) --
        ($(2.north west) + (0, -8pt)$) arc(180:90:8pt) --
        ($(7d.north east) + (-8pt, 0)$) arc(90:0:8pt) --
        ($(7d.south east) + (0, 8pt)$) arc(0:-90:8pt) --
        cycle;
    \end{pgfonlayer}
  \end{tikzpicture}}\par}
  \pause

  \begin{mining}[0.8\textwidth]\emph{Proof.}
  Write~$M = \left(\begin{smallmatrix}x\\y\end{smallmatrix}\right)$. By surjectivity,
  have~$u, v \in A$ with
  $
    u \left(\begin{smallmatrix}x\\y\end{smallmatrix}\right) = \left(\begin{smallmatrix}1\\0\end{smallmatrix}\right)
  $ and $
    v \left(\begin{smallmatrix}x\\y\end{smallmatrix}\right) = \left(\begin{smallmatrix}0\\1\end{smallmatrix}\right)
  $.
  Hence
  $
    1 = (vy)(ux) = (uy)(vx) = 0
  $. \qed
  \end{mining}
\end{frame}

\addtocounter{framenumber}{-1}
\renewcommand{\insertframeextra}{b}
\begin{frame}{Maximal ideals as convenient fictions?}
  \begin{itemize}
    \item[\triang] In \bad{classical mathematics}, every ring has a maximal ideal
    by \bad{Zorn's lemma}.
    \bigskip\pause

    \item[\triang] Without \bad{Zorn}, at least every \bad{countable} ring
    $A = \{ x_0, x_1, \ldots \}$ has a maximal ideal.

    \small
    -- Iterative construction given
    an ideal membership test
    \fixedhref{https://link.springer.com/article/10.1007/BF01454872}{[Krull
    1929]}:
    \begin{align*}
      \mmm_0 &= \{ 0 \}, &
      \mmm_{n+1} &= \begin{cases}
        \mmm_n + (x_n), & \text{if $1 \not\in \mmm_n + (x_n)$}, \\
        \mmm_n, & \text{else.}
      \end{cases}
      \intertext{\visible<3->{-- Also without membership test!
      \fixedhref{https://citeseerx.ist.psu.edu/document?repid=rep1&type=pdf&doi=a7ff57cacdad6735040459dcf450b231948dbb2f}{[Krivine
      1996]},
      \fixedhref{https://www.sciencedirect.com/science/article/pii/S0168007204000181}{[Berardi--Valentini
      2004]}}}
      \action<3->{\mmm_0 &= \{ 0 \}, &
      \mmm_{n+1} &= \mmm_n + (\underbrace{\{ x_n \,|\, 1 \not\in \mmm_n + (x_n)
      \}}_{\text{a certain subsingleton set}})}
    \end{align*}
    \bigskip
    \pause
    \pause

    \normalsize
    \justifying
    \item[\triang] Without \bad{Zorn}, \hil{every} ring has a maximal ideal in
    a ``suitable \hil{forcing extension} of the universe''
    \fixedhref{https://raw.githubusercontent.com/iblech/constructive-maximal-ideals/master/tex/extended.pdf}{[B.--Schuster
    2024]}.
    In plain terms:
    \hil{Approximate} a (perhaps non-existing) surjection~$\NN \twoheadrightarrow A$
    by partial functions which can \hil{grow on demand}.
  \end{itemize}
\end{frame}
\renewcommand{\insertframeextra}{}

\end{document}

Beyond verified correctness and collaborative proof engineering: Proofs as programs?

A century ago, Hilbert called upon the mathematical community to explain how to
extract concrete numerical content from abstract proofs involving transfinite
methods. For instance, from a qualitative proof of the existence of a limit, we
might hope to extract a quantitative bound on the rate of convergence. Proof
assistants based on modern type theory offer the tantalizing prospect of
facilitating such extraction by running formalized proofs as programs—adding
value to mechanization beyond verified correctness and collaborative proof
engineering. In the talk, we will explore a case study from commutative algebra
on this kind of proof mining, obtained in joint work with Peter Schuster.

- Start:
  - classical logic fairy tale?
  - overview as in Swansea talk

- A glimpse of proof mining
  - Euclid proof
  - Euler proof
  - Successes of proof mining in diverse fields
  - Example: running Euclid

- A case study in algebra
  - Textbook proof
  - Issue: Zorn's lemma
  - Issue: LEM

- Motto: Running proofs as effectful programs

- Brunerie?
- Hilbert & certificates
- Extracted algorithms are nontrivial, cf. implicational wqo

- Applications of AI:
  - automatic application of metalogical extraction techniques
  - support for refactoring proofs (for instance for inserting ¬¬'s)
  - resulting constructive proofs/algorithms can look "alien" (= artificial intelligence)