Every time I see a story about an LLM proving an important open conjecture, I think “it’s going to turn out that the LLM did not prove an important open conjecture” and so far I have always been somewhat vindicated for one or more of the following reasons:
1: The LLM actually just wrote code to enumerate some cases / improve some bound (!)
2: The (expert) human spent enough time iterating with the LLM that it is not clear the LLM was driving the proof.
3: The result was actually not novel (sometimes the human already knew how to do it and just wanted to test the LLM out on filling in details), or the result is immediately improved or proven independently by humans, which seems suspicious.
Every time I see a story about an LLM proving an important open conjecture, I think “it’s going to turn out that the LLM did not prove an important open conjecture” and so far I have always been somewhat vindicated for one or more of the following reasons:
1: The LLM actually just wrote code to enumerate some cases / improve some bound (!)
2: The (expert) human spent enough time iterating with the LLM that it is not clear the LLM was driving the proof.
3: The result was actually not novel (sometimes the human already knew how to do it and just wanted to test the LLM out on filling in details), or the result is immediately improved or proven independently by humans, which seems suspicious.
4: No one seems to care about the result.
In this case 2 and 3 apply.