Editing Openai/696202aa-e614-800c-a993-2d8abc734eb7 (section)

=== User: Please, rewrite this historical paragraph about a mathematical finding process more slowly, in form of a true short sto… ===
Please, rewrite this historical paragraph (about a mathematical finding process) more slowly, in form of a true short story, best in simple English.. Ask me, if you are unsure about the meaning of something. -** the story of this proof

While the mathematical and literature contents of the writeup is already complete, this proof has
a significance of being the first recognized Erdos problem (a problem proposed by Paul Erdos
and collected on the Erdos problems website https://www.erdosproblems.com) that was solved
autonomously by an AI system, with no prior literature found as of the date of this writing.
As this is a milestone, it is of interest to ask about the nature of the proof (e.g. how com
plex/novel it is compared to other mathematical results). Unfortunately (or fortunately) the re
sulting proof is in formalized form in Lean. While this boosts confidence in correctness, it may not
be readily digestible.
This writeup attempts to address this issue. The author has received substantial assistance
from ChatGPT in writing this manuscript. Indeed, a large fraction of the words were penned
by ChatGPT. However, the author does not take this to mean we compromise on correctness; in
contrast, everything has been manually checked up to roughly the level that the author himself
would be confident in were he to write it himself and send it off as a journal submission! Of course,
mistakes are still possible and any correction is welcome.
It is of interest to record the story of this proof as follows. The “raw” story may be read in the
Erdos problems website thread: https://www.erdosproblems.com/728.
On Jan 4, 2026, Kevin Barreto announced that he has a proof from the AI system: Aristotle
by Harmonic. This is a Lean system, and the input to Aristotle is based on an informal argument
from GPT-5.2 Pro. However there is one nuance here: at that time, the problem as stated on the
website is vague, with the intended interpretation from Erdos unclear. Barreto’s version resolves
one version of the problem, but it wasn’t clear whether this is the intended version.
Afterwards, forum participants commented on this vagueness; a consensus then emerged that
this should be regarded as a partial result, which does not yet fully resolve the problem.
But- on Jan 5, 2026, Barreto again asked GPT-5.2 Pro whether its argument can be upgraded
to tackle the version that forum participants had now identified as the problem. GPT-5.2 Pro
responded in affirmative; Aristotle was then run based on this latest response and produced a
formal proof on Jan 6, 2026.
There was a misunderstanding around this time that this second output had been based on
a human’s mathematical observation, which would render the result not autonomous by the AIs
involved. Nevertheless, Barreto has clarified that this was a misunderstanding and a human obser
vation was not provided in order to reach this result. With autonomy confirmed, the problem was
now understood to be fully resolved by AI.
In particular, Terence Tao has vouched for this autonomous status which helped in cementing
the consensus.
Afterwards, a forum participant who goes by KoishiChan attempted a literature review to locate
any prior literature resolving this problem. KoishiChan has been highly successful in locating prior
literature in the past for problems claimed to be solved by AI; however this time around an existing
11
literature resolving this problem was not found. It is of course possible that such literature exists,
as it is impossible to disprove the possibility, but we have not found such literature as of the date
of this writing. Thus, the current status is that Erdos Problem 728 was fully resolved autonomously
by AI with no prior human literature resolving the problem found.
On Jan 6, 2026, Boris Alexeev ran Aristotle again on the Aristotle proof in order to simplify it,
producing a new proof. This is the Lean proof in [1] which this present writeup is based on.
The author has then worked with ChatGPT in order to extract a human-readable proof from
[1] to make it accessible to a wider audience. Later, the presentation was iteratively improved and
relevant literature included in order to make it a fuller presentation with maximum value to the
mathematical community; this is the present writeup.
For reference, the conversation with ChatGPT that the author collaborates with in producing
this writeup can be accessed here1. Note that while there are many drafts there, none of them is
the current writeup, in which the author further applies significant rewrites in various places by
himself-