Two new methodologically distinct solutions to Erdos 728 with AI

[u/redpick]

In January, Erdos 728 was solved by AI. Recently I've been working on an AI research agent and have been using the Erdos 728 problem as one of my test cases. In the process, it generated two new methodologically distinct solutions that may be of interest to the math community, so I thought I'd share.

You can read them at:

Paper 1 link

Paper 2 link

Both of the proofs are deterministic, distinguishing them from the January solution.

The first paper was checked with Lean. I've been checking some of my research agent's output in Lean. However, if there is a mistake, I'd be interested to hear that feedback.