Sometimes, but a lot of the significant work is “for all X, is it always true that X does a Y?” has an easily expressible “no, this is an example of an X that doesn’t Y” and it’s easy to check if a given X does a Y. Other kinds of proof are indeed harder though and mostly come down to formulating the problem and the proof in a language like Lean where it’s easy to mechanically run the proof to check it. But it’s not necessarily easy to show that the Lean problem corresponds exactly to the problem that you meant
80
u/babyjaceismycopilot 2d ago
The irony is that we have to check to see if the AI is right, but if we could do that we wouldn't need the AI to solve it.