Autoformalization of mathematical theorems? No shit!

I've been formalizing mathematical theorems in Lean for some years now, and one of the major blocks is the difficulty of formalizing elementary results that mathematicians do not take the time to even state. For example, a mathematician's integer can implicitly be a natural number at a line and a real number at the next one, while proof assistants require that some “coercion” maps be introduced. Having three `1` in the same formula, of three different natures, leads to unexpected nightmares. It is therefore very important for the development of proof-assisted mathematics that some automation be provided by the type checking system, with as many obvious things being taken care of by a combination of a fine-tuned API and efficient search algorithms. 

Another reason for the difficulty of formalizing proofs is having to navigate in a gigantic mathematical library (Mathlib, for example, has 1.5 million line of codes) and the lack of a definitive search engine and of a reliable and complete documentation. This is not to blame my colleagues — all of this is difficult to write, time consuming, and our personal interests are driven in different directions. 

This may explain that part of the field of formalization is driven by the “AI hype”, and — although this hype is so finely rebuted by Emily Bender and Alex Hannah in their last book, The AI Con, which I recommend heartily — that several colleagues use LLMs to create proofs, either in natural language, or in Lean's syntax. They say it is successful, but from the outside, it is really hard to tell whether it is really the case. My main impression is that these softwares obliterate the time where our mind tries to form ideas, leading — for me — to another kind of stress. There are also serious arguments that the systematic cognitive friction is a necessity of well-formed thinking, and cannot be replaced by stochastic optimization. Moreover, these colleagues usually do not address the environmental cost of using such kinds of generative AI, and whether its output is worth that cost.

A few days ago, after I complained — one more time — that stochastic algorithms do not think, I was asked my opinion about the “trinity autoformalization system”. I have to confess I carefully avoid the AI news and hadn't heard about it. A first search led me to a 2022 paper Autoformalization with Large Language Models. Here is the definition of “autoformalization” from their paper:

Autoformalization refers to the task of automatically translating from natural language mathematics to a formal language.

In this case, the authors took as a benchmark statements of mathematical competition problems, and were happy to have their LLMs translate correctly roughly 25% of those problems. This might be a technical exploit, but le me stay unimpressed for the moment: what mathematicians need is more than that, and is not elementary statements of math olympiad problems, but the most advanced mathematical concepts that the human mind is capable to grasp despite the fact that they involve extremely intricate and sometimes combinatorically involved constructions. I am not sure that we fully know what it means to understand these concepts, but I am certain that it doesn't reduce to being able of formally stating a mathematical statement. (And what about those very fine colleagues who demonstrate everyday their mathematical depth while failing at stating precise statements?)

It appears my colleague from the Lean community meant another result. Trinity is a project from Morph Labs, which their web page describes as follows:

Morph Labs is building a cloud for superintelligence.
Infinibranch enables AI agents on Morph Cloud to snapshot, replicate, autoscale, test, debug, deploy, and reason about software at light speed.

This starts pretty badly. First of all, superintelligence is even less defined than intelligence is, and claims of developing superintelligence can only be suspicious, especially when no scientific claim justifies that AI softwares feature any intelligence at all, and most of the AI experiments show a poor rate of success. The next sentence may be worse, since the speed of reasoning is not measured in m/s (nor in ft/hr), and the speed of electric waves in cables is smaller than the speed of light (although, I just learnt, it can be up to 99% of it!).

Their blog page on Trinity starts as follows:

tl;dr
We're excited to announce Trinity, an autoformalization system that represents a critical step toward verified superintelligence.

which combines the colloquial tl;dr (too long, don't read) with the brutal claim that their autoformalization could be a step towards superintelligence. Later on the webpage, they boast about a nearly infinite supply of verified training environments which, in our finite world plagued by a brutal climate change, is quite a thing. 

What these people claim to have done is the autoformalization of a 1962 theorem by N. G. de Bruijn (who, incidentally, is the father of Automath, one of the first proof assistants to be built), regarding the behaviour of the number $N(n)$ of integers $\leq n$ all of whose prime factors divide $n$, when $n$ grows to infinity. Answering a question of Erdös, de Bruijn proved that, on average, $N(n)$ is at most $n^{1+\varepsilon}$. On the other hand, the Trinity team puts the accent on a consequence of that result to the abc conjecture of Masser and Oesterlé. That conjecture asserts that for any $\varepsilon\gt0$, there exists a real number $k\gt0$ such that there are only finitely many triples $(a,b,c)$ of coprime natural numbers such that $a+b =c $ and such that the product $\operatorname{rad}(abc)$ of all prime numbers dividing $abc$ is at most $c^{1-\varepsilon}$. Implications of that mysterious elementary looking conjecture to number theoretical questions are manifold, from an asymptotic version of Fermat's Last Theorem to an effective version of the Mordell conjecture to Siegel zeroes of L-functions, etc. In effect, the theorem of de Bruijn implies that there are at most $\mathrm O(N^{2/3})$ triples $(a,b,c)$ of coprime natural numbers at most $N$ such that $\operatorname{rad}(abc)\lt c^{1-\varepsilon}$. When this bound is compared to the $\approx \frac6{\pi^2}N^2$ triples of coprime integers $(a,b,c)$ such that $a+b=c\leq N$, this indicates that the (hoped to be finite) set of the abc conjecture is kind of sparse.

To be fair, I am not capable of judging the difficulty of what they achieved, and I presume this is a difficult piece of software engineering to adjust the myriad of parameters of the implied neural networks. But what I can tell is whether they did what they say they did, and whether (this is more of an opinion) this has any relevance for the future of mathematical formalization. The answers, you can guess, will be no, definitely no. 

I would first like to make a mathematical comment on the sentence

We obtain the first formalized theorem towards the abc conjecture, showing it is true almost always. 

that can be read on the github page for the project which compares to the title of the (nice) exposition paper by Jared Lichtman: “The abc conjecture is true almost always”, but adds the idea that this theorem would be a step towards the abc conjecture. I claim that it is nothing like that. Indeed, it is an observation of Oesterlé (see Szpiro's paper, page 12) that the $\varepsilon=0$-variant of the abc conjecture is false. On the other hand, the exact same argument shows that the counterexamples to this false conjecture are as sparse, maybe with an upper bound $N^{2/3+\varepsilon}$ for the number of counterexamples. Consequently, if de Bruijn's result were a step towards the abc conjecture, it would simultaneously be a step towards a false conjecture. The most reasonable conclusion is then to admit that this theorem has no proof-theoretic relevance to the abc conjecture.

Then, while Morph's blog says: 

Trinity systematically processes entire papers, intelligently corrects its own formalization errors by analyzing failed attempts, and automatically refactors lengthy proofs to extract useful lemmas and abstractions,

the github page for the actual project mentions a human-supplied blueprint. This is a file in (La)TeX format that serves as a convenient host for the Lean project, providing information to the Lean prover. From the expression “human-supplied”, one has to understand that human beings have written that file, that is to say, have split the proof of de Bruijn's theorem in a series of 67 lemmas which divide the initial paper into tiny results, while giving references to other lemmas as indications of how they could be proved. As an example, here is “lemma24”:

\begin{lemma} \label{lem24} \lean{lemma24}
Let $p_1<\cdots<p_k$ be distinct primes, and denote the product $r = p_1 \cdots p_k$. If an integer $n\ge1$ satisfies $\rad(n)=r$, then $n = p_1^{a_1}\cdots p_k^{a_k}$ for some integers $a_1,\dots,a_k\ge 1$.
\end{lemma}
\begin{proof}\leanok
\uses{thm3, lem20}
Uses theorem \ref{thm3} with $n$, then uses lemma \ref{lem20}.
\end{proof}

which means that if an integer $r$ is the product of distinct primes $p_1,\dots,p_k$ and $\operatorname{rad}(n)=r$, then $n$ can be written $p_1^{a_1}\cdots p_k^{a_k}$, for some integers $a_1,\dots,a_k\geq 1$. The indication is to use “thm3” (the fundamental theorem of arithmetic) and “lem20” (the formula for the radical of an integer in terms of its decomposition into prime factors). 

To summary, humans have converted the 2-page proof of this result into 67 tiny chunks, supplying plenty of information that would have probably been unnecessary to most professional mathematicians, and fed that to their LLM. I am reluctant to draw a comparison with the AI farms in Kenya where workers were (and probably still are) exploited at tagging violent images for a ridiculous pay, but this is yet another instance where “mechanized artificial intelligence” relies crucially on human's work (beyond the invention and deployment of neural networks, etc., which are human's work as well, of course). And as in these other cases, the technostructure makes every effort to make this human work invisible: the blueprint has no author, the blog post has no author. Everything is made so that you believe that no human was implied in this project. 

Let's go back to the content of the blueprint, taking for granted that such a work has to be done anyway. However, we, humans, do not want to have to write endlessly tiny lemmas, each of them apparently irrelevant to the big mathematical picture. We do not want to keep them in a mathematical library, for almost all of them have no interest outside of their specific contect. Moreover, once these lemmas are written, there would be no additional effort for a human to formalize the proof. What we do want is a way to translate with as little effort as possible mathematical ideas, keeping mostly close their natural expression.

Moreover, even if we would have had to provide these tiny lemmas, we wouldn't be able to keep them in a human-accessible mathematical library, for that library would be cluttered by millions of uninteresting rapidly redundant lemmas. Building a mathematical library is a human task, that reflects the activity of past human minds, to be used by future human minds. 

As a matter of fact, this project considers a result in elementary mathematics, at an undergraduate level,  and can completely ignore the difficulty of building a large scale mathematical library, while this is precisely there that we need better automation. Something which is missing in Lean (but exists in other proof assistant systems, such as Rocq) is a coherent management system of all algebraic/analytic structures, which would allow to optimize their construction without having to modify the rest of the code. There are some cases of such an automation in Lean though, for example the automatic conversion of mathematical lemmas for groups written in multiplicative form to groups written in additive forms, giving one proof for two. Building such a tool requires a good proficiency in parsers and a clear view of what mathematicians do “in their heads” when they perform that apparently innocuous conversion. (For this reason, another automatic conversion for changing the direction of ordering relations appears more difficult to write, because what we would want is less clear. For the moment, mathlib has resolved itself to systematically privilege the $\leq$ inequality; the other one can be made to the dual order, but automating this prompts out the very same problem.) Another kind of crucial automation is the implementation of solvers for linear inequalities, or automatic proofs of algebraic identifies (in numbers, in groups, whatrever) so that the sentence “a computation shows that…” could almost be translated as such in formal code. This requires a good knowledge in programming, and the use of subtle but classical algorithms (simplex method, Gröbner bases, SAT solvers…), each of them finely tailored for its applications. This is a truly beautiful combination of mathematics and computer science, but nothing close of a so-called “general intelligence” tool.

There is something positive, though, that I could say about the search for automatic formalization. The AI companies do not acknowledge it, most of the public opinion is delusionnal, but LLMs have no reasoning faculty at all, and they just can't. What they do is put words together that would fit together with a good probability given the existing corpus that the machine has been given. Patterns exist in language, they exist in mathematics as well, and the (impressing, I concede) faculty of these softwares allows them to simulate text, be it litterary or mathematical, that looks plausible. But that doesn't make it true. On the other hand, these softwares could be combined with proofs assistants that work in a formal, proof-amenable, language, hereby offering a way of assessing the veracity of the output of the vernacular text. (On the other hand, one would need to be sure that the text couldn't say $1+1=3$ when the Lean code has certified that $1+1=2$.)

As a final paragraph, I would like to comment on the metaphors invoked by Morph Labs. Everyone who is even loosely knowledgeable in Sci-Fi movies will have recognized the Wachowskis's movie The Matrix. In that dystopic movie, humans are trapped in a machine-made “reality” after they lost a war against the artificial intelligences they created. Of course, Morpheus and Trinity are humans who fight against this power, but I wonder what the creators of Morph Labs had in mind when they decided to call themselves under this name, and to go on with the metaphor by using the name Trinity. (And who's Neo?) Their obvious reference is a world where artificial intelligence led to humanity's doom, while their rhetoric is one of AI hype. We rejoin here the discussion of Bender and Hannah in their abovementioned book, where they explain that AI doomerism/boosterism are the two faces of the same coin, that takes every development of genAI as unavoidable, whatever its social, ethical, and ecological costs.

Number theory and finite automata

$\gdef\abs#1{\lvert#1\rvert}$

There are many parts of number theory I don't know of, and today's story is about one I learnt very recently, at the intersection of number theory and computer science. It is about the natural numbers that we can recognize using a finite automaton. 

Finite automata and automatic functions

Finite automata

Finite automata are very elementary computers. These machines can receive instructions of finitely many sorts, and can be in finitely many states; moreover, their behaviour is prescribed: when, in a given state, they receive one instruction, they just move to another state. Mathematically, one can say that there is a finite set $A$ of instructions, a finite set $S$ of states, and a mapping $\phi\colon A \times S\to S$. One state $\varepsilon$ is labeled as the initial state; wen reading a list of instructions $[a_1,\dots,a_m]$, the machine goes through the states $s_0=\varepsilon$, $s_1=\mu(a_1,s_0)$, $s_2=\mu(a_2,s_1)$, etc. until it reaches and outputs its the final state $s_n$. All in all, the automaton defines a function $\Phi$ from the set $A^*$ of lists in $A$ to the set $S$. Such functions are called automatic.

In practice, some states could be labeled as admissible, in which case the machine unlocks the door, and the set of lists $\alpha\in A^*$ such that $\Phi(\alpha)$ is admissible is then called the language of the automaton.

The basic question of automata theory is to describe the (so-called “regular”) languages recognizable by some automaton, more generally the automatic functions. It appears that they are of a very restricted nature: due to the elementary nature of finite automata, they are much more restricted than the kind of languages that would be recognizable by a program in the programming language of your choice. The reason is that they have a fixed memory while “theoretical” computers, as modelled by Turing machines for example, have a potentially infinite memory, that is, as large as the computation may require.

Numbers

Number theory enters when you decide that the set $A$ of instructions are digits 0, 1, 2,…, 9 and the lists in $A^*$ represent a number. You then wish to understand what numbers can be recognizable, or what functions $\Phi\colon\mathbf N\to S$ are automatic, for a finite set $S$. This is what happens, for example, in the very elementary finite automata that stand at almost all Paris doors as electronic locks. They recognize exactly one 4-digit number (and any 4-digit number) puts them back in the initial state.

When it comes about digits, they can be the usual ones, 0, 1, 2,… , 9, writing number in base 10, but any other basis can be considered, and any set of digits that allows to write all numbers can be used. For example, one can consider writing numbers in base 3, with digits 0, 1, 2, 3, 4.

Let us thus fix some basis $b$. The first theorem is that the set of automatic functions does not depend on the set of digits which is considered. The reason is that one can build another kind of machine (called a transducer) that works like a finite automaton except that it output something at each step. Here, we can have a transducer that outputs the digits in some representation given the digits in another one. There could be carries to take care of, but when the basis is the same, their impact is controlled, and it can be controlled by finitely many of them. It is important for this argument that the basis stays the same, and we will see that in a more striking way later on. For this reason, we will not specify the set of digits in the sequel.

Examples

Here are some examples of recognizable sets of numbers.

• The empty set works. It suffices to have no terminal state.
• Singletons work. For example, to recognize “314”, one needs one initial state “$\varepsilon$”, three states labeled “3”, “31” and “314”, and a junk state “J”. The machine moves from “$\varepsilon$” to “3” if it receives “3”, and to “J” otherwise; from “3” to “31” if it receives “1”, etc.
• The union and the intersection of two recognizable sets are recognizable. Just make an automaton whose sets are pair of states of the two automata that recognize the given states, and simulate the moves of each of them. Similarly, the complement of a recognizable set is recognizable.
• By the previous examples, finite sets and complements of finite sets are recognizable.
• Here is a number theoretically more interesting example : arithmetic progressions are recognizable. To produce an automaton that, say, recognize all integers congruent to 1 modulo 4, it suffices to have a machine with 4 states that computes the euclidean reminder step by step.
• Another number theoretically interesting example: powers of $b$. Indeed their writing in base $b$ consists of one digit “1” followed by a series of “0”.
• A number theoretically annoying property of recognizable sets: since a finite automaton has finitely many states, the “pumping lemma” shows that for any large enough recognizable number, one can replicate at will some inner part of the writing and get another number. I suppose one can deduce from this property that the set of prime numbers cannot be recognizable. (This is exercise 5.8.12 in the book Automatic sequences, by J-P. Allouche and J. Shallit.)
• Numbers recognizable in base $b$ are also recognizable in base $b^2$ (or some other power) and conversely: it suffices to emulate the base $b^2$-writing of a number using base $b$-digits, or conversely.

Building from characteristic functions of admissible languages, the preceding results can be turned to examples of automatic functions. In particular, we obtain that functions which are ultimately periodic are automatic.

Cobham's theorem

Statement

Number theory can also enter a topic from two sides at a time, and here is the point of this blog post. Can one compare the sets of recognizable numbers from different bases? By the following theorem, they are genuinely distinct.

Theorem (Cobham, 1969). — Let $S$ be a finite set and let $f\colon \mathbf N\to S$ be a function which is automatic in two bases $b$ and $c$. If $b$ and $c$ are not powers of the same integer, then $f$ is ultimately periodic.
Since ultimately periodic functions are automatic in any basis, this theorem is definitely optimal.

The original proof of Cobham's theorem is said to be difficult, and this theorem has obtained various other simpler proofs, often partially flawed. I wish to describe here the recent proof by Thijmen Krebs (publisher version, arXiv:1801.06704) which calls itself “more reasonable”.

The assumption that $a$ and $b$ are not powers of the same integer will appear in different, equivalent, form in the proof: they do not have common powers.

Local periods

To prove that $f$ is ultimately periodic, Krebs proves that $f$ is periodic on large overlapping intervals.

Lemma 1. — Let $f: \mathbf N\to S$ be a function and let $I$ and $J$ be intervals of integers. We assume that $f$ has period $p$ on $I$ and period $q$ on $J$. If $\operatorname{Card}(I\cap J)\geq p+q$, then $f$ has period $p$ on the interval $I\cup J$.

The proof is elementary. Consider $x\in I\cup J$ such that $x+p\in I\cup J$. If both $x$ and $x+p$ belong to $I$, then $f(x)=f(x+p)$. Let us assume otherwise. If $x$ belongs to $I$, but not $x+p$, then $x+p\in J$; since $I\cap J$ has at least $p+q$ elements, $x$ must belongs to $J$. The other cases are similar and show that both $x, x+p$ belong to $J$. Using that $I\cap J$ is large, we pick up elements $y,y+p$ in $I\cap J$ such that $x\equiv y \pmod q$. Then $f(x)=f(y)=f(y+p)=f(x+p)$, the first and last equality using the $q$-periodicity on $J$, and the middle one the $p$-periodicity on $I$.

A diophantine approximation lemma

Lemma 2. — Let $a$ and $b$ be two real numbers such that $a,b>1$. For every $\varepsilon>0$, there exist nonzero natural numbers $m$ and $n$ such that $\abs{a^m-b^n}<\varepsilon b^n$.

The result is obvious if $a$ and $b$ have a common power, so we may assume that this is not the case. Then various proofs are possible. For example, one may consider the additive subgroup of $\mathbf R$ generated by $\log(a)$ and $\log(b)$; by assumption, it is dense hence there exists a small linear combination $m\log(a)-n\log(b)$; taking exponentials, $a^m/b^n$ is close to~$1$, as claimed.

Krebs gives a “pigeonhole-like” proof which is nice. For every integer $m\geq1$, consider the unique integer $n_m\geq 1$ such that $1\leq a^m/b^{n_m}<b$. There must be two integers $m$ and $p$ such that $m<p $ and such that $a^m/b^{n_m}$ and $a^p/b^{n_p}$ differ at most from $\varepsilon$, and this implies the result.

Some functional equations

Let $f\colon \mathbf N\to S$ be a function which is automatic in some basis $c$, computed by an automaton with set of states $S$. For every $s\in S$, let $L(s)$ be the set of integers $n$ such that $f(n)=s$. Note that these sets form a partition of $\mathbf N$.

The following lemma is a variant of the pumping lemma in the theory of automata; it is by it that automatic functions acquire their specific properties.

Lemma 3. — For every integers $x,y\in L(s)$ and any integer $z$ such that $0\leq z < c^n$, one has $f(x c ^ n+z)=f(yc ^n +z)$.

Indeed, when the automaton reads the integer $xc^n+z$, it first reads $x$, and goes to state $s$; similarly, when it reads $yc^n+z$, it first reads $y$ and reaches the state $s$ too. In both cases it then reads $z$ and ends up in the same final state.

Construction of local periods

We now consider a function $f$ which is automatic in two bases $a$ and $b$ which do not have common powers. We thus have two finite automata $A$ and $B$, with sets of states $S$ and $T$. For each state $s\in S$, we have a set $L(s)$ of integers as above; these sets form a partition of $\mathbf N$. Let $S^\infty$ be the set of states $s\in S$ such that $L(s)$ is infinite. For $t\in T$, we define $M(t)$ similarly, as well as $T^\infty$.

Let $s\in S^\infty$. Since the $M(t)$, for $t\in T$, form a finite partition of $\mathbf N$ and $L(s)$ is infinite, there exists a state $t(s)$ and two distinct integers $x(s)$ and $y(s)\in L(s)\cap M(t(s))$. Let $K$ be an integer strictly greater than all $x(s), y(s)$, for $s\in S^\infty$.

Applying lemma 3 for $\varepsilon = 1/6K$, we obtain integer $m,n$ such that $\abs{a^m-b^n}<a^m/6K$. For $s\in S^\infty$, we $p(s)=\pm (x(s)-y(s))(a^m-b^n)$; since $a$ and $b$ have no common power, this is a nonzero integer, and we choose the sign so that it is strictly positive.

For each integer $x$, we define an interval $I_x$ of integers by $I_x=[(x+\frac13)a^m,(x+\frac53)a^m]\cap\mathbf N$.

Lemma 4. — For every state $s\in S_\infty$ and any integer $x\in L(s)$, the function $f$ has period $p(s)$ on $I_x$.

To that aim, we consider $z\in [\frac13a^m,\frac53a^m]$ and prove that $f(xa^m+z)=f(xa^m+z+p)$. First of all, we have the inequality $$ \abs{z-x(s)(a^m-b^n)-b^n} \leq \abs{z-a^m}+(x(s)+1) \abs{a^m-b^n} \leq \frac23 a^m + K\abs{a^m-b^n} \leq \frac56a^m\leq b^n $$ because $\abs{a^m-b^n}\leq \frac16 a^m$. Consequently, $z$ is written with at most $n$ digits in base $b$. Applying lemma 3, we have $ f(x a^m+z) = f(x(s)a^m+z$, because $x$ and $x(s)\in L(s)$. Applying lemma 3 again, this is equal to $f(x(s)a^m+z-x(s)(a^m-b^n))$, hence to $f(y(s)a^m+z-x(s)(a^m-b^n)) = f(y(s)a^m+z+p(s))$. Applying lemma 3 a third time, this is equal to $f(xa^m+z+p(s)$. This concludes the proof.

Conclusion

Since the sets $L(s)$, for $s\notin S_\infty$ are finite, the set $L(s)$ for $s\in S_\infty$ cover all integers larger than some integer, say $x$.

For $y\geq x$, there exists $s\in S_\infty$ such that $y\in L(s)$ and we have shown that $f$ is periodic with period $p(s)\leq \frac16a^m$ on an interval $I(x)=[(y+\frac13)a^m,(y+\frac53)a^m]$. By abuse of notation, write $p(x)=p(s)$.

Let $J(z)$ be the union of the intervals $I(y)$, for $x\leq y\leq z$. One has $J(x)=I(x)$; for $z>x$, the intersection $J(z)\cap J(z-1)$ is $[(z+\frac13)a^m;(z+\frac23)a^m]$ hence has at least $\frac13a^m$ points, thus at least $p(x)+p(z)$. Using lemma 1, $f$ has period $p(x)$ on $J(z)$, for all $z$.

This concludes the proof that $f$ is ultimately periodic