Aristotle from HarmonicMath has solved Erdős Problem 124 in LEAN

[This is a guest post by Boris Alexeev. Now over to Boris.]

I’m here to tell you about various exciting developments centering on Erdős problems, especially involving the formalization of old and new mathematics using artificial intelligence.

Background

As is well known, Paul Erdős was a prolific mathematician of the 20th century who posed an extraordinary number of conjectures. Around May 2023, Thomas Bloom set up erdosproblems.com to collect these problems and keep track of progress on them. Over the past 2.5 years, this progress has accelerated as many people realized they could solve problems that were previously unknown to them. In August 2025, Thomas added a forum that became active very quickly, further accelerating developments.

In May 2025, Google DeepMind launched the Formal Conjectures project, an open repository of formalized mathematics conjectures, including (but not at all limited to) Erdős problems. In August 2025, Thomas Bloom and Terence Tao proposed a crowdsourced project to link up erdosproblems.com to the Online Encyclopedia of Integer Sequences (OEIS). These are both part of a greater push to increase the number of mathematical databases, as well as links between them.

At present, there are over 1100 problems on erdosproblems.com, of which approximately 40% have been solved. (Note that only ~100 problems are known to have monetary prizes associated with them.) Approximately 240 problems have statements formalized in Lean, and 17 have solutions formalized in Lean. Approximately 260 problems have been linked to sequences in the OEIS. Alexis Olson has implemented a progress graph displaying these statistics visually over time.

Human formalization without AI

At first, formalization was not a large part of the story with Erdős problems. One of the first developments was several years ago when Thomas Bloom and Bhavik Mehta formalized Bloom’s solution to Problem 47 about unit fractions (and its further applications to several related problems). I would like to highlight a couple of passages from their paper (emphasis mine):

The formalisation began in January 2022 and concluded in July 2022. At the beginning of the formalisation, the first author had no experience with Lean at all, and learnt Lean (or at least a sufficient subset of Lean) through the formalising process.

and

This formalisation is a first in several respects: it is the first recent analytic number theory result to be formally verified; the first instance of the circle method; the first solution to a long-standing problem of Erdős. Part of the motivation for this formalisation was as a proof of concept: the Lean proof assistant and accompanying mathlib is advanced enough to make feasible the fast formalisation of new research results in mathematics, on the same timescale as the production of the ‘human-readable’ paper. Of course, this was made feasible by the relatively elementary and self-contained nature of the mathematics involved. Nonetheless, we believe that this arrangement, with a formal certificate of validation accompanying the human version of the paper, is a sign of things to come.

In this post, I focus mostly on the formalization of solutions that completely resolve a problem, but following this proof, there was a lot of great formalization work for results that don’t technically resolve a problem in full. Luckily, this blog has already featured a guest post by Bhavik Mehta of this kind involving Problem 77. Similarly, last year, there was some extensive work on Problem 216 and separately involving the Hadwiger-Nelson problem (which is Problem 508 ).

I am not personally aware of any further developments in this area (my apologies to anyone I left out!) until the launch of the Formal Conjectures project. This project, of course, includes the formalization of a large (and increasing) number of the statements of Erdős problems, but does not generally include the formalization of solutions. Nonetheless, it does include a succinct proof by Bhavik Mehta of a counterexample to Problem 316 found by Tom Stobart (slightly smaller than Csaba Sándor’s original counterexample).

Shortly after the launch of the forum on erdosproblems.com, a collaboration between Stijn Cambie, Vjekoslav Kovač, and Terence Tao resolved Problem 379, with the solution formalized in Lean. A couple of days later, Terence Tao also resolved Problem 987 (unaware that Erdős himself had done so) and formalized the solution in Lean. I believe that both of these formalizations were done primarily “by hand”.

Human formalization with AI

Kevin’s latest blog post, discussing the formal and informal approaches to theorem proving, mentioned my paper with Dustin Mixon (and maybe also ChatGPT and Lean — should we have further included Marshall Hall?) resolving Problem 707. There are several fun aspects to that story, and I encourage readers to look at Sections 7 and 1 of our paper for more details (or perhaps they may enjoy a summary ). However, the part of the story relevant to formalization is that after the “usual” mathematics was complete, we were able to vibe code the proof in Lean using ChatGPT (without Pro).

While writing the paper, we felt like we were trying a new style of mathematical research: combining large language models with formal verification to produce significant, certifiably correct results. I’m happy to have heard from several friends that our experience motivated them to look into formalizing results in Lean themselves. One mentioned that they hadn’t looked at Lean in three years, and they found that the landscape had changed completely in that time: improvements to Mathlib and Lean, together with the rise of LLMs, made it significantly easier to prove results in a reasonable amount of time. Our experience also motivated Terence Tao to similarly vibe code a solution to Problem 613 by Oleg Pikhurko.

In retrospect, I feel that our paper was written during a very brief window in time when our specific manner of interacting with an LLM and a formal assistant was the most effective manner for a novice to formalize (existing) mathematics. In Section 7 of the paper, we describe what our preferred interaction style would have been using a simple schematic drawing:

This is much closer to reality now. Approximately at the same time as we finished our paper, Harmonic released Aristotle to the general public.

At first, Aristotle could only fill in a sorry in a Lean proof; in other words, given a statement that had already been formalized in Lean, it could (attempt to) supply a proof. This immediately transformed my interactions with Lean. Problem 105 had been recently solved by Wu Xichuan in the forum, and I was able to use ChatGPT to generate formal Lean statements describing the proof, which Aristotle was able to fill in. Before Aristotle, I had tried to formalize this proof with ChatGPT alone, but did not succeed. Note that although Wu’s counterexample is not simple to find, verifying that it works is entirely straightforward. (I was also able to use Aristotle to formalize multiple results from non-Erdős mathematics I was working on. For example, see Section 5.3 of this paper, written in the first person from the perspective of my coauthor Dustin.)

As it turns out, that style of interaction was also a brief moment in time. Shortly thereafter, Aristotle released “informal” mode, which accepts mathematics written in informal language (possibly in LaTeX) and formalizes it all. As a result, Wouter van Doorn, Gemini DeepThink, Terence Tao, Aristotle, and I were able to formalize a solution to part of Problem 367.

I was excited to try using these tools to formalize more solutions. I noticed Problem 418 had recent activity on the forum and that it might be suitable for an experiment. I asked ChatGPT to explain the solution to the problem and then Aristotle to auto-formalize the resulting LaTeX file. The actual theorem statement was already available at the Formal Conjectures projec…