Formalization of Erdős Problems

Summary

[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 fir…