Solving Erdős Problem 123 with Lean 4 Formal Verification
Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel
We solved Erdős Problem 123 by proving that every large integer is a sum of distinct terms from pairwise-coprime bases, ensuring no term divides another. Our breakthrough involved a novel 'optional interior shell' construction to overcome previous induction limits. The entire proof is rigorously formalized in Lean 4 using Mathlib, confirming the result without any placeholders.
The important lesson was that large additive width is not enough; the lower endpoint has to remain under quantitative control.
- vessenes
Very interesting, on many levels: first, the raw additional compute / search harness is worth reading about; huge numbers of Lean 4 theorems, thousands of vCPUs available for spreading out search, embedding databases of proofs, all very interesting.
Second, the proofs -- I understand the Lean 4 proofs to be refereed by Fable, and generated by Chat 5.6 Sol. Unlike the leaked proof of the Cycle Double Cover Conjecture last week which had a very nicely readable nearly humanlike writeup, the proof summaries (from Fable) read like Claude tends to read to me these days - real difficulty with the theory of mind of the reader, they are filled with technical phrases, acknowledgment of hard bits and oblique reference to solutions. In short, they suck. I didn't see the word load-bearing, but I bet it's there.
That said, a Lean 4 proof is a pretty compelling output artifact. I find it interesting that it's an additional type of effort to turn these into human readable / appreciable / beautiful / non-shitty proofs.
To those who say who cares -- indeed. But. One of the major reasons things like the Erdos problems are valuable is that they can at times spur new techniques and concepts. The best of these concepts are applied elsewhere, advancing the frontier. While we gain a lot from solving these problems, we'll gain even more from that next step of distillation / explanation into something humans and computers can grok together. I'd hope that with so many tentatively marked 'solved' we wil […]
- fractorial
My mouth is agape at the fact that this project
is basically what I have been working on non-stop
for the last three weeks and just yesterday gotten
to the point of evaluating; hats off... I only have
one novel proof (non-Erdos) and 13 first-time
formalizations thus far.
I still like doing maths by pen and paper, but
this is fun too.
- zitterbewegung
I was studying Erdos problems by only taking ChatGPT 5.5 outputs and just asking it to keep on attempting to solve it by asking it to go further. I haven't started doing this with chatgpt 5.6 I have some partial results here https://chatgpt.com/g/g-p-69f03400f420819192418b18ca90ffee-d...
What was really interesting is that during the process it was able to find lemmas or theorems that might be related or relevant to be published.
While I was doing that I was also trying to use Aristotle to do the Lean formalization and I have a WIP system to do that at https://github.com/aconsapart/thesisus/
- orlandpm
Who is funding this? Sounds like a fun experiment but that’s a huge amount of compute if I understand correctly.
- gravypod
What kind of harness does the exploration? Where did the corpus of Lean proofs come from? Is the code backing Ton 618 open source?
- toomuchtodo
Exceptional work. Reminds me of https://www.distributed.net/Main_Page | https://boinc.berkeley.edu/ | https://en.wikipedia.org/wiki/EFF_DES_cracker. Consider scaling up by distributing this work more broadly. "Many hands make light work." Lots of problems remaining to solve.
- zingar
I feel like I'm seeing a maths+AI change from "let's test the limits of LLMs by seeing if they can do useful math" to "LLMs can do useful math, now let's solve lots of problems!", or put a different way the goal has shifted from "interesting exercise for AI" to "making a big difference in math". Am I correct?
Are there practical applications of any these problems being solved? No judgement implied, I'm well aware that "no" only means "not yet".
- aureianimus
Very cool! It seems you've got a great setup. An addition that would be very convincing is going the extra mile and making a comparator setup for your Lean proofs. (https://github.com/leanprover/comparator) This ensures that the AI is not, in any way, modifiying the Lean context in ways that could lead to unsoundness.