% Based on the arxiv-paper-reader Beamer template.
% Compile with: python3 build_slides.py slides.en.tex
\documentclass[aspectratio=169,11pt]{beamer}
\usepackage[T1]{fontenc}
\usepackage[utf8]{inputenc}
\usepackage{amsmath,amssymb,graphicx,booktabs}
\usepackage{tikz}
\usetikzlibrary{arrows.meta,positioning}

\definecolor{AcademicBlue}{RGB}{26,57,86}
\definecolor{AcademicTeal}{RGB}{0,105,112}
\definecolor{SoftGray}{RGB}{243,246,249}
\setbeamercolor{structure}{fg=AcademicBlue}
\setbeamercolor{frametitle}{fg=AcademicBlue,bg=white}
\setbeamercolor{title}{fg=AcademicBlue}
\setbeamercolor{alerted text}{fg=AcademicTeal}
\setbeamercolor{block title}{fg=white,bg=AcademicBlue}
\setbeamercolor{block body}{fg=black,bg=AcademicBlue!5}
\setbeamertemplate{navigation symbols}{}
\setbeamertemplate{itemize items}[circle]
\setbeamertemplate{footline}{%
  \hfill\usebeamerfont{page number in head/foot}%
  \insertframenumber\,/\,\inserttotalframenumber\hspace{4mm}\vspace{3mm}}
\setbeamersize{text margin left=8mm,text margin right=8mm}
\setbeamerfont{frametitle}{size=\Large,series=\bfseries}
\setbeamerfont{title}{size=\LARGE,series=\bfseries}
\setbeamerfont{block title}{size=\normalsize,series=\bfseries}
\setbeamertemplate{itemize/enumerate body begin}{\setlength{\itemsep}{5pt}}
\newcommand{\papersource}[1]{\par\smallskip{\scriptsize\color{gray}#1\par}}
\newcommand{\E}{\mathbb{E}}
\newcommand{\OPT}{\operatorname{OPT}}
\newcommand{\SRev}{\operatorname{SRev}}
\newcommand{\BRev}{\operatorname{BRev}}
\newcommand{\STR}{\operatorname{STR}}
\newcommand{\PoA}{\operatorname{PoA}}
\newcommand{\pFPA}{\mathsf{pFPA}}
\pdfstringdefDisableCommands{\def\translate#1{#1}}

\title[Cogentic]{Cogentic: Multi-Agent Orchestration\texorpdfstring{\\}{ }for Automated Proof Discovery}
\subtitle{Research paper discussion \textbar\ 25-minute main talk}
\author{Paper by Yang Cai, Vineet Gupta, Yanchen Jiang,\texorpdfstring{\\}{ }
Christopher Liaw, Aranyak Mehta, Grigoris Velegkas, and Di Wang}
\institute{Google Research \textbar\ Additional affiliations: Yale; Google DeepMind}
\date{arXiv:2609.40324v1 \textbar\ 30 September 2026\\
Reading prepared 3 October 2026}

\begin{document}

\begin{frame}
  \titlepage
  \vspace{-5mm}
  \begin{center}
    \color{AcademicTeal}\textbf{Turn failed proof attempts into reusable, verified progress.}
  \end{center}
  \papersource{\href{https://arxiv.org/abs/2609.40324v1}{arxiv.org/abs/2609.40324v1}. A reading presentation; not authored by the paper's authors.}
\end{frame}

\begin{frame}{Open problems require progress across attempts}
  \begin{block}{Research question}
    How can a language model explore competing proof directions,\newline
    overcome subtle errors, and preserve useful intermediate results?
  \end{block}
  \begin{itemize}
    \item \textbf{Search:} one plausible approach can stall at a technical gap.
    \item \textbf{Verification:} natural-language arguments lack a cheap, faithful score.
    \item \textbf{Memory:} correct lemmas and failed conjectures need different treatment.
  \end{itemize}
  \medskip
  Cogentic produces mathematical prose for expert review.
  \papersource{Paper, Sec. 1, PDF pp. 1--2.}
\end{frame}

\begin{frame}{Each round writes the starting point for the next}
  \centering
  \includegraphics[width=\linewidth,height=0.68\textheight,keepaspectratio]{figures/fig-01-overview.pdf}
  \par\medskip
  \textbf{Plan $\rightarrow$ prove $\rightarrow$ verify $\rightarrow$ retain progress.}
  \papersource{Original Fig. 1, PDF p. 3. Reused from the authors' TeX assets.}
\end{frame}

\begin{frame}{Independent briefings preserve different approaches}
  \begin{columns}[T,onlytextwidth]
    \column{0.47\textwidth}
    \begin{block}{Orchestrator}
      Assigns a claim, bound, construction, counterexample search, or repair task.
      \medskip

      Allocates prover slots and manages shared files.
    \end{block}
    \column{0.49\textwidth}
    \begin{block}{Summarizer $\rightarrow$ prover}
      Selects relevant attempts, critiques, and verified lemmas.
      \medskip

      Each briefing is produced independently; the prover chooses its next step.
    \end{block}
  \end{columns}
  \medskip
  Long documents are passed as paths for selective reading.\newline
  Literature reviewers can return when a technical barrier persists.
  \papersource{Paper, Secs. 2--2.1, PDF pp. 2--4. Functional roles follow Sec. 2.1; Fig. 1's caption calls the briefing writer an advisor.}
\end{frame}

\begin{frame}{Acceptance requires two scopes of adversarial review}
  \begin{columns}[T,onlytextwidth]
    \column{0.47\textwidth}
    \begin{block}{One draft at a time}
      Check the candidate's steps, assumptions, and citations.
    \end{block}
    \column{0.49\textwidth}
    \begin{block}{All drafts in the round}
      Compare arguments and identify shared blind spots.
    \end{block}
  \end{columns}
  \medskip
  \[
    \operatorname{Accept}(P_i)=
    V_{\mathrm{local}}(P_i)\land V_{\mathrm{cross}}(P_i;\mathcal P_r)
  \]
  $P_i$: a candidate proof; $\mathcal P_r$: the round's proof batch.\newline
  Both reviewers demand justification rather than presume correctness.
  \papersource{Paper, Sec. 2.2, PDF p. 4. Equation is explanatory notation, not a paper equation. No verifier error rate is reported.}
\end{frame}

\begin{frame}{A rejected proof can still contribute a valid lemma}
  \begin{columns}[T,onlytextwidth]
    \column{0.47\textwidth}
    \begin{block}{Record of attempts}
      Target claim, attempted method, and the objection that defeated it.
      \medskip

      Supports allocation and avoids repeating errors.
    \end{block}
    \column{0.49\textwidth}
    \begin{block}{Verified ledger}
      Extract a valid fragment.\newline
      State it as a self-contained lemma.\newline
      Verify it again in isolation.\newline
      Make it available to later provers.
    \end{block}
  \end{columns}
  \medskip
  Verified counterexamples also exclude unattainable targets.\newline
  \alert{The memory unit is a checked claim with conditions.}
  \papersource{Paper, Sec. 2.3, PDF p. 4. ``Verified'' denotes the system's review process.}
\end{frame}

\begin{frame}{Process adaptation and final writing get separate checks}
  \begin{itemize}
    \item A \textbf{process advisor} reads logs across rounds: repeated gaps, missed errors, and weak review standards.
    \item It adjusts instructions and advises on allocation. The advisor and orchestrator may not supply their own mathematical opinions.
    \item After a proof passes, exploration may continue for a stronger result.
  \end{itemize}
  \medskip
  \begin{block}{Consolidation}
    Compare accepted proofs $\rightarrow$ write a complete manuscript\newline
    $\rightarrow$ audit the manuscript against the accepted argument.
  \end{block}
  \papersource{Paper, Secs. 2.4--2.5, PDF pp. 4--5. ``Formal writer'' means mathematical exposition here, not proof-assistant certification.}
\end{frame}

\begin{frame}{The evidence consists of five research results}
  \begin{itemize}
    \item \textbf{Setting:} open questions in online learning, auction theory, and mechanism design, chosen within the authors' expertise.
    \item \textbf{Engine:} Gemini; roughly $O(100)$ calls for most problems and $O(1000)$ for the hardest, as reported by the authors.
    \item \textbf{Validation:} domain experts subsequently checked the proofs; companion papers develop the mathematics.
  \end{itemize}
  \medskip
  Table 1 compares \alert{mathematical bounds}. It is not a controlled comparison of agent architectures.
  \papersource{Paper, Secs. 1 and 3, PDF pp. 1, 5--6. Exact per-task tokens, costs, and model configuration are not provided.}
\end{frame}

\begin{frame}{Inverse optimization achieves finite total shortfall}
  $\mathbb B$: unit ball in $\mathbb R^d$; hidden $w^*\in\mathbb B$; compact $X_t\subseteq\mathbb B$.
  \[
    x_t\in\arg\max_{x\in X_t}\langle w^*,x\rangle,
    \qquad R_T=\sum_{t=1}^T\langle w^*,x_t-\hat x_t\rangle.
  \]
  \begin{block}{Theorem 1}
    Deterministic, proper, anytime algorithm with $R_T=O(d)$ for all $T$.\newline
    Per round: $O(d^2)$ arithmetic \textbf{plus one linear optimization}.
  \end{block}
  \begin{itemize}
    \item Proper: commit to a nonzero linear objective estimate \emph{before} seeing $X_t$.
    \item Prior efficient bound: $O(d\ln T)$; prior $O(d)$ rule was improper and costly.
  \end{itemize}
  \papersource{Paper, Sec. 3.1, Theorem 1, PDF pp. 5--7. $\hat x_t$: learner's action; $d$: dimension.}
\end{frame}

\begin{frame}{A decreasing trace potential removes the horizon term}
  $g_t=-v_t$, with $v_t$ a unit separation direction; $H_t$ is a metric.
  \[
    s_t=\sqrt{g_t^\top H_t^{-1}g_t},\qquad
    \Phi_t=\operatorname{tr}(H_t^{-1/2}).
  \]
  Self-normalize the rank-one metric increment by $s_t$. Then
  \[
    \Phi_t-\Phi_{t+1}\ge\frac{\tau}{4}s_t^2,\quad
    \Phi_1=d,\quad\Phi_t\ge0
    \ \Longrightarrow\ 
    \sum_t s_t^2\le\frac{4d}{\tau}=O(d^2).
  \]
  Metric scale $\tau$ and iterate step $\alpha$ are both $\Theta(1/d)$:
  \[
    R_T=O\!\left(1/\alpha+\alpha\sum_t s_t^2\right)=O(d).
  \]
  \papersource{Paper, Sec. 3.1, PDF pp. 6--7. The paper also notes a later, inefficient tight $O(\sqrt d)$ bound; efficient $O(\sqrt d)$ remains open in this account.}
\end{frame}

\begin{frame}{Two extra sellers suffice on the smaller side}
  \begin{block}{Theorem 2: a two-sided Bulow--Klemperer result}
    $m$ buyers, $n$ sellers, $m\ge n\ge1$. Buyer values first-order stochastically dominate seller costs.
    \[
      \STR(m,n+2)\ \ge\ \OPT(m,n).
    \]
  \end{block}
  \begin{itemize}
    \item Compare expected gains from trade: Seller Trade Reduction in the expanded market vs. first-best in the original market.
    \item Prior constant recruitment bound: at least 20,000 agents \emph{per side}.
    \item Adding just one seller is insufficient, even starting from $m=n=1$, within the stated mechanism restrictions.
  \end{itemize}
  \papersource{Paper, Sec. 3.2, Theorem 2, PDF p. 7; Table 1, p. 6. Table 1 specifies DSIC, IR, weak budget balance for the lower bound; the theorem summary says prior-independent.}
\end{frame}

\begin{frame}{With many experts, anytime has no leading-order price}
  Loss vectors lie in $[0,1]^n$; regret is relative to the best fixed expert.
  \[
    \underbrace{\sqrt{t\ln n/2}}_{\text{fixed horizon}}
    \qquad\text{vs.}\qquad
    \underbrace{\sqrt{t\ln n}}_{\text{previous anytime guarantee}}.
  \]
  \begin{block}{Theorem 3}
    Without knowing the horizon, simultaneously for all $t\ge1$:
    \[
      R_t\le\left(1+O\!\left(\sqrt{\frac{\ln\ln n}{\ln n}}\right)\right)
      \sqrt{\frac{t\ln n}{2}}.
    \]
  \end{block}
  The relative overhead vanishes as \alert{$n\to\infty$}.\newline
  This is not exact equality for each fixed number of experts.
  \papersource{Paper, Sec. 3.3, Theorem 3, PDF pp. 7--8. For two experts, a strict anytime penalty is known.}
\end{frame}

\begin{frame}{Limit each instance's lifetime to bound aggregation cost}
  A multiplicative-weights instance for each $H^m=(1+\varepsilon)^m$:
  \[
    \text{wake at }\lfloor\delta H^m\rfloor,
    \qquad\text{retire after }\lfloor H^m\rfloor.
  \]
  \centering
  \begin{tikzpicture}[x=0.15cm,y=0.54cm,>=Latex]
    \draw[->,gray] (0,0)--(67,0) node[right,font=\scriptsize]{time};
    \foreach \a in {0,8,16,32,64}
      \draw[gray] (\a,0.10)--(\a,-0.10) node[below,font=\scriptsize]{\a};
    \foreach \endx/\startx/\yy in {8/2/1,16/4/2,32/8/3,64/16/4}{
      \draw[AcademicTeal,line width=3pt] (\startx,\yy)--(\endx,\yy);
      \node[left,font=\scriptsize] at (0,\yy) {$H^m=\endx$};
    }
    \draw[AcademicBlue,dashed] (12,0)--(12,4.5) node[above,font=\scriptsize]{$t=12$};
  \end{tikzpicture}
  \par\smallskip\raggedright
  At time $t$, only $O(\varepsilon^{-1}\log\delta^{-1})$ instances are awake.\newline
  A similar bound on arrivals during each lifetime controls mass redistribution.
  \papersource{Paper, Sec. 3.3, PDF p. 8. Diagram is a teaching example: grid ratio 2, $\delta=1/4$; not the theorem's optimized parameters.}
\end{frame}

\begin{frame}{Simple selling mechanisms guarantee a 3.52 approximation}
  One additive buyer; values of the $n$ items are independent.
  \[
    M=\max\{\SRev,\BRev\},\qquad \OPT\le3.52M.
  \]
  \begin{columns}[T,onlytextwidth]
    \column{0.47\textwidth}
    \begin{block}{Simple mechanisms}
      $\SRev$: best separate posted prices.\newline
      $\BRev$: best price for the grand bundle.
    \end{block}
    \column{0.49\textwidth}
    \begin{block}{Comparison}
      Approximation factor: $5.2\to3.52$.\newline
      Guaranteed share: $19.23\%\to28.41\%$ of optimal revenue.
    \end{block}
  \end{columns}
  \medskip
  These shares are reciprocals of worst-case bounds.\newline
  The best known lower bound on the factor is 2.
  \papersource{Paper, Sec. 3.4, Theorem 4, PDF p. 8. Percentage conversions are explanatory calculations, not measured revenue gains.}
\end{frame}

\begin{frame}{Truncating at a joint revenue scale simplifies the proof}
  Let $V=\sum_jv_j$ and $M_{\max}=\max_jv_j$. Duality gives
  \[
    \OPT\le\SRev+\E[V-M_{\max}].
  \]
  Truncate at $M=\max\{\SRev,\BRev\}$ rather than at $\SRev$:
  \[
    V_M=\sum_{j=1}^n\min\{v_j,M\},\qquad
    \E[V-M_{\max}]\le\E[V_M].
  \]
  \begin{itemize}
    \item The non-favorite welfare is controlled by one truncated quantity.
    \item Extremal bounds on $\E[V_M^2]$, at fixed mean, constrain $\E[V_M]/M$.
    \item The main paper sketches this route; the companion supplies the full constant calculation.
  \end{itemize}
  \papersource{Paper, Sec. 3.4, PDF pp. 8--9. The inequalities concern expectations under the independent-value setting.}
\end{frame}

\begin{frame}{Randomized proportional allocation improves autobidding}
  Prior-free autobidding with return-on-spend (RoS) constraints.
  \[
    \PoA=\frac{\text{optimal allocation welfare}}{\text{worst equilibrium welfare}}
    \qquad\text{(smaller is better)}.
  \]
  \begin{block}{$r$-Proportional First-Price Auction: $\pFPA_r$}
    Bidder $i$ wins query $j$ with probability
    \[
      x_{i,j}=\frac{b_{i,j}^r}{\sum_{k=1}^n b_{k,j}^r}.
    \]
    The winner pays its own bid; an unopposed bidder wins for free.
  \end{block}
  $r$ controls how strongly allocation favors the highest bid.\newline
  Deterministic mechanisms face a PoA barrier of 2 in this setting.
  \papersource{Paper, Sec. 3.5, PDF p. 9. $b_{i,j}$: bid; $n$: number of bidders.}
\end{frame}

\begin{frame}{Two bidders admit 1.5; general $n$ improves on 2}
  \begin{columns}[T,onlytextwidth]
    \column{0.47\textwidth}
    \begin{block}{Two bidders}
      \[
        \PoA(\pFPA_1)\le1.5.
      \]
      Previous bound: 1.8.\newline
      Matching lower bound for the stated anonymous mechanism class and assumptions.
    \end{block}
    \column{0.49\textwidth}
    \begin{block}{General $n\ge2$}
      \[
        \PoA(\pFPA_{2n})\le2-\frac1{4n+1}.
      \]
      Requires \textbf{undominated bids}: no feasible bid increase can win more while respecting RoS.
    \end{block}
  \end{columns}
  \medskip
  For even $n$, an anonymous-mechanism lower bound is $2-4/(n+4)$.\newline
  The general result matches the \alert{order of the $1/n$ improvement},\newline
  while the two-bidder constant is tight in the stated class.
  \papersource{Paper, Theorem 5, PDF p. 9; Table 1, p. 6 specifies anonymous, monotone mechanisms for the two-bidder optimum.}
\end{frame}

\begin{frame}{The supplied prompts already shape the research target}
  \begin{itemize}
    \item \textbf{Two-sided markets:} the prompt specifies STR and asks for exactly two additional sellers.
    \item \textbf{Two-bidder autobidding:} both proportional allocation and the 1.5 conjecture are supplied.
    \item \textbf{Many experts:} the target is the existing conjecture that the anytime price tends to 1.
    \item \textbf{Simple revenue:} the prompt asks for factor 3, with factor 4 as a fallback; the reported result is 3.52.
  \end{itemize}
  \medskip
  \alert{Autonomous proof development occurs inside an expert-defined task.}
  \papersource{Paper, Appendix A.2--A.5, PDF pp. 15--17; Sec. 3.5, p. 10.}
\end{frame}

\begin{frame}{Expert checking and later refinement remain part of the story}
  \begin{itemize}
    \item The authors report no human mathematical intervention \textbf{during the runs}; experts subsequently checked the proofs.
    \item Autobidding initially assumed strictly positive values on all queries. Appendix A.5 says Gemini was later asked to remove that assumption.
    \item Human authors improved exposition, literature context, and in some cases extended the results.
  \end{itemize}
  \begin{block}{A practical bottleneck}
    Candidate generation can outpace expert reading. Formal verification may help checking; understanding still takes work.
  \end{block}
  \papersource{Paper, Sec. 3, PDF p. 5; Sec. 4, p. 10; Appendix A.5, pp. 16--17.}
\end{frame}

\begin{frame}{The next system study should isolate the sources of gain}
  \begin{columns}[T,onlytextwidth]
    \column{0.47\textwidth}
    \begin{block}{What this paper establishes}
      Five reported mathematical advances, an explicit workflow, and expert-reviewed outputs.
    \end{block}
    \column{0.49\textwidth}
    \begin{block}{What is not isolated}
      Equal-budget agent baselines, module ablations, verifier error rates, and a denominator of attempted problems.
    \end{block}
  \end{columns}
  \medskip
  \textbf{Suggested experiments (reader's analysis):}
  \begin{itemize}
    \item Remove the ledger or cross-draft verifier at matched compute.
    \item Trace which verified lemmas were reused in the final proof.
    \item Report failed tasks and the human effort needed to accept a result.
  \end{itemize}
  \papersource{Assessment of the evidence in Secs. 1--4, PDF pp. 1--10. Proposed experiments are not reported results.}
\end{frame}

\begin{frame}{The reusable idea is evidence-bearing memory}
  \begin{enumerate}
    \item \textbf{Explore independently.}\newline
      Give provers distinct directions and selected views of history.
    \item \textbf{Review at several scopes.}\newline
      Check individual arguments, shared blind spots, isolated lemmas, and the final manuscript.
    \item \textbf{Retain partial success.}\newline
      Keep failed attempts as history and rechecked claims as reusable premises.
  \end{enumerate}
  \medskip
  \alert{Five mathematical advances make this workflow worth studying.}\newline
  Its component-level benefits remain to be measured.
  \papersource{Synthesis of Secs. 2--4, PDF pp. 2--10.}
\end{frame}

\begin{frame}{Primary paper and companion results}
  \textbf{Cai et al. (2026), Cogentic}\newline
  \href{https://arxiv.org/abs/2609.40324v1}{arXiv:2609.40324v1} \textbar\ 30 September 2026
  \medskip
  \begin{itemize}
    \item Inverse optimization: \href{https://arxiv.org/abs/2609.13440}{arXiv:2609.13440}.
    \item Two-sided markets: \href{https://arxiv.org/abs/2609.27304}{arXiv:2609.27304}.
    \item Anytime experts: \href{https://arxiv.org/abs/2609.27206}{arXiv:2609.27206}.
    \item Simple revenue: \href{https://arxiv.org/abs/2609.28873}{arXiv:2609.28873}.
    \item Autobidding: \emph{Efficiency of Generalized Proportional First-Price Auctions Under Auto-bidding}, listed as forthcoming in v1.
  \end{itemize}
  \papersource{Companion references as listed in the primary paper, PDF p. 11. This talk follows the primary paper's statements and proof sketches. Project: \href{https://sites.google.com/view/cogentic}{sites.google.com/view/cogentic}.}
\end{frame}

\appendix

\begin{frame}{Backup: a round updates three different kinds of state}
  \[
    S_r=(A_r,L_r,I_r)
  \]
  $A_r$: attempts and critiques; $L_r$: verified claims; $I_r$: standing instructions.
  \begin{enumerate}
    \item Plan directions and produce independent briefings from $S_r$.
    \item Generate candidates; apply local and cross-draft verification.
    \item Append attempts and objections to $A_{r+1}$.
    \item Extract fragments, restate them, and reverify before adding to $L_{r+1}$.
    \item Review logs to update $I_{r+1}$ and guide the next round.
  \end{enumerate}
  \papersource{Teaching abstraction of Secs. 2.1--2.4, PDF pp. 4--5. The paper does not specify this state tuple as an algorithm.}
\end{frame}

\begin{frame}{Backup: why the awake pool is independent of time}
  Ignoring floors for the count, instance $m$ is awake when
  \[
    \delta H^m\le t\le H^m
    \quad\Longrightarrow\quad
    t\le H^m\le t/\delta.
  \]
  On the grid $H^m=(1+\varepsilon)^m$, the pool size is
  \[
    O\!\left(1+\frac{\log(1/\delta)}{\log(1+\varepsilon)}\right)
    =O\!\left(\varepsilon^{-1}\log\delta^{-1}\right).
  \]
  The missed prefix is handled recursively, costing
  \[
    1+\sqrt\delta+\delta+\cdots=\frac1{1-\sqrt\delta}.
  \]
  Set $\varepsilon=\sqrt{\ln\ln n/\ln n}$ and $\delta=\varepsilon^3$ for large $n$.
  \papersource{Expanded explanation of the proof sketch in Sec. 3.3, PDF p. 8. Full analysis also controls arrivals and aggregation regret.}
\end{frame}

\begin{frame}{Backup: keep the two autobidding mechanisms separate}
  With two positive bids $(1,2)$, the allocation probabilities are
  \[
    r=1:\ (1/3,2/3),\qquad r=4:\ (1/17,16/17).
  \]
  \begin{center}
  \begin{tabular}{lcc}
    \toprule
    Setting & Mechanism & Reported PoA upper bound\\
    \midrule
    Two-bidder result & $\pFPA_1$ & $1.5$\\[3pt]
    General result at $n=2$ & $\pFPA_4$ & $17/9\approx1.889$\\[3pt]
    General result at $n=10$ & $\pFPA_{20}$ & $81/41\approx1.976$\\
    \bottomrule
  \end{tabular}
  \end{center}
  \medskip
  The general bound assumes undominated bids.\newline
  The bid example illustrates allocation, not an equilibrium or a PoA proof.
  \papersource{Teaching calculations from the mechanism and Theorem 5, Sec. 3.5, PDF p. 9.}
\end{frame}

\end{document}