Also, even GPT-3 (6 years ago) was a very powerful search tool for exactly these kinds of problems. You needed some result that would give a bound on some obscure property, and it instantly gave you five different applicable theorems from three different domains of math. Usually, the theorems even existed.

I was taken aback by the progress in 2025/2026 because late 2024 did seem to be a plateau, but 5-10 years seemed inevitable.

Even when I first studied automated theorem provers in around 2013, the 10-20 years to automating proofs (not theory building) seemed inevitable. They were already superhumanly fast and generating real results, and neural networks were making massive progress on translation, image processing, and games. Someone just had to work out how to stick a neural net inside an ATP. The surprise was that it happened the other way around, and that it solved even more than just mathematical proofs.

AI has only just begun to expose the depth of willful human ignorance.

> late 2024 did seem to be a plateau

Why? o1 was released in late 2024