\documentclass[11pt]{article} \usepackage[T1]{fontenc} \usepackage{lmodern} \usepackage[margin=1in]{geometry} \usepackage{amsmath,amssymb,amsthm} \usepackage{booktabs,longtable,array} \usepackage{microtype} \usepackage[colorlinks=true,linkcolor=blue,citecolor=blue,urlcolor=blue]{hyperref} \hypersetup{pdftitle={Linchpin Theorems},pdfauthor={}} \setlength{\emergencystretch}{2em} \newtheorem{linchpin}{Statement}[section] \newtheorem{proposition}[linchpin]{Proposition} \newtheorem{lemma}[linchpin]{Lemma} \theoremstyle{remark} \newtheorem{remark}[linchpin]{Remark} \numberwithin{equation}{section} \newcommand{\N}{\mathbb N} \newcommand{\Z}{\mathbb Z} \newcommand{\Q}{\mathbb Q} \newcommand{\R}{\mathbb R} \newcommand{\C}{\mathbb C} \newcommand{\F}{\mathbb F} \newcommand{\PP}{\mathbb P} \newcommand{\eps}{\varepsilon} \newcommand{\adiff}{\operatorname{adiff}} \providecommand{\dotminus}{\dot{-}} \newcommand{\rank}{\operatorname{rank}} \newcommand{\vol}{\operatorname{vol}} \newcommand{\SO}{\operatorname{SO}} \newcommand{\so}{\mathfrak{so}} \newcommand{\ord}{\operatorname{ord}} \newcommand{\status}[1]{\par\smallskip\noindent\textit{Status.} #1\par\smallskip} \newcommand{\doi}[1]{\href{https://doi.org/#1}{\nolinkurl{doi:#1}}} \newcommand{\arxiv}[1]{\href{https://arxiv.org/abs/#1}{arXiv:#1}} \title{Linchpin Theorems} \author{} \date{} \begin{document} \maketitle \begin{abstract} A proof assistant checks a formal proposition. It does not check that the proposition expresses the mathematics that its author intended. This distinction becomes pressing when large bodies of mathematics are autoformalized. We propose the use of \emph{linchpin theorems}: statements whose meanings can be audited with relatively little mathematical infrastructure, and whose proofs connect them to substantial results. Examples range from sphere packing and the classification of Lie algebras to regularity theory, the Weil conjectures, and computational complexity. Some linchpins are equivalent reformulations. Others are consequences, or stronger conjectures. We specify the direction of each implication and the background theorems used in the connection. A linchpin is an instrument of audit, not an end in itself. A proof that bypasses the mathematics under audit can expose a weakness of the instrument. \end{abstract} \section{Introduction} The conclusion of a long formal proof can be difficult to read. A theorem about varieties, manifolds, or automorphic representations may depend for its meaning on hundreds of definitions. A human auditor who wishes to know whether an autoformalization has proved the intended theorem must look beyond the final line. The definitions, conventions, and hypotheses are part of the claim. A small trusted kernel addresses a different problem. It checks that the formal conclusion follows from the formal premises. It cannot determine whether a definition of a smooth variety, a packing, or a computation captures the intended concept. A translation error may leave a well-typed, provable proposition. Autoformalization therefore increases the value of statements whose mathematical meanings are easy to inspect. Pollack \cite{Pollack} makes this distinction between checking a derivation and understanding the informal meaning of its conclusion. We call such a statement a \emph{linchpin} when it is chosen to audit a specified body of mathematics. A useful linchpin has a short statement, few prerequisites for understanding that statement, and a documented connection with the theorem under audit. It may involve only finite counting or polynomial equations. These are useful features, not requirements. An intelligible statement about continuous maps may serve better than an opaque encoding by natural numbers. The intended arrangement is as follows. A substantial theorem \(T\) is formalized, and a statement \(L\) is derived from it. A human checks the meaning of \(L\), while the proof assistant checks its derivation from \(T\) and the supporting library. The bridge from \(T\) to \(L\) must itself be included in the formal development. This reduces the amount of specialized language at the point of human inspection. It does not eliminate the need to examine premises, axioms, or dependencies. Autoformalization by language models is already an active subject \cite{Autoformalization}. Our concern here is the mathematical interface presented to an auditor, independently of the method used to produce the formal text. We use the word \emph{linchpin} informally. It describes a role in an audit, not a new logical property of propositions. In particular, a consequence does not recover all the content of its source. Several consequences may be needed to test different parts of a development. Nor does a citation establish that a theorem is indispensable to a proof. A published proof may use a theorem that another proof avoids. Linchpins are not ends in themselves. Suppose that a proposed linchpin for a deep theorem acquires a proof that bypasses that theorem, whether by a human argument or by autoformalization. The new proof may be valuable mathematics. For the proposed audit, however, it shows that the linchpin did not serve its purpose. One should then seek a better linchpin. It would be a mistake to protect the choice of statement at the expense of the purpose for which it was chosen. There are four kinds of connection in this paper. An \emph{equivalent reformulation} satisfies \(T\Longleftrightarrow L\), using specified background results. A \emph{downstream consequence} satisfies \(T\Longrightarrow L\); we make no converse claim. A \emph{stronger conjectural formulation} implies the conjecture under discussion, without a known reverse implication. Finally, some theorems already have suitable statements and require no reformulation. Equivalence is always relative to established background mathematics. A short reduction can use a substantial representation theorem. We identify these inputs rather than include their cost in the word \emph{elementary}. For open problems, these statements are proposals for a future audit, as well as ways of isolating the content of the conjecture. We do not give new proofs of the underlying deep results. The contribution is the selection of statements, their precise elementary forms, and the connections between them. The arguments below are mathematical reductions; they have not been checked in a proof assistant. \subsection*{Prior work and challenge theorems} Validation by consequences has a substantial history in formal methods. Rushby \cite[\S2.3.2]{Rushby} proposes \emph{formal challenges}: putative theorems that should follow if a specification expresses its intended meaning. Madlener, Smetsers, and van Eekelen \cite{Madlener} use the term \emph{challenge theorems} in a published validation of a storm-surge barrier's control system. A challenge may test a single expected property. The term requires neither broad coverage of the specification nor a mathematically elementary statement. Linchpins adapt this practice to the audit of substantial mathematics, with particular emphasis on the simplicity of the statement and the amount of mathematical content retained. These are additional aims, not a disjoint classification of statements. The single-curve Sato--Tate statement in \S\ref{sec:st} and the filling inequality in \S\ref{sec:almgren} are close to challenge theorems: each tests a restricted part of its source. The family version in \S\ref{sec:st}, however, recovers the full non-CM Sato--Tate theorem over \(\Q\). Allowing all ambient dimensions in the filling inequality still tests only a particular application of Almgren regularity. A close precedent within formalized mathematics is Topaz's account of the Liquid Tensor Experiment \cite{Topaz}. Proved examples and characterizations make its definitions accessible for inspection and guard against unintended trivializations. More recently, implication probes have been proposed for evaluating autoformalizations \cite{MohammadSheikh}. Our contribution is the selection and analysis of mathematical statements for this purpose, with explicit bridges and limits on what each statement audits. We make no claim to originate validation by consequences. \subsection*{Guide to the examples} The source theorem and the strength retained by each proposed linchpin are listed below. The Almgren example is deliberately included as a provisional choice: it illustrates the distinction between a documented dependency and a convincing audit of a theorem's full strength. {\small \begin{longtable}{@{}>{\raggedright\arraybackslash}p{.24\textwidth} >{\raggedright\arraybackslash}p{.39\textwidth} >{\raggedright\arraybackslash}p{.29\textwidth}@{}} \toprule Source & Linchpin & Connection\\ \midrule \endhead Kepler conjecture & Integer points in a box, \S\ref{sec:kepler} & Equivalent to the HOL Light statement\\ Sato--Tate & Cubic congruences and Catalan moments, \S\ref{sec:st} & Equivalent for the specified curves\\ Riemann hypothesis & Three arithmetic criteria, \S\ref{sec:rh} & Each equivalent; open\\ Fundamental lemma & Twelve-square counts at primes, \S\ref{sec:fl} & Downstream from the unitary case\\ Finite simple groups & Six assignable entries; prime-power rearrangements, \S\ref{sec:cfsg} & Two classification consequences\\ Complex simple Lie algebras & A commutator-closed space of skew matrices, \S\ref{sec:lie} & Downstream through Borel's theorem\\ Almgren regularity & A sharp polyhedral filling inequality, \S\ref{sec:almgren} & Downstream; provisional as an audit\\ Poincar\'e conjecture & A polynomial with two critical points, \S\ref{sec:poincare} & Equivalent in dimension three\\ Weil conjectures & Hypersurface counts; Ramanujan's \(\tau\), \S\ref{sec:weil} & Equivalent to the RH part; downstream\\ Birch--Swinnerton-Dyer & Point-count products; rational triangles, \S\ref{sec:bsd} & Stronger than rank BSD; conditional consequence\\ \(\mathsf P\ne\mathsf{NP}\) & Polynomial local updates on a line, \S\ref{sec:pnp} & Equivalent; open\\ Boolean Pythagorean triples; \(S(5)=160\) & Finite coloring statements, \S\ref{sec:coloring} & Original statements, already elementary\\ \bottomrule \end{longtable} } \subsection*{Conventions} We write \(\N=\{0,1,2,\ldots\}\), \([n]=\{1,\ldots,n\}\), and \(\#S\) for the cardinality of a finite set. On \(\N\), put \[ a\mathbin{\dotminus}b=\max(a-b,0),\qquad \adiff(a,b)=(a\mathbin{\dotminus}b)+(b\mathbin{\dotminus}a). \] Thus \(\adiff(a,b)=|a-b|\), without leaving the natural numbers. Ranks of rational or integer matrices are taken over \(\Q\), unless another field is indicated. Limits over primes use all primes outside the finite exceptional set that is specified. Finite lists, integer matrices, and rational numbers can be encoded by natural numbers. We usually leave these encodings implicit. Positive denominators may be cleared in a finite rational inequality. Neither convention removes an unbounded quantifier or supplies a rate of convergence. \section{The Kepler conjecture}\label{sec:kepler} For \(x,y\in\N^3\), define \[ d(x,y)=\sum_{i=1}^3\adiff(x_i,y_i)^2. \] Here \(d\) is the squared Euclidean distance. \begin{linchpin}[Integer packings in a box]\label{lp:kepler} For all integers \(m\ge1\) and \(n\ge0\), and every set \(S\subseteq\{0,\ldots,mn\}^3\), if \[ x,y\in S,\quad d(x,y)<4m^2\quad\Longrightarrow\quad x=y, \] then \begin{equation}\label{eq:keplerbox} 32(\#S)^2\le(n+2)^6. \end{equation} \end{linchpin} \status{A theorem, equivalent to the proposition \texttt{the\_kepler\_conjecture} in the HOL Light formalization \cite[\S3]{Flyspeck}.} The normalization is that of spheres of radius one. Dividing coordinates by \(m\) gives centers separated by at least \(2\), which explains the factor \(4m^2\). Put \[ \rho=\frac1{4\sqrt2},\qquad \alpha=\frac{4\pi}{3}\rho=\frac{\pi}{\sqrt{18}}. \] The number \(\rho\) is the optimal number of centers per unit volume. The HOL Light proposition, written in mathematical notation, is \begin{equation}\label{eq:holkepler} \forall V\subseteq\R^3,\quad \operatorname{packing}(V)\ \Longrightarrow\ \exists c\in\R\ \forall r\ge1,\quad \#(V\cap B(0,r))\le\alpha r^3+cr^2, \end{equation} where distinct points of a packing have distance at least \(2\). The constant \(c\) is allowed to depend on \(V\). \begin{proposition} Statements \eqref{eq:keplerbox} and \eqref{eq:holkepler} are equivalent. \end{proposition} \begin{proof} Assume \eqref{eq:holkepler}, and set \(P=S/m\). The periodic set \[ W=P+(n+2)\Z^3 \] is a packing. Points in different copies are separated by at least \(2\) in some coordinate. A fundamental cube has volume \((n+2)^3\) and contains \(\#S\) centers. Counting fundamental cubes that meet the boundary of a large ball gives \[ \lim_{r\to\infty}\frac{\#(W\cap B(0,r))}{(4\pi/3)r^3} =\frac{\#S}{(n+2)^3}. \] Apply \eqref{eq:holkepler} and let \(r\) tend to infinity. This gives \(\#S\le\rho(n+2)^3\), and hence \eqref{eq:keplerbox}. For the reverse implication, first consider a packing with cubic period \(T>0\) and \(q\) centers in a half-open fundamental cube. A block of \(k^3\) cubes contains \(qk^3\) centers. Choose an integer \(n_k\) with \(kT2(r+2)\). For each translate \(\Lambda+t\), delete its points in \(B(Tz,r+2)\), for every \(z\in\Z^3\), and insert \(F+Tz\). The result is a periodic packing. If \[ M(t)=\#((\Lambda+t)\cap B(0,r+2)), \] its number of centers per period is \(\rho T^3-M(t)+N\). By \eqref{eq:periodic}, \(N\le M(t)\). Averaging \(t\) over a fundamental cube gives \[ N\le\rho\,\vol B(0,r+2)=\alpha(r+2)^3. \] Indeed, the average number of points of a translated lattice in a bounded measurable set is its volume divided by the lattice covolume; this follows by integrating the sum of the indicator functions of its lattice translates. A packing has finitely many centers in any bounded ball, so the estimate applies to \(F=V\cap B(0,r)\). For \(r\ge1\), \[ (r+2)^3\le r^3+26r^2. \] This proves \eqref{eq:holkepler}, even with \(c=26\alpha\) independent of \(V\). \end{proof} The shift by \(2\) avoids an unspecified boundary constant. An equivalent alternative is \[ \exists C\in\N\ \forall m,n\ge1\ \forall S,\qquad 32(\#S)^2\le n^6+Cn^5 \] under the same packing hypotheses. Statement \ref{lp:kepler} gives \(C=728\), by expanding \((n+2)^6\). Conversely, this alternative gives \eqref{eq:periodic} by the same block argument. The exponent \(5\) cannot be replaced by \(4\). For \(k\ge1\), set \(n=\lceil\sqrt2\,k\rceil\), and choose \(\sqrt2\rho(n+\sqrt2-1)^3. \] Thus \(N^2-n^6/32\) is bounded below by a positive constant times \(n^5\). Clearing denominators gives integer examples. Both the separation threshold and the boundary exponent matter. \section{Sato--Tate from cubic congruences}\label{sec:st} Let \(C_j=\frac1{j+1}\binom{2j}{j}\) be the Catalan numbers. They can also be defined by \(C_0=1\) and \(C_{j+1}=\sum_{i=0}^j C_iC_{j-i}\). For each prime \(p\ne2,31\), put \[ A_p=\#\{(x,y)\in\{0,\ldots,p-1\}^2: y^2\equiv x^3+x+1\pmod p\}, \qquad h_p=\min\{h\in\N:h^2\ge p\}, \] and \(b_p=(p+2h_p)\mathbin{\dotminus} A_p\). Write \(\mathcal P_X=\{p\le X:p\text{ prime},\ p\ne2,31\}\). \begin{linchpin}[Catalan moments of cubic counts]\label{lp:st} For every \(k\in\N\), \begin{equation}\label{eq:stmom} \lim_{X\to\infty}\frac1{\#\mathcal P_X} \sum_{p\in\mathcal P_X}\left(\frac{b_p}{h_p}\right)^k =C_{k+1}. \end{equation} \end{linchpin} \status{A theorem, equivalent to Sato--Tate for \(y^2=x^3+x+1\). The nonintegral-\(j\) theorem of Harris--Shepherd-Barron--Taylor suffices \cite{HSBT}.} This statement tests one curve. It does not by itself recover the theorem for all non-CM elliptic curves; the family version below does. The curve has discriminant \(-16\cdot31\) and \(j=6912/31\). It has no complex multiplication, since a rational complex-multiplication \(j\)-invariant is an integer \cite{SilvermanAdvanced}. The affine count \(A_p\) omits one point at infinity. Consequently the Frobenius trace is \(a_p=p-A_p\). Hasse's bound \(|a_p|\le2\sqrt p\) \cite{Silverman} shows that the truncated subtraction loses nothing and that \[ z_p:=b_p/h_p=2+a_p/h_p\in[0,4],\qquad \left|z_p-\left(2+a_p/\sqrt p\right)\right|\le2/h_p\longrightarrow0. \] Sato--Tate says that \(a_p/(2\sqrt p)\) has limiting density \((2/\pi)\sqrt{1-t^2}\) on \([-1,1]\). After the change of variable \(z=2+2t\), the density is \[ d\nu(z)=\frac1{2\pi}\sqrt{z(4-z)}\,dz,\qquad 0\le z\le4. \] A beta integral gives \begin{equation}\label{eq:catalanmom} \int_0^4z^k\,d\nu(z) =\frac1{k+2}\binom{2k+2}{k+1}=C_{k+1}. \end{equation} Thus Sato--Tate implies \eqref{eq:stmom}. Conversely, convergence of these moments gives convergence against every polynomial. Polynomial approximation on \([0,4]\) gives convergence against every continuous function. The vanishing rounding error then recovers Sato--Tate. This is the full distribution statement for the curve, including the signs of its traces. For an entirely arithmetic version, let \(X\ge3\), \(D_X=X!\), \(G_X=\#\mathcal P_X\), and \[ U_{k,X}=\sum_{p\in\mathcal P_X} \bigl(b_p(D_X/h_p)\bigr)^k. \] The divisions are exact. Statement \ref{lp:st} is equivalent to \begin{equation}\label{eq:stnat} \begin{gathered} \forall k\ge0\ \forall q\ge1\ \exists X_0\ge3\ \forall X\ge X_0,\\ q\,\adiff(U_{k,X},C_{k+1}G_XD_X^k)\le G_XD_X^k. \end{gathered} \end{equation} In this form there are no real numbers in the statement. The same construction applies to \[ y^2=x^3+Ax+B,\qquad A,B\in\Z,\qquad D=4A^3+27B^2\ne0, \] using primes \(p\nmid2D\). The elementary condition \(D\nmid6912A^3\) says that \(j=6912A^3/D\) is not an integer. Quantifying \eqref{eq:stmom} over this family is equivalent to the nonintegral-\(j\) case of Sato--Tate over \(\Q\). One can cover every non-CM elliptic curve over \(\Q\) by excluding the following fixed set: \[ \begin{split} J=\{&0,\ 12^3,\ -15^3,\ 20^3,\ -32^3,\ 2\cdot30^3,\ 66^3,\\ &-96^3,\ -3\cdot160^3,\ 255^3,\ -960^3,\ -5280^3,\ -640320^3\}. \end{split} \] These are the rational CM \(j\)-invariants, from the classical class-number-one classification \cite{Cox}. Replace the nonintegrality condition by \[ 6912A^3\ne cD\quad\text{for every }c\in J. \] Every elliptic curve over \(\Q\) admits an integral short Weierstrass equation. Changes of model affect only finitely many excluded primes. The resulting family of moment assertions is therefore equivalent to the full non-CM Sato--Tate theorem over \(\Q\) \cite[Corollary 8.9]{BLGHT}. This last equivalence uses the classification of rational CM invariants in addition to the elementary moment argument. \section{Three formulations of the Riemann hypothesis}\label{sec:rh} The following three statements retain different features of the Riemann hypothesis. The first has the shortest notation. The second asks for finite certificates of approximation. The third consists entirely of universal rational inequalities. \subsection{Squarefree counting} Let \(E(n)\) and \(O(n)\) count the squarefree integers in \([n]\) with, respectively, an even and an odd number of distinct prime factors. The integer \(1\) is counted in \(E(n)\). Put \(D(n)=\adiff(E(n),O(n))\). \begin{linchpin}[Squarefree cancellation]\label{lp:mobius} For every integer \(k\ge1\), there is \(N\ge1\) such that \[ D(n)^{2k}\le n^{k+1}\qquad(n\ge N). \] \end{linchpin} \status{Open; equivalent to the Riemann hypothesis.} Let \(M(x)=\sum_{a\le x}\mu(a)\), where \(\mu\) is the M\"obius function. Then \(D(n)=|M(n)|\). Littlewood's criterion states \[ \mathrm{RH}\quad\Longleftrightarrow\quad M(x)=O_\eps(x^{1/2+\eps})\quad\text{for every }\eps>0; \] see \cite{Littlewood,Soundararajan}. Under RH use \(\eps=1/(4k)\) and absorb the constant into \(n^{1/2}\) after raising to the power \(2k\). Conversely, choose \(k\) arbitrarily large. The direction from cancellation to RH has a short explanation. Partial summation makes \[ s\int_1^\infty M(x)x^{-s-1}\,dx \] holomorphic on \(\Re s>1/2\). It agrees with \(1/\zeta(s)\) on \(\Re s>1\), so the zeta function has no zeros to the right of the critical line. Its functional equation gives the remaining assertion. The reverse implication is the substantial analytic part of the criterion. \subsection{Approximation by remainders} Write \(r_d(n)\) for the remainder on dividing \(n\) by \(d\). For \(m\ge2\) and \(c_2,\ldots,c_m\in\Q\), put \[ F_c(n)=\sum_{d=2}^m c_d r_d(n),\qquad B_c=1+\sum_{d=2}^m |c_d|(d-1). \] \begin{linchpin}[Finite remainder certificates]\label{lp:remainders} For every integer \(q\ge1\), there are integers \(m\ge2\), \(N\ge1\) and rational numbers \(c_2,\ldots,c_m\) such that \begin{equation}\label{eq:remainder} q\left(\sum_{n=1}^{N}\frac{(1-F_c(n))^2}{n(n+1)} +\frac{B_c^2}{N+1}\right)<1. \end{equation} \end{linchpin} \status{Open; equivalent to RH by the Nyman--Beurling--B\'aez-Duarte criterion, in its sequence form.} The sequence criterion says that RH is equivalent to the constant sequence \(1\) belonging to the closed linear span of the remainder sequences in the norm \[ \|f\|^2=\sum_{n=1}^\infty\frac{|f(n)|^2}{n(n+1)}. \] Bagchi gives this precise sequence version \cite[Theorem 1]{Bagchi}, using the fractional parts \(r_d(n)/d\), which have the same linear span. Its analytic antecedents are \cite{Nyman,Beurling,BaezDuarte}. Real coefficients suffice by taking real parts, and rational coefficients suffice by finite-dimensional approximation. Since \(|1-F_c(n)|\le B_c\), the omitted tail has the explicit bound \[ \sum_{n>N}\frac{(1-F_c(n))^2}{n(n+1)} \le B_c^2\sum_{n>N}\left(\frac1n-\frac1{n+1}\right) =\frac{B_c^2}{N+1}. \] This proves one implication. For the other, first choose an approximation with squared norm less than \(1/(2q)\), then make \(B_c^2/(N+1)<1/(2q)\). Every witness to \eqref{eq:remainder} is checked by a finite rational calculation. Borisov's work connects this circle of ideas with factorial ratios and quotient singularities \cite{Borisov}. It provides a relevant geometric context, but the remainder criterion above is attributed to the Nyman--Beurling--B\'aez-Duarte theory. \subsection{A rational form of Lagarias's inequality} Set \[ H_n=\sum_{j=1}^n\frac1j,\qquad \sigma(n)=\sum_{d\mid n}d. \] For rational \(h\ge1\) and integer \(m>h\), define \[ U_m(h)=\left(\frac{m}{m-h}\right)^m,\qquad V_m(h)=(h-1)\sum_{j=0}^{m-1}\frac1{m+j(h-1)}. \] \begin{linchpin}[Divisor sums and rational upper bounds]\label{lp:lagarias} For every \(n\ge1\) and every \(m\ge n+1\), \begin{equation}\label{eq:lagariasrational} \sigma(n)\le H_n+U_m(H_n)V_m(H_n). \end{equation} \end{linchpin} \status{Open; equivalent to RH by Lagarias's theorem \cite{Lagarias}, which uses Robin's work \cite{Robin}.} Lagarias's criterion is \begin{equation}\label{eq:lagarias} \sigma(n)\le H_n+e^{H_n}\log H_n\qquad(n\ge1). \end{equation} For fixed \(h\ge1\), the exponential limit gives \(U_m(h)\ge e^h\) and \(U_m(h)\to e^h\). The quantity \(V_m(h)\) is the left Riemann sum for \(\int_1^h dt/t\), so \(V_m(h)\ge\log h\) and \(V_m(h)\to\log h\). These quantities are nonnegative. Thus \eqref{eq:lagarias} implies \eqref{eq:lagariasrational}; letting \(m\to\infty\) proves the converse. All denominators are positive because \(H_n\le n8(p^5+1)\}. \] Then \begin{equation}\label{eq:12sign} \forall q\ge1\ \exists X_0\ge3\ \forall X\ge X_0,\qquad q\,\adiff(2A(X),P(X))\le P(X). \end{equation} The positive and negative halves of the semicircle each have measure \(1/2\). Statement \eqref{eq:12sign} is therefore downstream from Statement \ref{lp:12squares}, but it loses most of the distribution theorem. The integer count itself can be written using only natural numbers: \[ R_{12}(n)= \sum_{\substack{x_1,\ldots,x_{12}\in\{0,\ldots,n\}\\ x_1^2+\cdots+x_{12}^2=n}} 2^{\,\#\{i:x_i>0\}}. \] Replacing a limit by its quantified definition and clearing the finite denominators gives an arithmetic statement, as in \eqref{eq:stnat}. No modular forms or Galois representations occur in the resulting statement. \section{Consequences of the classification of finite simple groups} \label{sec:cfsg} A list \(a=(a_0,\ldots,a_{n-1})\) will be called a \emph{rearrangement} if its entries are precisely \(0,\ldots,n-1\), each occurring once. For two rearrangements define \[ a*b=(a_{b_0},\ldots,a_{b_{n-1}}). \] A nonempty set of rearrangements closed under this operation is a permutation group: powers of any element give the identity and its inverse. The following statements avoid group-theoretic terminology in their hypotheses and conclusions. \begin{linchpin}[Six freely assignable entries]\label{lp:six} Let \(n\ge6\), and let \(S\) be a set of rearrangements of \(0,\ldots,n-1\). Suppose that \(a*b\in S\) whenever \(a,b\in S\). Suppose also that, for every six pairwise distinct numbers \(y_0,\ldots,y_51\), and let \(S\) be a composition-closed set of rearrangements such that, for every \(y0\), there is a rational polyhedral chain \(Q\) with integer coefficients such that \[ \partial Q=P,\qquad \mathbf M_g(Q)<\mathbf M_g(T)+\eps. \] \end{lemma} \begin{proof} Write \(\mathbf M\) for Euclidean mass. We first obtain polyhedral chains with real vertices, integer coefficients, the exact boundary \(P\), and convergent Euclidean mass. Integral polyhedral approximation \cite[\S\S4.2.21--4.2.22]{Federer} gives chains \(B_j\) with \(\mathbf M(B_j)\to\mathbf M(T)\) and decompositions \[ T-B_j=U_j+\partial V_j,\qquad \mathbf M(U_j)+\mathbf M(V_j)\longrightarrow0, \] where \(U_j,V_j\) are integral currents and all supports lie in a fixed compact set. This is approximation in the integral flat norm, so the correction currents also have integer multiplicities. Since \(\partial U_j=P-\partial B_j\) is polyhedral, the integral deformation theorem \cite[\S4.2.9]{Federer}, with mesh \(\delta_j\), gives \[ U_j=R_j+E_j+\partial Z_j, \] where \(R_j,E_j\) are integral polyhedral chains and \[ \begin{aligned} \mathbf M(R_j)&\le C\bigl(\mathbf M(U_j) +\delta_j\mathbf M(\partial U_j)\bigr),\\ \mathbf M(E_j)&\le C\delta_j\mathbf M(\partial U_j),\qquad \mathbf M(Z_j)\le C\delta_j\mathbf M(U_j). \end{aligned} \] Here \(C\) depends only on the dimensions. The fact that the boundary is polyhedral makes the boundary error \(E_j\) polyhedral as well; see also the two-step argument in \cite[\S1.2]{CFM}. Choose \(\delta_j\to0\) with \(\delta_j\mathbf M(\partial U_j)\to0\), and set \(A_j=B_j+R_j+E_j\). Then \[ \partial A_j=P,\qquad T-A_j=\partial(V_j+Z_j). \] Thus \(A_j\to T\) in flat norm and \(\limsup\mathbf M(A_j)\le\mathbf M(T)\); lower semicontinuity gives \(\mathbf M(A_j)\to\mathbf M(T)\). The deformation moves supports by at most a constant times \(\delta_j\), so a common compact set still contains them. Regard these currents as measures with values in the Euclidean space \(\Lambda^k\R^N\). Flat convergence and the uniform mass bound give weak convergence of these vector measures. Because the currents are rectifiable, their polar vectors are simple, and their Euclidean total variations are exactly their masses. The convergence just proved therefore satisfies the hypotheses of Reshetnyak's continuity theorem \cite{Reshetnyak}; see \cite[Theorem 2.39]{AFP}. Apply it to the continuous function \(\Phi_g(x,\xi)=|\xi|_{g_x}\), the norm on exterior powers induced by the metric, restricted to Euclidean unit vectors \(\xi\). On a common compact neighborhood this function is bounded. We obtain \[ \mathbf M_g(A_j)\longrightarrow\mathbf M_g(T). \] Fix \(A=A_j\) with \(\mathbf M_g(A)<\mathbf M_g(T)+\eps/2\). It remains to make the vertices rational without changing the boundary chain. Represent \(P\) on a finite rational simplicial complex \(L\), and choose a common finite triangulation \(K\) of \(A\) and \(L\). The subdivision may introduce irrational vertices on \(L\), so simply fixing all boundary vertices would not suffice. For each vertex of \(K\) on \(|L|\), choose a nearby rational point in the smallest face of \(L\) containing it. Such points are dense in that face. Choose nearby rational points for the remaining vertices, and extend these choices affinely over each simplex of \(K\), obtaining a piecewise affine map \(f\). For every subdivided simplex of \(P\), both \(f\) and the straight homotopy \(H(s,x)=(1-s)x+sf(x)\) remain in the same face of \(L\), of dimension at most \(k-1\). Hence the swept-out \(k\)-current \(H_\#([0,1]\times P)\) is zero. Since \(\partial P=0\), the homotopy formula gives \[ f_\#P-P=\partial H_\#([0,1]\times P)=0. \] Consequently \(Q=f_\#A\) is rational polyhedral with integer coefficients and \(\partial Q=f_\#P=P\). Write \(A=\sum_\sigma a_\sigma\sigma\) on \(K\), after cancellation. The \(g\)-volume of each of these finitely many simplices is continuous in its vertices. Thus the choices can be made so close that \[ \mathbf M_g(Q)\le \sum_\sigma |a_\sigma|\,\mathbf M_g(f_\#\sigma) <\mathbf M_g(A)+\eps/2. \] Possible overlaps in the images only decrease mass after cancellation. This proves the lemma. \end{proof} Apply the lemma to the minimizing filling \(T\), choosing \(\eps>0\) so small that \[ 36\pi\bigl((\mathbf M_g(T)+\eps)^2-\mathbf M_g(T)^2\bigr)<1/r. \] For polyhedral chains the metric mass is exactly the weighted volume in \eqref{eq:weightedvolume}. Schulze's inequality and \(\partial Q=P\) now give Statement \ref{lp:almgren}. Schulze invokes Almgren's singular-set bound for minimizing \emph{three}-currents in the uniqueness argument of \cite[\S5, Lemma 5.2]{Schulze}. Here Almgren gives Hausdorff dimension at most \(3-2=1\) for the interior singular set. This codimension two is measured within the three-dimensional current; the ambient codimension of the filling is \(N-3\). Varying \(N\) thus includes three-dimensional fillings in arbitrary codimension, but does not test Almgren's theorem in every intrinsic dimension. Small regular patches are removed from a minimizing filling. The codimension-two singular-set estimate and unique continuation are used to obtain uniqueness for the remaining problem, which enters the proof of the isoperimetric inequality. This is a specific use of the regularity theorem, rather than an appeal to an unspecified result of Almgren. There are reasons for caution about the choice of linchpin. The metric has translations and rotations in the \(y\)-variables, and projection onto \(t=0\) contracts lengths. When \(N\ge4\), its sharp constant is already witnessed by Euclidean round three-balls in that slice. These facts leave room for a special proof that avoids the regularity theorem. Moreover, another uniqueness argument might replace its use in Schulze's proof. Projection alone does not prove the result: it changes the prescribed boundary. For example, when \(N\ge4\), the cylinder needed to restore a small two-sphere at height \(t_0\ne0\) has volume of order its radius squared, whereas the desired filling estimate has order its radius cubed. Thus the most immediate shortcut fails. Nevertheless, no converse has been established, and no claim of indispensability is justified. This example records a valid consequence and an unresolved question about its value as an audit. The same argument gives a broader version: allow any symmetric rational-polynomial \(N\times N\) matrix field \(G\) with \(G(x)\succeq I\) and nonpositive sectional curvature, and use \eqref{eq:weightedvolume} with this \(G\). The lower bound on the metric ensures completeness. This removes the symmetry of the particular example, but it still gives no reverse implication to Almgren regularity and no assertion that this polynomial class represents every relevant geometry. If desired, the integrals can be removed from the formal statement. Their integrands are square roots of nonnegative rational polynomials on rational simplices. Subdivision and explicit continuity estimates give rational upper and lower bounds to arbitrary accuracy; the same is true of \(\pi\). A strict inequality therefore has a finite rational certificate. The resulting assertion has the form \(\forall P,r\ \exists Q,s\), where \(s\) certifies the numerical inequality and all checks are finite. \section{Poincar\'e in dimension three}\label{sec:poincare} Here the polynomial models cover every closed smooth three-manifold. This representation theorem prevents the loss of generality that is a concern in the preceding example. \begin{linchpin}[Two critical points on a polynomial three-manifold] \label{lp:poincare} Let \(p_1,\ldots,p_s\in\Z[x_1,\ldots,x_7]\), and set \[ X=\{x\in\R^7:p_1(x)=\cdots=p_s(x)=0\}. \] Suppose that: \begin{enumerate} \item \(X\) is nonempty, bounded, and connected; \item at each point of \(X\), four of the \(p_i\) have independent gradients, and their common zero set agrees locally with \(X\); \item every continuous map \(S^1\to X\) extends to a continuous map of the closed disk into \(X\). \end{enumerate} Then there is \(h\in\Z[x_1,\ldots,x_7]\) such that \(h|_X\) has exactly two critical points, both nondegenerate. \end{linchpin} \status{A theorem equivalent to the three-dimensional Poincar\'e conjecture, using smooth structures in dimension three, the rational Nash--Tognoli theorem, and elementary Morse theory. Perelman's work proves the source theorem \cite{Perelman1,Perelman2,Perelman3}; see also \cite{MorganTian}.} The first two assumptions say that \(X\) is a compact connected smooth three-manifold without boundary. The third says it is simply connected. A critical point is taken along \(X\); the ambient gradient of \(h\) need not vanish. Assume Poincar\'e. Uniqueness of smooth structures in dimension three \cite{Moise} gives a diffeomorphism \(X\to S^3\). Pull back the ordinary height function on \(S^3\). It has two nondegenerate critical points. Extend this smooth function to an ambient neighborhood and approximate it in the \(C^2\) norm on a compact neighborhood by a polynomial. Such approximation follows, for example, by polynomial approximation with derivatives on a box after taking a smooth extension. Rational coefficients can be used by a further sufficiently small perturbation. A sufficiently small \(C^2\) perturbation preserves the two Morse critical points and creates no others. Near each critical point, nondegeneracy gives stability; on the complement of small neighborhoods the tangential gradient has a positive lower bound. Multiplying the rational polynomial by a positive common denominator gives the required integer polynomial. Conversely, a compact connected manifold with a Morse function having exactly two critical points is homeomorphic to a sphere \cite[Theorem 4.1]{Milnor}. In dimension three, neighborhoods of the minimum and maximum are balls, and the region between them is \(S^2\times[0,1]\). Gluing the two balls along their boundary gives \(S^3\), since a homeomorphism of \(S^2\) extends over the ball. To apply this to an arbitrary closed smooth three-manifold, use the rational Nash--Tognoli theorem of Ghiloni--Savi \cite[Theorem 1.7]{GhiloniSavi}. Every compact smooth \(d\)-manifold has a nonsingular algebraic model in \(\R^{2d+1}\), with both its global equations and its local nonsingularity defined over \(\Q\). For \(d=3\) this is \(\R^7\). A finite generating family for the rational vanishing ideal provides the required equations; locally, four of its gradients are independent. Clear denominators. The linchpin now proves Poincar\'e for smooth three-manifolds, and existence of smooth structures in dimension three \cite{Moise} gives the topological statement. The conclusion also has a direct algebraic description. Let \(J(x)\) have rows \(\nabla p_i(x)^{\mathsf T}\). On \(X\), \(\rank J(x)=4\) and \(T_xX=\ker J(x)\). A point is critical precisely when \[ \rank\begin{pmatrix}J(x)\\ \nabla h(x)^{\mathsf T}\end{pmatrix}=4. \] Choose four local defining equations \(q_1,\ldots,q_4\) with independent gradients, and at a critical point write \(\nabla h=\sum_i\lambda_i\nabla q_i\). Nondegeneracy means that the quadratic form \[ D^2h-\sum_{i=1}^4\lambda_iD^2q_i \] is nonsingular on \(\ker J(x)\). Thus the assertion about a proposed \(h\) is expressible by real polynomial equations and inequalities. The hypothesis about loops is retained in its usual topological form. There is no imposed bound on the degree of \(h\). \section{The Weil conjectures}\label{sec:weil} We distinguish two linchpins. The first retains the Riemann-hypothesis part of the Weil conjectures, using a substantial reduction theorem. The second is the familiar Ramanujan inequality, whose statement is particularly short. \subsection{Counting zeros of a homogeneous polynomial} Let \(K\) be a finite field with \(q\) elements, and let \(F\in K[x_1,\ldots,x_m]\) be nonzero and homogeneous of degree \(d\ge1\), where \(m\ge3\). Impose the following smoothness condition: in every finite extension \(K'/K\), \begin{equation}\label{eq:smoothhyp} F(x)=\frac{\partial F}{\partial x_1}(x)=\cdots =\frac{\partial F}{\partial x_m}(x)=0 \quad\Longrightarrow\quad x=0. \end{equation} Including \(F(x)=0\) is necessary when the characteristic divides \(d\). This condition says exactly that the projective hypersurface is smooth. Put \(A(F,K)=\#\{x\in K^m:F(x)=0\}\). \begin{linchpin}[A hypersurface counting inequality]\label{lp:weil} For every \(K,m,d,F\) as above satisfying \eqref{eq:smoothhyp}, \begin{equation}\label{eq:weilcount} \bigl(A(F,K)-q^{m-1}\bigr)^2 \le(d-1)^{2m-2}q^m. \end{equation} \end{linchpin} \status{A theorem. It is equivalent to the Riemann-hypothesis part of the Weil conjectures for all smooth proper varieties over finite fields, using the cohomological background and Scholl's reduction \cite{Scholl}. It is not presented as a reformulation of every part of the Weil conjectures at once.} Here is the connection. Let \(X\subset\PP^{m-1}_K\) be the hypersurface \(F=0\), of dimension \(n=m-2\). Then \[ A(F,K)=1+(q-1)\#X(K),\qquad q^{m-1}=1+(q-1)(1+q+\cdots+q^n). \] The trace formula and weak Lefschetz theorem express the difference \(\#X(K)-(1+\cdots+q^n)\) as the signed trace on the primitive middle cohomology. Its dimension is \[ B_{m,d}=\frac{(d-1)^m+(-1)^m(d-1)}d \le(d-1)^{m-1}; \] see \cite[\S4]{GhorpadeLachaud}. Deligne's theorem \cite{Deligne} bounds each eigenvalue in this cohomology by \(q^{n/2}\) in absolute value. It follows that \[ |A(F,K)-q^{m-1}| \le(q-1)B_{m,d}q^{(m-2)/2} \le(d-1)^{m-1}q^{m/2}, \] which proves \eqref{eq:weilcount}. For the converse, fix \(F\) and apply \eqref{eq:weilcount} over every extension of degree \(r\). Dividing by \(q^r-1\) gives \[ \left|\#X(\F_{q^r})-\sum_{j=0}^n q^{rj}\right| \le 2(d-1)^{m-1}q^{rn/2}. \] If \(\alpha_1,\ldots,\alpha_B\) are the primitive middle eigenvalues, the trace formula identifies the left side with \(\left|\sum_i\alpha_i^r\right|\). We use the elementary power-sum observation that \[ \left|\sum_{i=1}^B\alpha_i^r\right|=O(R^r)\ (r\ge1) \quad\Longrightarrow\quad |\alpha_i|\le R\ \text{for every }i. \] Indeed, the generating function of these sums is \(\sum_i\alpha_i z/(1-\alpha_i z)\). A nonzero eigenvalue of modulus greater than \(R\) would give a pole inside its disk of convergence. Equal eigenvalues add their positive multiplicities, so their poles cannot cancel. Apply this observation to every complex realization of the eigenvalues. Poincar\'e duality pairs \(\alpha\) with \(q^n/\alpha\), giving \(|\alpha|=q^{n/2}\). The remaining cohomology of a smooth hypersurface is the known ambient cohomology. Thus the counting inequality recovers the Riemann hypothesis for smooth hypersurfaces. Scholl's theorem states that the Riemann hypothesis in dimension \(d-1\), together with that for smooth hypersurfaces of dimension \(d\), implies it for all smooth proper varieties of dimension \(d\) \cite[Theorem 3.3]{Scholl}. Induction, starting in dimension zero, completes the converse. Scholl's reduction uses de Jong's alterations \cite{deJong,deJongFamilies}, the Rapoport--Zink vanishing-cycles spectral sequence \cite{RapoportZink}, and Deligne's local monodromy theorem for punctually pure sheaves on curves \cite[Theorem 1.8.4]{DeligneII}; the last is recalled as Theorem~1.9 of \cite{Scholl}. These are established dependencies of the reduction, not further conjectures. In particular, the local monodromy theorem used here has a proof independent of the general Riemann hypothesis being recovered \cite[Introduction]{Scholl}. The reduction is substantial, and its explicit inclusion is essential to the claimed strength of the linchpin. Finite fields can be described by finite addition and multiplication tables. Thus both the hypothesis over extensions and the conclusion can be stated using finite algebraic data, although the hypothesis quantifies over all finite extensions. The coarse constant in \eqref{eq:weilcount} was chosen to simplify the statement. A sharp Betti-number constant is unnecessary for the reverse implication. \subsection{Ramanujan's coefficients} Define integers \(\tau(n)\) by the formal power series \[ t\prod_{j=1}^\infty(1-t^j)^{24} =\sum_{n=1}^\infty\tau(n)t^n. \] Each coefficient requires only finitely many factors. \begin{linchpin}[Ramanujan's inequality]\label{lp:tau} For every prime \(p\), \[ \tau(p)^2\le4p^{11}. \] \end{linchpin} \status{A theorem downstream from Deligne's Riemann hypothesis over finite fields \cite[Theorem 8.2]{Deligne}. No converse is claimed.} The roots of \(T^2-\tau(p)T+p^{11}\) are realized in the appropriate degree of the cohomology of a Kuga--Sato variety. Deligne's theorem gives absolute value \(p^{11/2}\) for each root, and their sum is \(\tau(p)\). The square in the displayed inequality removes the only real power from the usual statement. This is an example where a classical formulation already provides nearly all the desired simplification. \section{Birch and Swinnerton-Dyer}\label{sec:bsd} The original experiments of Birch and Swinnerton-Dyer concerned products of point counts. Their asymptotic conjecture preceded the modern formulation by the order of vanishing of an \(L\)-function \cite{BSD1,BSD2,Birch}. That asymptotic gives a natural linchpin, provided its extra strength is stated explicitly. \subsection{Comparing finite-field and rational point counts} Fix \(A,B\in\Z\) with \(\Delta=-16(4A^3+27B^2)\ne0\). For primes \(p\nmid\Delta\), put \[ N_p=1+\#\{(x,y)\in\{0,\ldots,p-1\}^2: y^2\equiv x^3+Ax+B\pmod p\}. \] For \(x=u/v\in\Q\) in lowest terms, \(v>0\), define \(H(x)=\max(|u|,v)\), and for \(X\ge1\) set \[ M_{A,B}(X)=1+ \#\{(x,y)\in\Q^2:y^2=x^3+Ax+B,\ H(x)\le X\}. \] The added \(1\) counts the point at infinity. \begin{linchpin}[A point-count product]\label{lp:bsdproduct} For every such pair \(A,B\), there is a real constant \(C_{A,B}>0\) such that \begin{equation}\label{eq:bsdproduct} \prod_{\substack{p\le X\\p\nmid\Delta}}\frac{N_p}{p} \sim C_{A,B}\,M_{A,B}(X)^2 \qquad(X\to\infty). \end{equation} \end{linchpin} \status{Open. This is a stronger conjectural formulation implying the rank part of BSD for every elliptic curve over \(\Q\), and also the Riemann hypothesis for each of its \(L\)-functions. It is not known to follow from the modern rank conjecture alone.} For the elliptic curve \(E:y^2=x^3+Ax+B\), let \(r=\rank E(\Q)\). Mordell--Weil and the canonical height give, unconditionally, \begin{equation}\label{eq:heightcount} M_{A,B}(X)\sim c_{A,B}(\log X)^{r/2}, \qquad c_{A,B}>0. \end{equation} Indeed, modulo torsion the rational points form a lattice of rank \(r\), and the canonical height is a positive definite quadratic form. The difference between \(\log H(x)\) and twice the canonical height is bounded. Counting lattice points in expanding ellipsoids proves \eqref{eq:heightcount}; see \cite[Chapter VIII]{Silverman}. When \(r=0\), the count is eventually the size of the torsion group, so the same assertion holds with exponent zero. Consequently \eqref{eq:bsdproduct} is equivalent to the historical product asymptotic \[ \prod_{\substack{p\le X\\p\nmid\Delta}}\frac{N_p}{p} \sim C'_{A,B}(\log X)^r,\qquad C'_{A,B}>0. \] Omitting finitely many local factors changes only the constant. Goldfeld proved that such an asymptotic forces the exponent to be \(\ord_{s=1}L(E,s)\), and forces \(L(E,s)\ne0\) for \(\Re s>1\) \cite{Goldfeld}. Modularity of elliptic curves supplies the analytic continuation needed here \cite{BCDT}. Conrad gives the precise implication and analyzes the stronger convergence requirement \cite[Theorems 1.1 and 1.3]{Conrad}. The functional equation then gives the elliptic-curve Riemann hypothesis. Combining the equality of exponents with \eqref{eq:heightcount} gives the rank conjecture. The constant in \eqref{eq:bsdproduct} is unspecified. Thus this statement does not by itself express the refined BSD formula involving the regulator, periods, local factors, and the Tate--Shafarevich group. It is stronger in its analytic convergence assertion, while its stated arithmetic conclusion is the rank equality. These are separate comparisons of strength. \subsection{Rational right triangles} For positive integers \(c,d,m\), let \[ R_{c,d}(m)=\#\{(x,y,z)\in\Z^3:x^2+cy^2+dz^2=m\}. \] All signs and zero coordinates are included. \begin{linchpin}[A counting test for rational triangles]\label{lp:tunnell} Let \(n\) be a positive squarefree integer. There are \(u,v,w\in\Q_{>0}\) such that \[ u^2+v^2=w^2,\qquad uv=2n \] if and only if \[ \begin{cases} R_{2,8}(n)=2R_{2,32}(n),&n\text{ odd},\\ R_{4,8}(n/2)=2R_{4,32}(n/2),&n\text{ even}. \end{cases} \] \end{linchpin} \status{The implication from a triangle to the count equality is unconditional. The converse follows from the rank conjecture for the curves \(E_n:y^2=x^3-n^2x\), by Tunnell's theorem \cite{Tunnell}. The full biconditional remains a conditional downstream statement, not a theorem proved here.} A rational triangle of area \(n\) exists exactly when \(E_n(\Q)\) has positive rank. The elementary correspondence sends a rational point with \(y\ne0\) to side lengths \[ \left|\frac{x^2-n^2}{y}\right|,\qquad \left|\frac{2nx}{y}\right|,\qquad \left|\frac{x^2+n^2}{y}\right|. \] Conversely, from a triangle one obtains \(x=n(u+w)/v\), \(y=2n^2(u+w)/v^2\). The usual torsion calculation for \(E_n\) completes the positive-rank equivalence. Tunnell identifies the vanishing of the relevant difference of representation counts with \(L(E_n,1)=0\), using modular forms of weight \(3/2\) and the central-value formula of Waldspurger \cite{Tunnell,WaldspurgerHalf}. For the unconditional direction one also needs the theorem of Coates--Wiles for elliptic curves with complex multiplication \cite{CoatesWiles}: if \(L(E_n,1)\ne0\), then \(E_n(\Q)\) is finite. Each \(E_n\) has complex multiplication by \(\Z[i]\). Thus a triangle gives positive rank, hence \(L(E_n,1)=0\), and then the count equality. This dependency is explicit in \cite[p.~325]{Tunnell}. In the other direction, the count equality gives \(L(E_n,1)=0\); rank BSD then gives positive rank and a triangle. More precisely, together with these established results, Statement \ref{lp:tunnell} is equivalent to the assertion \[ \rank E_n(\Q)>0\quad\Longleftrightarrow\quad L(E_n,1)=0 \] for this family. It distinguishes rank zero from positive rank; it does not identify an arbitrary positive rank with the order of vanishing. \section{\texorpdfstring{\(\mathsf P\ne\mathsf{NP}\)}{P is not NP} by polynomial local updates} \label{sec:pnp} We use one-dimensional cellular automata because they are computationally universal, with polynomial time overhead for simulation by and of Turing machines \cite{Smith,NearyWoods}. This preserves the distinction between polynomial and nonpolynomial time required here. ``One-dimensional'' refers to the line of cells; the local update need not be a linear function. Allowing the finite local rule to vary makes the input convention simple. The reduction below gives the polynomial simulations explicitly. Fix a prime \(p\ge7\) and a polynomial \(F\in\F_p[X,Y,Z]\) with \(F(0,0,0)=0\). For a sequence \(z_i(t)\in\F_p\), indexed by \(i\in\Z\), define \begin{equation}\label{eq:ca} z_i(t+1)=F(z_{i-1}(t),z_i(t),z_{i+1}(t)). \end{equation} This is a cellular automaton on a line, with a common rule at every position and time. Let \(G\) be a simple graph on \([n]\), \(n\ge1\), with adjacency matrix \((e_{uv})\). Start the recurrence with \[ \begin{aligned} z_0(0)&=3,\\ z_{(u-1)n+v}(0)&=1+e_{uv}\quad(1\le u,v\le n),\\ z_{n^2+1}(0)&=4, \end{aligned} \qquad z_i(0)=0\quad\text{at every other position}. \] The symbols \(3,4\) mark the input, \(1,2\) encode its bits, and \(0\) is the blank symbol. A graph is \(3\)-colorable if there is \(\chi:[n]\to\{1,2,3\}\) with \(\chi(u)\ne\chi(v)\) whenever \(e_{uv}=1\). \begin{linchpin}[No uniformly fast local coloring rule]\label{lp:pnp} There do not exist a prime \(p\ge7\), a polynomial \(F\in\F_p[X,Y,Z]\) with \(F(0,0,0)=0\), and positive integers \(c,k\), such that for every \(n\ge1\) and every simple graph \(G\) on \([n]\), the recurrence above satisfies \[ z_0(cn^k)= \begin{cases} 5,&G\text{ is }3\text{-colorable},\\ 6,&G\text{ is not }3\text{-colorable}. \end{cases} \] \end{linchpin} \status{Open; equivalent to \(\mathsf P\ne\mathsf{NP}\). The connection uses established polynomial simulation and the NP-completeness of graph \(3\)-colorability \cite{Cook,GJS,Smith}. No additional conjecture is required.} Suppose the statement is false. The fixed rule uses a fixed finite field, so one update takes constant time in a conventional model of computation. At time \(T\), only an interval of \(O(n^2+T)\) cells can have been affected, because a change travels at most one position per update and an all-zero neighborhood stays zero. Simulating \(T=cn^k\) steps takes \(O(T(n^2+T))\) time. The rule therefore decides \(3\)-colorability in polynomial time, and NP-completeness gives \(\mathsf P=\mathsf{NP}\). Conversely, assume \(\mathsf P=\mathsf{NP}\). Take a deterministic polynomial-time procedure for graph \(3\)-colorability. It can be implemented on a one-tape Turing machine with a left end and polynomial overhead. Encode each tape square by its symbol, together with a state marker if the head is present. The initial symbol \(3\) encodes both the left-end marker and the head in its initial state at position \(0\). The machine preserves the left-end marker; after the head leaves, that square retains a distinct unheaded marker state. Assign distinct labels at least \(7\) to all additional encoded states. The next state of a square depends only on it and its two neighbors: the head moves by at most one square. This is a nearest-neighbor cellular automaton with a fixed finite alphabet. After the decision, return the head to the marked initial square and write \(5\) or \(6\). Make these output states absorbing, as specified below, so that the answer persists until the prescribed time. These operations still take polynomial time. The prescribed input is a delimited adjacency matrix, whose length is \(n^2+2\), so suitable \(c,k\) work for every \(n\). Choose a prime \(p\) large enough to encode all states, reserving \(0,\ldots,6\) for the specified symbols. Extend the local rule \(f\) to unused states, requiring \[ f(a,5,b)=5,\qquad f(a,6,b)=6 \quad\text{for all }a,b\in\F_p. \] Apart from these requirements and the blank transition below, the extension is arbitrary. Every function \(f:\F_p^3\to\F_p\) is polynomial: \[ F(X,Y,Z)=\sum_{a,b,d\in\F_p} f(a,b,d) \delta_a(X)\delta_b(Y)\delta_d(Z),\qquad \delta_a(X)=1-(X-a)^{p-1}. \] Choose the blank transition to be \(f(0,0,0)=0\). This gives a polynomial satisfying all the requirements that Statement \ref{lp:pnp} denies. The uniformity lies in the order of the quantifiers: \(p,F,c,k\) are chosen once for all graphs. Nothing depends on a separate circuit chosen for each input size. The recurrence is a model of computation, but its entire definition is the single polynomial update \eqref{eq:ca}. Polynomial universality is also known for a fixed small rule such as Rule 110 \cite{NearyWoods}; using that rule would move additional complexity into the input encoding without simplifying the present statement. \section{Theorems that already have elementary statements} \label{sec:coloring} Two results obtained by large satisfiability computations need no substantial reformulation. Their statements make clear that the length of a proof and the complexity of its conclusion are different matters. \begin{linchpin}[Boolean Pythagorean triples]\label{lp:bpt} Every map \(\chi:[7825]\to\{0,1\}\) has positive integers \(a,b,c\le7825\) such that \[ a^2+b^2=c^2,\qquad \chi(a)=\chi(b)=\chi(c). \] There exists a map \(\chi:[7824]\to\{0,1\}\) with no such triple. \end{linchpin} \status{A theorem of Heule--Kullmann--Marek \cite{HKM}. This is the original finite threshold theorem, used as its own linchpin. It implies the corresponding assertion for every two-coloring of the positive integers.} A formulation only about the infinite set of positive integers would omit the exact threshold. The finite statement includes both the obstruction and its sharpness. \begin{linchpin}[The fifth Schur number]\label{lp:schur} There exists a map \(\chi:[160]\to\{1,2,3,4,5\}\) for which no \(x,y,z\in[160]\) satisfy \[ x+y=z,\qquad \chi(x)=\chi(y)=\chi(z). \] Every map \(\chi:[161]\to\{1,2,3,4,5\}\) has such a triple. \end{linchpin} \status{The theorem \(S(5)=160\), proved by Heule \cite{Heule}. It is already an elementary linchpin statement.} The variables \(x,y,z\) need not be pairwise distinct; in particular \(x=y\) is allowed. This convention is essential to the definition of the Schur number. The first assertion is a finite witness, and the second is a finite universal claim. The computations in \cite{HKM,Heule} produce checkable certificates. In a formal audit one must also connect the coloring statement to the encoded satisfiability problem and verify the certificate checker. A large certificate does not remove this semantic obligation. \section{Using the linchpins} The examples separate three questions. Is the statement easy to understand? What is its mathematical relation to the source theorem? Does the particular formal proof test the mathematics that the auditor intended to test? A good answer to the first question does not settle the other two. Equivalent formulations offer the strongest protection against an accidental loss of content. The Kepler and Poincar\'e examples illustrate two different mechanisms: a packing can be inserted into a periodic configuration, and an arbitrary three-manifold can be represented by integer equations. The hypersurface example requires a much deeper bridge. Its elementary counting statement retains the full Riemann hypothesis over finite fields only because Scholl's theorem is part of the connection. Downstream statements may be more convenient, but they require an explicit decision about how much of the source is being tested. The six-entry rearrangement statement does not reconstruct CFSG. Twelve-square counts test an application of the unitary fundamental lemma. The weighted filling statement has a published proof route through Almgren regularity, yet may permit a bypass. These qualifications are part of the specification of an audit. A formal development should expose the chosen statement, its definitions, its premises, and the bridge that invokes the source theorem. A human should be able to read that interface without reconstructing the entire development. If a successful proof leaves the intended source untouched, the appropriate response is to reconsider the linchpin. The objective remains the audit of mathematics, rather than the preservation of a particular list of statements. \medskip \noindent\textit{AI statement.} ChatGPT-6 Astra generated this document on October 16, 2026 at the prompting of Thomas Hales. \begin{thebibliography}{99} \bibitem{Almgren} F.~J. Almgren, Jr., \emph{Almgren's Big Regularity Paper: \(Q\)-Valued Functions Minimizing Dirichlet's Integral and the Regularity of Area-Minimizing Rectifiable Currents up to Codimension 2}, edited by V. Scheffer and J.~E. Taylor, World Scientific Monograph Series in Mathematics, vol.~1, World Scientific, 2000. \bibitem{AFP} L. Ambrosio, N. Fusco, and D. Pallara, \emph{Functions of Bounded Variation and Free Discontinuity Problems}, Oxford Mathematical Monographs, Oxford University Press, 2000. \doi{10.1093/oso/9780198502456.001.0001}. \bibitem{ABC} J. Ara\'ujo, W. Bentz, and P.~J. Cameron, The existential transversal property: a generalization of homogeneity and its impact on semigroups, \emph{Trans. Amer. Math. Soc.} \textbf{374} (2021), 1155--1195. \doi{10.1090/tran/8285}. \bibitem{BaezDuarte} L. B\'aez-Duarte, A strengthening of the Nyman--Beurling criterion for the Riemann hypothesis, \emph{Rend. Lincei Mat. Appl.} (9) \textbf{14} (2003), 5--11. \arxiv{math/0202141}. \bibitem{Bagchi} B. Bagchi, On Nyman, Beurling and Baez-Duarte's Hilbert space reformulation of the Riemann hypothesis, \emph{Proc. Indian Acad. Sci. Math. Sci.} \textbf{116} (2006), 137--146. \doi{10.1007/BF02829783}. \bibitem{BLGHT} T. Barnet-Lamb, D. Geraghty, M. Harris, and R. Taylor, A family of Calabi--Yau varieties and potential automorphy II, \emph{Publ. Res. Inst. Math. Sci.} \textbf{47} (2011), 29--98. \doi{10.2977/PRIMS/31}. \bibitem{Beurling} A. Beurling, A closure problem related to the Riemann zeta-function, \emph{Proc. Natl. Acad. Sci. USA} \textbf{41} (1955), 312--314. \doi{10.1073/pnas.41.5.312}. \bibitem{Birch} B.~J. Birch, Conjectures concerning elliptic curves, in \emph{Arithmetic Algebraic Geometry}, Proc. Sympos. Pure Math., vol.~8, American Mathematical Society, 1965, pp.~106--112. \bibitem{BSD1} B.~J. Birch and H.~P.~F. Swinnerton-Dyer, Notes on elliptic curves. I, \emph{J. Reine Angew. Math.} \textbf{212} (1963), 7--25. \doi{10.1515/crll.1963.212.7}. \bibitem{BSD2} B.~J. Birch and H.~P.~F. Swinnerton-Dyer, Notes on elliptic curves. II, \emph{J. Reine Angew. Math.} \textbf{218} (1965), 79--108. \doi{10.1515/crll.1965.218.79}. \bibitem{Borel} A. Borel, Some remarks about Lie groups transitive on spheres and tori, \emph{Bull. Amer. Math. Soc.} \textbf{55} (1949), 580--587. \doi{10.1090/S0002-9904-1949-09251-0}. \bibitem{Borisov} A. Borisov, Quotient singularities, integer ratios of factorials, and the Riemann hypothesis, \emph{Int. Math. Res. Not.} \textbf{2008}, article rnn052. \doi{10.1093/imrn/rnn052}. \bibitem{BCDT} C. Breuil, B. Conrad, F. Diamond, and R. Taylor, On the modularity of elliptic curves over \(\Q\): wild \(3\)-adic exercises, \emph{J. Amer. Math. Soc.} \textbf{14} (2001), 843--939. \bibitem{BridsonHaefliger} M.~R. Bridson and A. Haefliger, \emph{Metric Spaces of Non-Positive Curvature}, Grundlehren der mathematischen Wissenschaften, vol.~319, Springer, 1999. \doi{10.1007/978-3-662-12494-9}. \bibitem{Cameron} P.~J. Cameron, \emph{Permutation Groups}, London Mathematical Society Student Texts, vol.~45, Cambridge University Press, 1999. \bibitem{CFM} A. Chambolle, L.~A.~D. Ferrari, and B. Merlet, Strong approximation in \(h\)-mass of rectifiable currents under homological constraint, \emph{Adv. Calc. Var.} \textbf{14} (2021), 343--363. \doi{10.1515/acv-2018-0079}. \bibitem{CoatesWiles} J. Coates and A. Wiles, On the conjecture of Birch and Swinnerton-Dyer, \emph{Invent. Math.} \textbf{39} (1977), 223--251. \doi{10.1007/BF01402975}. \bibitem{Conrad} K. Conrad, Partial Euler products on the critical line, \emph{Canad. J. Math.} \textbf{57} (2005), 267--297. \doi{10.4153/CJM-2005-012-6}. \bibitem{Cook} S.~A. Cook, The complexity of theorem-proving procedures, in \emph{Proceedings of the Third Annual ACM Symposium on Theory of Computing}, ACM, 1971, pp.~151--158. \doi{10.1145/800157.805047}. \bibitem{Cox} D.~A. Cox, \emph{Primes of the Form \(x^2+ny^2\): Fermat, Class Field Theory, and Complex Multiplication}, second ed., Wiley, 2013. \bibitem{deJong} A.~J. de Jong, Smoothness, semi-stability and alterations, \emph{Publ. Math. Inst. Hautes \'Etudes Sci.} \textbf{83} (1996), 51--93. \doi{10.1007/BF02698644}. \bibitem{deJongFamilies} A.~J. de Jong, Families of curves and alterations, \emph{Ann. Inst. Fourier (Grenoble)} \textbf{47} (1997), 599--621. \doi{10.5802/aif.1575}. \bibitem{Deligne} P. Deligne, La conjecture de Weil. I, \emph{Publ. Math. Inst. Hautes \'Etudes Sci.} \textbf{43} (1974), 273--307. \href{https://www.numdam.org/item/PMIHES_1974__43__273_0/}{Numdam}. \bibitem{DeligneII} P. Deligne, La conjecture de Weil. II, \emph{Publ. Math. Inst. Hautes \'Etudes Sci.} \textbf{52} (1980), 137--252. \href{https://www.numdam.org/item/PMIHES_1980__52__137_0/}{Numdam}. \bibitem{Federer} H. Federer, \emph{Geometric Measure Theory}, Grundlehren der mathematischen Wissenschaften, vol.~153, Springer, 1969. \bibitem{FKS} B. Fein, W.~M. Kantor, and M. Schacher, Relative Brauer groups. II, \emph{J. Reine Angew. Math.} \textbf{328} (1981), 39--57. \doi{10.1515/crll.1981.328.39}. \bibitem{GJS} M.~R. Garey, D.~S. Johnson, and L. Stockmeyer, Some simplified NP-complete graph problems, \emph{Theoret. Comput. Sci.} \textbf{1} (1976), 237--267. \doi{10.1016/0304-3975(76)90059-1}. \bibitem{GhiloniSavi} R. Ghiloni and E. Savi, The Nash--Tognoli theorem over the rationals and its version for isolated singularities, preprint, 2023, revised 2025. \arxiv{2302.04142v4}. \bibitem{GhorpadeLachaud} S.~R. Ghorpade and G. Lachaud, \'Etale cohomology, Lefschetz theorems and number of points of singular varieties over finite fields, \emph{Mosc. Math. J.} \textbf{2} (2002), 589--631; corrected version, \arxiv{0808.2169}. \bibitem{Goldfeld} D. Goldfeld, Sur les produits partiels eul\'eriens attach\'es aux courbes elliptiques, \emph{C. R. Acad. Sci. Paris S\'er. I Math.} \textbf{294} (1982), 471--474. \bibitem{HalesNgo} T.~C. Hales, The work of Ng\^o Bao Ch\^au, \emph{Notices Amer. Math. Soc.} \textbf{58} (2011), 453--458. \arxiv{1012.0382}. \bibitem{Flyspeck} T. Hales, M. Adams, G. Bauer, T.~D. Dang, J. Harrison, L.~T. Hoang, C. Kaliszyk, V. Magron, S. McLaughlin, T.~T. Nguyen, Q.~T. Nguyen, T. Nipkow, S. Obua, J. Pleso, J. Rute, A. Solovyev, T.~H.~A. Ta, N.~T. Tran, T.~D. Trieu, J. Urban, K. Vu, and R. Zumkeller, A formal proof of the Kepler conjecture, \emph{Forum Math. Pi} \textbf{5} (2017), e2, 29 pp. \doi{10.1017/fmp.2017.1}. \bibitem{HSBT} M. Harris, N. Shepherd-Barron, and R. Taylor, A family of Calabi--Yau varieties and potential automorphy, \emph{Ann. of Math.} (2) \textbf{171} (2010), 779--813. \doi{10.4007/annals.2010.171.779}. \bibitem{Heule} M.~J.~H. Heule, Schur number five, in \emph{Proceedings of the AAAI Conference on Artificial Intelligence}, vol.~32, 2018, pp.~6598--6606. \doi{10.1609/aaai.v32i1.12209}. \bibitem{HKM} M.~J.~H. Heule, O. Kullmann, and V.~W. Marek, Solving and verifying the Boolean Pythagorean triples problem via cube-and-conquer, in \emph{Theory and Applications of Satisfiability Testing---SAT 2016}, Lecture Notes in Computer Science, vol.~9710, Springer, 2016, pp.~228--245. \doi{10.1007/978-3-319-40970-2_15}. \bibitem{Humphreys} J.~E. Humphreys, \emph{Introduction to Lie Algebras and Representation Theory}, Graduate Texts in Mathematics, vol.~9, Springer, 1972. \bibitem{Knapp} A.~W. Knapp, \emph{Lie Groups Beyond an Introduction}, second ed., Progress in Mathematics, vol.~140, Birkh\"auser, 2002. \bibitem{Lagarias} J.~C. Lagarias, An elementary problem equivalent to the Riemann hypothesis, \emph{Amer. Math. Monthly} \textbf{109} (2002), 534--543. \doi{10.1080/00029890.2002.11919883}. \bibitem{LaumonNgo} G. Laumon and B.-C. Ng\^o, Le lemme fondamental pour les groupes unitaires, \emph{Ann. of Math.} (2) \textbf{168} (2008), 477--573. \doi{10.4007/annals.2008.168.477}. \bibitem{Littlewood} J.~E. Littlewood, Quelques cons\'equences de l'hypoth\`ese que la fonction \(\zeta(s)\) de Riemann n'a pas de z\'eros dans le demi-plan \(\Re s>1/2\), \emph{C. R. Acad. Sci. Paris} \textbf{154} (1912), 263--266. \bibitem{Madlener} K. Madlener, S. Smetsers, and M. van Eekelen, A formal verification study on the Rotterdam storm surge barrier, in \emph{Formal Methods and Software Engineering---ICFEM 2010}, Lecture Notes in Computer Science, vol.~6447, Springer, 2010, pp.~287--302. \doi{10.1007/978-3-642-16901-4_20}. \bibitem{Milnor} J. Milnor, \emph{Morse Theory}, Annals of Mathematics Studies, vol.~51, Princeton University Press, 1963. \bibitem{MohammadSheikh} N.~I.~S. Mohammad and T. Sheikh, The faithfulness gap: certifying semantic equivalence between natural-language and formal mathematical statements, preprint, 2026. \arxiv{2606.16541}. \bibitem{Moise} E.~E. Moise, \emph{Geometric Topology in Dimensions 2 and 3}, Graduate Texts in Mathematics, vol.~47, Springer, 1977. \bibitem{MorganTian} J. Morgan and G. Tian, \emph{Ricci Flow and the Poincar\'e Conjecture}, Clay Mathematics Monographs, vol.~3, American Mathematical Society and Clay Mathematics Institute, 2007. \bibitem{NearyWoods} T. Neary and D. Woods, P-completeness of cellular automaton Rule 110, in \emph{Automata, Languages and Programming---ICALP 2006}, Lecture Notes in Computer Science, vol.~4051, Springer, 2006, pp.~132--143. \doi{10.1007/11786986_13}. \bibitem{Ngo} B.-C. Ng\^o, Le lemme fondamental pour les alg\`ebres de Lie, \emph{Publ. Math. Inst. Hautes \'Etudes Sci.} \textbf{111} (2010), 1--169. \doi{10.1007/s10240-010-0026-7}. \bibitem{Nyman} B. Nyman, \emph{On Some Groups and Semigroups of Translations}, doctoral thesis, Uppsala University, 1950. \bibitem{ONeill} B. O'Neill, \emph{Semi-Riemannian Geometry with Applications to Relativity}, Pure and Applied Mathematics, vol.~103, Academic Press, 1983. \bibitem{Perelman1} G. Perelman, The entropy formula for the Ricci flow and its geometric applications, preprint, 2002. \arxiv{math/0211159}. \bibitem{Perelman2} G. Perelman, Ricci flow with surgery on three-manifolds, preprint, 2003. \arxiv{math/0303109}. \bibitem{Perelman3} G. Perelman, Finite extinction time for the solutions to the Ricci flow on certain three-manifolds, preprint, 2003. \arxiv{math/0307245}. \bibitem{Pollack} R. Pollack, How to believe a machine-checked proof, in G. Sambin and J. Smith (eds.), \emph{Twenty Five Years of Constructive Type Theory}, Oxford University Press, 1998, pp.~205--220. Preprint: BRICS Report RS-97-18, 1997, \doi{10.7146/brics.v4i18.18945}. \bibitem{RapoportZink} M. Rapoport and T. Zink, \"Uber die lokale Zetafunktion von Shimuravariet\"aten. Monodromiefiltration und verschwindende Zyklen in ungleicher Charakteristik, \emph{Invent. Math.} \textbf{68} (1982), 21--101. \doi{10.1007/BF01394268}. \bibitem{Reshetnyak} Yu.~G. Reshetnyak, The weak convergence of completely additive vector-valued set functions, \emph{Siberian Math. J.} \textbf{9} (1968), 1039--1045. \doi{10.1007/BF02196453}. \bibitem{Robin} G. Robin, Grandes valeurs de la fonction somme des diviseurs et hypoth\`ese de Riemann, \emph{J. Math. Pures Appl.} (9) \textbf{63} (1984), 187--213. \bibitem{Rushby} J. Rushby, \emph{Formal Methods and their Role in the Certification of Critical Systems}, Technical Report SRI-CSL-95-1, Computer Science Laboratory, SRI International, 1995. Also issued as NASA Contractor Report 4673 under the title \emph{Formal Methods and Their Role in Digital Systems Validation for Airborne Systems}. \href{https://ntrs.nasa.gov/citations/19960008816}{NASA report}. \bibitem{Scholl} A.~J. Scholl, Hypersurfaces and the Weil conjectures, \emph{Int. Math. Res. Not.} \textbf{2011}, no.~5, 1010--1022. \doi{10.1093/imrn/rnq098}. \bibitem{Schulze} F. Schulze, Optimal isoperimetric inequalities for surfaces in any codimension in Cartan--Hadamard manifolds, \emph{Geom. Funct. Anal.} \textbf{30} (2020), 255--288. \doi{10.1007/s00039-020-00522-8}. \bibitem{Silverman} J.~H. Silverman, \emph{The Arithmetic of Elliptic Curves}, second ed., Graduate Texts in Mathematics, vol.~106, Springer, 2009. \bibitem{SilvermanAdvanced} J.~H. Silverman, \emph{Advanced Topics in the Arithmetic of Elliptic Curves}, Graduate Texts in Mathematics, vol.~151, Springer, 1994. \bibitem{Smith} A.~R. Smith III, Real-time language recognition by one-dimensional cellular automata, \emph{J. Comput. System Sci.} \textbf{6} (1972), 233--253. \doi{10.1016/S0022-0000(72)80004-7}. \bibitem{Soundararajan} K. Soundararajan, Partial sums of the M\"obius function, \emph{J. Reine Angew. Math.} \textbf{631} (2009), 141--152. \doi{10.1515/CRELLE.2009.044}. \bibitem{Topaz} A. Topaz, Definitions in the liquid tensor experiment, \emph{Lean community blog}, 14 October 2022. \href{https://leanprover-community.github.io/blog/posts/lte-examples/} {Online article}. \bibitem{Tunnell} J.~B. Tunnell, A classical Diophantine problem and modular forms of weight \(3/2\), \emph{Invent. Math.} \textbf{72} (1983), 323--334. \doi{10.1007/BF01389327}. \bibitem{WaldspurgerHalf} J.-L. Waldspurger, Sur les coefficients de Fourier des formes modulaires de poids demi-entier, \emph{J. Math. Pures Appl.} (9) \textbf{60} (1981), 375--484. \bibitem{WaldspurgerFL} J.-L. Waldspurger, Endoscopie et changement de caract\'eristique, \emph{J. Inst. Math. Jussieu} \textbf{5} (2006), 423--525. \bibitem{Autoformalization} Y. Wu, A.~Q. Jiang, W. Li, M.~N. Rabe, C. Staats, M. Jamnik, and C. Szegedy, Autoformalization with large language models, \emph{Advances in Neural Information Processing Systems} \textbf{35} (2022), 32353--32368. \arxiv{2205.12615}. \end{thebibliography} \end{document}