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.

Yet another proof of the Weierstrass approximation theorem

Browsing through my Zotero database, I fall upon a paper by Harald Kuhn where he proposes an elementary proof of the Weierstrass approximation theorem. The proof is indeed neat, so here it is.

Theorem. — Let $f\colon[0;1]\to\mathbf R$ be a continuous function and let $\varepsilon$ be a strictly positive real number. There exists a polynomial $P\in\mathbf R[T]$ such that $\left|P(x)-f(x)\right|<\varepsilon$ for every $x \in[0;1]$.

The proof goes out of the world of continuous functions and considers the Heaviside function $H$ on $\mathbf R$ defined by $H(x)=0$ for $x<0$ and $H(x)=1$ for $x\geq 0$ and will construct a polynomial approximation of $H.$

Lemma. — There exists a sequence $(P_n)$ of polynomials which are increasing on $[-1;1]$ and which, for every $\delta>0$, converge uniformly to the function $H$ on $[-1;1]\setminus [-\delta;\delta]$.

For $n\in\mathbf N$, consider the polynomial $Q_n=(1-T^n)^{2^n}$. On $[0;1]$, it defines an decreasing function, with $Q_n(0)=1$ and $Q_n(1)=0$.

Let $q\in[0;1]$ be such that $0\leq q<1/2$. One has $$ Q_n(q) = (1-q^n)^{2^n} \geq 1-2^n q^n $$ in view of the inequality $(1-t)^n \geq 1-nt$ which is valid for $t\in[0;1]$. Since $2q<1$, we see that $Q_n(q)\to 1$. Since $Q_n$ is decreasing, one has $Q_n(q)\leq Q_n(x)\leq Q_n(1)=1$ for every $x\in[0;q]$, which shows that $Q_n$ converges uniformly to the constant function $1$ on the interval $[0;q]$.

Let now $q\in[0;1]$ be such that $1/2<q\leq 1$. Then $$ \frac1{Q_n(q)} = \frac1{(1-q^n)^{2^n}} = \left(1 + \frac{q^n}{1-q^{n}}\right)^{2^n} \geq 1 + \frac{2^nq^n}{1-q^{n}} $$ so that $Q_n(q)\to 0$. Since $Q_n$ is decreasing, one has $0=Q_n(1)\leq Q_n(x)\leq Q_n(q)$ for every $x\in[q;1]$, so that $Q_n$ converges uniformly to the constant function $0$ on the interval $[q;1]$.

Make an affine change of variables and set $P_n = Q_n((1-T)/2)$. The function defined by $P_n$ on $[-1:1]$ is increasing; for any real number $\delta$ such that $\delta>0,$ it converges uniformly to $0$ on $[-1;-\delta]$, and it converges uniformly to $1$ on $[\delta;1]$. This concludes the proof of the lemma.

We can now turn to the proof of the Weierstrass approximation theorem. Let $f$ be a continuous function on $[0;1]$. We may assume that $f(0)=0.$

The first step, that follows from Heine's uniform continuity theorem, consists in noting that there exists a uniform approximation of $f$ by a function of the form $ F(x)=\sum_{m=1}^N a_m H(x-c_m)$, where $(a_1,\dots,a_m)$ and $(c_1,\dots,c_m)$ are real numbers in $[0;1].$ Namely, Heine's theorem implies that there exists $\delta>0$ such that $|f(x)-f(y)|<\varepsilon$ if $|x-y|<\delta$. Choose $N$ such that $N\delta\geq 1$ and set $c_m=m/N$; then define $a_1,\dots,a_N$ so that $a_1=f(c_1)$, $a_1+a_2=f(c_2)$, etc. It is easy to check that $|F(x)-f(x)|\leq \varepsilon$ for every $x\in[0;1]$. Moreover, $\lvert a_m\rvert\leq\varepsilon/2$ for all $m$.

Now, fix a real number $\delta>0$ small enough so that the intervals $[c_m-\delta;c_m+\delta]$ are pairwise disjoint, and $n\in\mathbf N$ large enough so that $|P_n(x)-H(x)|\leq\varepsilon/2A$ for all $x\in[-1;1]$ such that $\delta\leq|x|$, where $A=\lvert a_0\rvert+\dots+\lvert a_N\rvert$. Finally, set $P(T) = \sum_{m=1}^N a_m P_n(T-c_m)$.

Let $x\in[-1;1]$. If $x$ doesn't belong to any interval of the form $[c_m-\delta;c_m+\delta]$, one can write $$\lvert P(x)-F(x)\rvert\leq \sum_{m} \lvert a_m\rvert \,\lvert P_n(x-c_m)- H(x-c_m)\rvert \leq \sum_m \lvert a_m\rvert (\varepsilon/A)\leq \varepsilon. $$ On the other hand, if there exists $m\in\{1,\dots,N\}$ such that $x\in[c_m-\delta;c_m+\delta]$, then there exists a unique such integer $m$. Writing $$\lvert P(x)-F(x)\rvert\leq \sum_{k\neq m} \lvert a_k\rvert \,\lvert P_n(x-c_k)- H(x-c_k)\rvert + \lvert a_m\rvert\, \lvert P_n(x-c_m)-H(x-c_m)\rvert, $$ the term with index $k$ in the first sum is bounded by $\lvert a_k\rvert \varepsilon/A$, while the last term is bounded by $ \lvert a_m\rvert$, because $0\leq P_n\leq H\leq 1$. Consequently, $$\lvert P(x)-F(x)\rvert \leq (\varepsilon/2A)\sum_{k\neq m} \lvert a_k\rvert +\lvert a_m\rvert \leq 2\varepsilon.$$ Finally, $\lvert P(x)-f(x)\rvert\leq \lvert P(x)-F(x)\rvert+\lvert F(x)-f(x)\rvert\leq 3\varepsilon$. This concludes the proof.

Yet another proof of the inequality between the arithmetic and the geometric means

This is an exposition of the proof of the inequality between arithmetic and geometric means given by A. Pełczyński (1992), “Yet another proof of the inequality between the means”, Annales Societatis Mathematicae Polonae. Seria II. Wiadomości Matematyczne, 29, p. 223–224. The proof might look bizarre, but I can guess some relation with another paper of the author where he proves uniqueness of the John ellipsoid. And as bizarre as it is, and despite the abundance of proofs of this inequality, I found it nice. (The paper is written in Polish, but the formulas allow to understand it.)

For $n\geq 1$, let $a_1,\dots,a_n$ be positive real numbers. Their arithmetic mean is $$ A = \dfrac1n \left(a_1+\dots + a_n\right)$$ while their geometric mean is $$G = \left(a_1\dots a_n\right)^{1/n}.$$ The inequality of the title says $G\leq A,$ with equality if and only if all $a_k$ are equal. By homogeneity, it suffices to prove that $A\geq 1$ if $G=1$, with equality if and only if $a_k=1$ for all $k.$ In other words, we have to prove the following theorem.

Theorem. — If $a_1,\dots,a_n$ are positive real numbers such that $a_1\dots a_n=1$ and $a_1+\dots+a_n\leq n,$ then $a_1=\dots=a_n=1.$

The case $n=1$ is obvious and we argue by induction on $n$.

Lemma. — If $a_1\cdots a_n=1$ and $a_1+\dots+a_n\leq n,$ then $a_1^2+\dots+a_n^2\leq n$

Indeed, we can write $$ a_1^2+\dots+a_n^2 = (a_1+\dots+a_n)^2 - \sum_{i\neq j} a_i a_j \leq n^2 - \sum_{i\neq j} a_i a_j,$$ and we have to give a lower bound for the second term. For given $i\neq j$, the product $a_i a_j$ and the remaining $a_k$, for $k\neq i,j$, are $n-1$ positive real numbers whose product is equal to $1$. By induction, one has $$ n-1 \leq a_i a_j + \sum_{k\neq i,j}a_k.$$ Summing these $n(n-1)$ inequalities, we have $$ n(n-1)^2 \leq \sum_{i\neq j} a_i a_j + \sum_{i\neq j} \sum_{k\neq i,j} a_k.$$ In the second term, every element $a_k$ appears $(n-1)(n-2)$ times, hence $$ n(n-1)^2 \leq \sum_{i\neq j} a_i a_j + (n-1)(n-2) \sum_{k} a_k \leq \sum_{i\neq j} a_i a_j + n(n-1)(n-2), $$ so that $$ \sum_{i\neq j} a_i a_j \geq n(n-1)^2-n(n-1)(n-2)=n(n-1).$$ Finally, we obtain $$a_1^2+\dots+a_n^2 \leq n^2-n(n-1)=n,$$ as claimed.

We can iterate this lemma: if $a_1+\dots+a_n\leq n$, then $$a_1^{2^m}+\dots+a_n^{2^m}\leq n$$ for every integer $m\geq 0$. When $m\to+\infty$, we obtain that $a_k\leq 1$ for every $n$. Since $a_1\dots a_n=1$, we must have $a_1=\dots=a_n=1$, and this concludes the proof.

A generalization of the Eisenstein criterion

Recently, in the Zulip server for Lean users, somebody went with something that looked like homework, but managed to sting me a little bit.

It was about irreducibility of polynomials with integer coefficients. Specifically, the guy wanted a proof that the polynomial $T^4-10 T^2+1$ is irreducible, claiming that the Eisenstein criterion was not good at it.

What was to proven (this is what irreducible means) is that it is impossible to write that polynomial as the product of two polynomials with integer coefficients, except by writing $T^4-10 T^2+1$ as $(1)·(T^4-10 T^2+1)$ or as $ (-1)·(-T^4+10 T^2-1)$.

This is both a complicated and a trivial question

Trivial because there are general bounds (initially due to Mignotte) for the integers that appear in any such factorization, and it could just be sufficient to try any possibility in the given range and conclude. Brute force, not very intelligent, but with a certain outcome.

Complicated because those computations would often be long, and there are many criteria in number theory to assert irreducibility.

One of the easiest criteria is the aforementioned Eisenstein criterion.

This criterion requires an auxiliary prime number, and I'll state it as an example, using another polynomial, say $T ^ 4 - 10 T ^ 2 + 2$. Here, one takes the prime number 2, and one observes that modulo 2, the polynomial is equal to $T ^ 4$, while the constant term, 2, is not divisible by $2^2=4$. In that case, the criterion immediately asserts that the polynomial $T^4-10T^2+2$ is irreducible.

With all due respect to Eisenstein, I don't like that criterion too much, though, because it only applies in kind of exceptional situations. Still, it is often useful.

There is a classic case of application, by the way, of the Eisenstein criterion, namely the irreducibility of cyclotomic polynomials of prime index, for example, $T^4+T^3+T^2+T+1$ (for the prime number $p=5$). But it is not visible that the criterion applies, and one needs to perform the change of variable $T = X+1$.

I had noticed that in that case, it maybe interesting to generalize the Eisenstein criterion to avoid this change of variables. Indeed, for a monic polynomial $f$ in $\mathbf Z[T]$, a variant of the criterion states: take an integer $a$ and a prime number $p$, and assume that :

• $f(T) \equiv (T-a)^d \mod p$
• $f'(a)$ (derivative at $a$) is not divisible by $p^2$.

Then $f$ is irreducible.

For the cyclotomic polynomial of index $5$, $f(T) = T^4+T^3+T^2+T+1$, still taking $p=5$, one has $f(T) \equiv (T-1)^4 \pmod5$ and $f'(1)=4·5/2=10$ is not divisible by $5^2=25$. Consequently, it is irreducible. And the same argument works for all cyclotomic polynomials of prime index.

The reason, that avoids any strange computation, is that $f(T)=(T^5-1)/(T-1)$, which modulo 5 is $(T-1)^4$ — by the divisibility of the binomial coefficients.

To go back to the initial example, $T^4-10T^2+1$, there are indeed no prime numbers with which the Eisenstein criterion can be applied. This is obvious in the standard form, because the constant coefficient is 1. But the variant doesn't help neither. The only prime it could seems to be 2, but its derivative at 1 is equal to $-16$, and is divisible by 4.

This is where a new variant of the criterion can be applied, this time with the prime number 3.

Theorem. — Let $q\in\mathbf Z[T]$ be a monic polynomial, let $p$ be a prime number such that $q$ is irreducible in $\mathbf F_p[T]$. Let $f\in\mathbf Z[T]$ be a monic polynomial. Assume that $f\equiv q^d$ modulo $p$, but that $f\not\equiv 0$ modulo $\langle q, p^2\rangle$. Then $f$ is irreducible in $\mathbf Z[T]$.

To see how this criterion applies, observe that modulo 3, one has $f(T)\equiv T^4+2T^2+1=(T^2+1)^2\pmod 3$. So we are almost as in the initial criterion, but the polynomial $T$ is not $T^2+1$. The first thing that allows this criterion to apply is that $T^2+1$ is irreducible modulo 3. In this case, this is because $-1$ is not a square mod 3.

The criterion also requires of variant of the condition on the derivative — it holds because the polynomial is not zero modulo $\langle T^2+1, 9\rangle. Here, one has \[ T^4-10T^2+1=(T^2+1)^2-12T^2 = (T^2+1)^2-12(T^2+1)+12\] hence it is equal to 3 modulo $\langle T^2+1, 9\rangle$.

And so we have an Eisenstein-type proof that the polynomial $T^4-10T^2+1$ is irreducible over the integers. CQFD!

I made the fun last a bit longer by formalizing the proof in Lean, first of the generalized criterion, and then of the particular example. It is not absolutely convincing yet, because Lean/Mathlib still lacks a bit of tools for handling explicit computations. And probably many parts can be streamlined. Still, it was a fun exercise to do.

The proof works in a more general context and gives the following theore:

Theorem. — Let $R$ be an integral domain, let $P$ be a prime ideal of $R$ and let $K$ be the field of fractions of $R/P$. Let $q\in R[T]$ be a monic polynomial such that $q$ is irreducible in $K[T]$. Let $f\in R[T]$ be a monic polynomial. Assume that $f\equiv q^d$ modulo $P$, but that $f\not\equiv 0$ modulo $\langle q\rangle + P^2$. Then $f$ is irreducible in $R[T]$.

A simple proof of a theorem of Kronecker

Kronecker's theorem of the title is the following.

Theorem. — Let $\alpha\in\mathbf C$ be an algebraic integer all of whose conjugates have absolute value at most $1$. Then either $\alpha=0$, or $\alpha$ is a root of unity.

This theorem has several elementary proofs. In this post, I explain the simple proof proposed by Gebhart Greiter in his American Mathematical Monthly note, adding details so that it would (hopefully) be more accessible to students.

The possibility $\alpha=0$ is rather unentertaining, hence let us assume that $\alpha\neq0$.

Let us first analyse the hypothesis. The assumption that $\alpha$ is an algebraic integer means that there exists a monic polynomial $f\in\mathbf Z[T]$ such that $f(\alpha)=0$. I claim that $f$ can be assumed to be irreducible in $\mathbf Q[T]$; it is then the minimal polynomial of $\alpha$. This follows from Gauss's theorem, and let me give a proof for that. Let $g\in \mathbf Q[T]$ be a monic irreducible factor of $f$ and let $h\in\mathbf Q[T]$ such that $f=gh$. Chasing denominators and dividing out by their gcd, there are polynomials $g_1,h_1\in\mathbf Z[T]$ whose coefficients are mutually coprime, and natural integers $u,v$ such that $g=ug_1$ and $h=vh_1$. Then $(uv)f=g_1 h_1$. Since $f$ is monic, this implies that $uv$ is an integer. Let us prove that $uv=1$; otherwise, it has a prime factor $p$. Considering the relation $(uv)f=g_1h_1$ modulo $p$ gives $0=g_1 h_1 \pmod p$. Since their coefficients are mutually coprime, the polynomials $g_1$ and $h_1$ are nonzero modulo $p$, hence their product is nonzero. This is a contradiction.

So we have a monic polynomial $f\in\mathbf Z[T]$, irreducible in $\mathbf Q[T]$, such that $f(\alpha)=0$. That is to say, $f$ is the minimal polynomial of $\alpha$, so that the conjugates of $\alpha$ are the roots of $f$. Note that the roots of $f$ are pairwise distinct — otherwise, the $\gcd(f,f')$ would be a nontrivial factor of $f$. Moreover, $0$ is not a root of $f$, for otherwhise one could factor $f=T\cdot f_1$.

Let us now consider the companion matrix to $f$: writing $f=T^n+c_1T^{n-1}+\dots+c_n$, so that $n=\deg(f)$, this is the matrix \[ C_f = \begin{pmatrix} 0 & \dots & 0 & -c_n \\ 1 & \ddots & \vdots & -c_{n-1} \\ 0 & \ddots & & -c_{n-2} \\ 0 & \cdots & 1 & -c_1 \end{pmatrix}.\] If $e_1,\ldots,e_n$ are the canonical column vectors $e_1=(1,0,\dots,0)$, etc., then $C_f\cdot e_1=e_2$, \ldots, $C_f \cdot e_{n-1}=e_{n}$, and $C_f\cdot e_n = -c_{n} e_1-\dots -c_1 e_n$. Consequently, \[ f(C_f)\cdot e_1 = C_f^n\cdot e_1 +c_1 C_f^{n_1} \cdot e_1+ \dots +c_n e_1 = 0.\] Moreover, for $2\leq k\leq n$, one has $f(C_f)\cdot e_k=f(C_f)\cdot C_f^{k-1}\cdot e_1=C_f^{k-1}\cdot f(C_f)\cdot e_1=0$. Consequently, $f(C_f)=0$ and the complex eigenvalues of $f(C_f)$ are roots of $f$. Since $f$ has simple roots, $C_f$ is diagonalizable and their exists a matrix $P\in\mathrm{GL}(n,\mathbf C)$ and diagonal matrix $D$ such that $C_f=P\cdot D\cdot P^{-1}$, the diagonal entries of $D$ are roots of $f$. Since $0$ is not a root of $f$, the matrix $D$ is invertible, and $C_f$ is invertible as well. More precisely, one can infer from the definition of $C_f$ that $g(C_f)\cdot e_1\neq 0$ for any nonzero polynomial $g$ of degre $<n$, so that $f$ is the minimal polynomial of $C_f$. Consequently, all of its roots are actually eigenvalues of $C_f$, and appear in $D$; in particular, $\alpha$ is an eigenvalue of $C_f$.

For every $k\geq 1$, one has $C_f^k=P\cdot (D^k)\cdot P^{-1}$. Since all entries of $D$ have absolute value at most $1,$ the set of all $D^k$ is bounded in $\mathrm{M}_n(\mathbf C)$. Consequently, the set $\{C_f^k\,;\, k\in\mathbf Z\}$ is bounded in $\mathrm M_n(\mathbf C)$. On the other hand, this set consists in matrices in $\mathrm M_n(\mathbf Z)$. It follows that this set is finite.

There are integers $k$ and $\ell$ such that $k< \ell$ and $C_f^k=C_f^\ell$. Since $C_f$ is invertible, one has $C_f^{\ell-k}=1$. Since $\alpha$ is an eigenvalue of $C_f,$ this implies $\alpha^{\ell-k}=1$. We thus have proved that $\alpha$ is a root of unity.

On numbers and unicorns

Reading a book on philosophy of mathematics, even if it's written lightly, such as that one, Why is there philosophy of mathematics at all? by Ian Hacking, may have unexpected effects. The most visible one has been a poll that I submitted on Mastodon on December 4th. As you can read, there were four options:

• Numbers exist
• Unicorns exist
• Numbers have more existence than unicorns
• Neither numbers no unicorns exist

As you can see, three main options each share a rough third of the votes, the existence of unicorns being favored by a small 4% of the 142 participants.

Post by @antoinechambertloir@mathstodon.xyz

View on Mastodon

In this post, I would like to discuss these four options, from the point of view of a mathematician with a limited expertise on philosophy. Funnily, each of them, including the second one, has some substance. Moreover, it will become apparent at the end that the defense of any of those options relies on the meaning we give to the word exist.

Numbers exist

We have traces of numbers as old as we have traces of writing. The Babylonian clay tablet known as “Plimpton 322” dates from 1800 BC and mentions Pythagorean triples (triples of integers $(a,b,c)$ such $a^2=b^2+c^2$) written in the sexagesimal (base 60) writing of Babylonians. More than 1000 years later, Pythagoras and his school wished to explain everything in the world using numbers, usually depicted geometrically, drawing pebbles arranged in triangles, squares, rectangles and even pentagons. Musical harmony was based on specific numerical ratios. Plato's writings are full of references to mathematics, and a few specific numbers, such as 5040, are even given a political relevance. Even earlier, the Chinese I Ching based predictions on random numbers.

Euclid's Elements give us an account of numbers that still sounds quite modern. A great part of elementary arithmetic can be found there: divisibility, the “Euclidean algorithm”, prime numbers and the fact that there are infinitely many of them or, more precisely, that there are more prime numbers than any given magnitude. On the other hand, it is worth saying that Euclid's concept of number doesn't exactly fit with our modern concept: since “A number is a multitude composed of units”, numbers are whole numbers, and it is implicit that that zero is not a number, and neither is one. Moreover, proposition 21 of book 10, which we read as proving the irrationality of the square root of 2, is not a statement about a hypothetical number called “square root of 2”, but the fact that the diagonal of a square of unit length is irrational, ie, not commensurable with the unit length.

History went on and on and numbers gradually were prevalent in modern societies. Deciding the exact date of Easter in a ill-connected Christian world led to the necessity of computing it, using an algorithm known as computus, and the name happened to be used for every calculation. The development of trade led to the development of computing devices, abacus, counting boards (the counter at your prefered shop is the place where the counting board was laid), and Simon Stevin's De Thiende explicitly motivates trade as an application of his book on decimal fractions.

Needless to say, our digital age is litteraly infused with numbers.

Unicorns exist

Traces of unicorns can be found by the Indus valley. The animal seems to have disappeared but the Greeks thought they lived in India. In Western Europe, Middle ages tapestry gives numerous wonderful representations of unicorns, such as the Paris Dame à la licorne. This extract from Umberto Eco's The name of the rose gives additional proof of their existence:

“But is the unicorn a falsehood? It’s the sweetest of animals and a noble symbol. It stands for Christ, and for chastity; it can be captured only by setting a virgin in the forest, so that the animal, catching her most chaste odor, will go and lay its head in her lap, offering itself as prey to the hunters’ snares.”
“So it is said, Adso. But many tend to believe that it’s a fable, an invention of the pagans.”
“What a disappointment,” I said. “I would have liked to encounter one, crossing a wood. Otherwise what’s the pleasure of crossing a wood?”

The Internet age gave even more evidence to the existence of unicorns. For example, we now know that though it is not rainbowish, contrary to a well-spread myth, unicorns have a colorful poop.

Numbers have more existence than unicorns

Whatever numbers and unicorns could be, we are litteraly surrounded by the former, and have scarce traces of the latter. I'd also like to add that numbers have a big impact in all modern human activities: the most basic trading activities use numbers, as does the most sophisticated science. But we don't need to wish to send a man to the moon to require numbers: the political life is build around votations and polls, all timed schedules are expressed in numbers, and schools, hospitals, movies are regularly ranked or assigned rates. An example given by Hacking is the existence of world records for, say, 50 m free stroke swimming. That requires good swimmers, of course, but also elaborate timers, very precise measurement tools to have the swimming pool acknowledged as a legitimate place, and so on. On the other hand, how nice the cultural or artistic representations of unicorns can be, they don't have that prevalence in the modern world, and it is rare that something is possible because of something involving unicorns.

Neither numbers nor unicorns exist

This is probably my favorite take, and that's maybe slightly bizarre from a mathematician, especially one versed in number theory. But give some lucid look at the discourse that we have about numbers. On one side, we have the famous quote of Leopold Kronecker, “Die ganzen Zahlen hat der liebe Gott gemacht, alles andere ist Menschenwerk.” — God made whole numbers, all the rest is the work of man. Does this mean that at least some numbers, the natural integers, exist in the world in the same way that we can find water, iron, gold or grass? Are there number mines somewhere? It doesn't seem so, and I'm inclined to say that if numbers exist, they also are the creation of mankind. The ZFC axioms of set theory postulate the existence of some set $\mathbf N$ satisfying an induction principle, and that induction principle is used to endow that set with an addition and a multiplication which make it a mathematical model of Kronecker's “whole numbers”, but does this mean that numbers exist? After all, what does guarantee that the ZFC axioms are not self contradictory? And if they were, would that mean that whole numbers cease to exist? Certainly not. In any case, our daily use of whole numbers would not be the least disturbed by a potential contradiction in those axioms. But that indicates that being able to speak of integers withing the ZFC set theory doesn't confer those integers some existence, in the same sense that grass, water, iron exist. Another indication of their elusive character is the way mathematicians or computer scientists pretend numbers are specific objects, such as zero being the empty set, 1 being the set $\{\emptyset\}$, and, more generally, the integer $n+1$ being $n \cup \{n\}$. This is at most a functional fiction, as is well explained by Benacerraf (1965) in his paper, “What numbers could not be” (The Philosophical Review, Vol. 74, No. 1, pp. 47-73).

But all in all, everything is fine, because whether numbers (resp. unicorns) exist or don't, we, humans, have developed a language to talk about them, make us think, make us elaborate new works of art or of science, and after all, this is all that counts, isn't it?