Can't you kind of think of them as a genetic algorithm that has a very good hypothesis generator? Humans could, in principle, help guide that (already very impressive) hypothesis generator to make better guesses to find the proof more easily.

Conversations with an ChatGPT with Terence Tao at the helm are a thing of beauty. An advanced practitioner prompting things beyond my understanding. Jarred Sumner's paper on the Riemann Hypothesis, however, was not that. No slight against him, but Jarred was a non-mathematician, and his prompting to improve the minimum fraction of zeta zeros by Claude amounted to "keep going" and "believe in yourself". Shit, anyone coulda done that in his position.

https://www.anthropic.com/research/riemann-zeta

My point is that it does matter who's driving the AI but it also matters the route. Just like F1 champion Max Verstappen is a ridiculously better driver than me at driving an F1 car around a track, if we're just driving a friend to the airport, it doesn't really matter if it's Max or me driving, so long as we don't crash.

>> If they were really stupid, a Prolog program, a genetic algorithm or a SAT solver would be enough to reach the goal. Clearly it was not the case.

"Clearly" as in "somebody tried that and failed" or "clearly" as in nobody ever thought to try it and now nobody will because there's no point?