Comment by evenhash
12 hours ago
> An AI-generated solution always provides ... proof that there is a solution
This is only true in the most trivial sense. A solution is a solution, sure... but how do you know it's a solution, and not an incoherent jumble of words? A human has to review and vouch for it.
Just because the AI gives you an arxiv-worthy PDF, or a Lean proof which compiles, doesn't mean it proves what the AI says it does. The AI could give you the same PDF/Lean code and says it proves the opposite, how would anyone know the difference?
You can't advance human understanding unless you produce things that humans can understand.
Not an expert by any means but the assumption here as I understand it is that the arxiv worthy PDF would not be acceptable or meaningful for impossible to understand proofs. And the lean proof would be meaningless unless the specific expression being proven is human understandable as the direct translation of the question the human is asking in formal form. So proving the negation is not a thing but if you make a subtle mistake in translating the statement you want to prove then obviously the QI is going to be proving the wrong thing. And otherwise you're relying on the correctness of lean as a system and on identifying/preventing if the proof is adversarially exploiting bugs in lean to falsely prove things.
> Just because the AI gives you an arxiv-worthy PDF, or a Lean proof which compiles, doesn't mean it proves what the AI says it does. The AI could give you the same PDF/Lean code and says it proves the opposite, how would anyone know the difference?
> You can't advance human understanding unless you produce things that humans can understand.
And you can't advance human understating unless you maintain that understanding.
I can see a version of the junior software engineer problem here: AI wrecks the problems that could train and motivate the next generation mathematicians, so students abandon the field because there's no place for them. The senior mathematicians who can review/vouch/prompt for AI output like Tao retire and die. Then there's no more math that anyone can understand and no more open problems for it to solve.
And that's probably happening already. I've read articles about AI performing the journeyman work that mathematicians cut their teeth on, rendering years of work obsolete, and derailing the careers that work was meant to start.
That was exactly my thought - taking out the problems that PhDs and early stage researchers work on kills the pipeline of developing mathematicians
That's why the solution should be presented in a verifiable formal language, such as Lean. Which is the case with the Navier-Stokes problem.
I might be wrong, but making an assumption that you could learn to read the mathematical output of the AI long before you could write a solution yourself. But hey, what do I know, I'm not a mathemagition.
What does "mathematical output of the AI" even mean? A proof? Intermediate tokens?
It's a Lean program that proves the theorem.