I've run this harness in GPT 5.6-Sol Pro for 679 minutes total (11 hours, 19 minutes)
A few failures, and two discoveries. One was a very niche problem that had like a few papers on it (it improved the bound)
Then I re-prompted it, to only consider problems that at least have a dedicated Wikipedia page.
It autonomously scans, use the theorem prover it wrote in C++, reads the relevant papers, and boom. New record.
Full convo: https://chatgpt.com/share/6a6c9582-2a58-83ee-8123-c9a90a7657b0
Back-story: In Ray Kurzweil's new book, there was a section about earliest theorem provers, starting in 1955 The Logic Theorist and GPS: General Problem Solver, so I thought it would be a fun experiment to ask ChatGPT Pro to reimplement it, and optimize all hot-paths... honestly, maybe it could have done it without it, basically it can do C++ on the web... bruh where are we heading?