Solving 20 Erdős Problems with 20 Codex Accounts Running in Parallel

Re:Solving 20 Erdős Problems with 20 Codex Accounts Running ... by zitterbewegung on Tuesday July 14, 2026 @11:22PM (#48915871)

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/

[ Parent | on HN ]

Re:Solving 20 Erdős Problems with 20 Codex Accounts Running ... by colin7snyder on Wednesday July 15, 2026 @01:47AM (#48916711)

I haven't played around with Aristotle at all, thanks for bringing it up & (also your codebase, thesisus, is very solid!)

[ Parent | on HN ]

Re:Solving 20 Erdős Problems with 20 Codex Accounts Running ... by universa1 on Wednesday July 15, 2026 @04:15AM (#48917733)

This looks interesting. I am not really familiar with lean, etc... Could I use this to formalize/verify a proof from a paper?

[ Parent | on HN ]

Re:Solving 20 Erdős Problems with 20 Codex Accounts Running ... by trenchgun on Wednesday July 15, 2026 @10:28AM (#48921396)

Yes, assuming the stuff it depends on is already formalized.

[ Parent | on HN ]

Re:Solving 20 Erdős Problems with 20 Codex Accounts Running ... by zitterbewegung on Wednesday July 15, 2026 @12:41PM (#48923518)

With Aristotle you could formalize a proof from only the text of a paper.

[ Parent | on HN ]