3 ms·
An AI-generated solution always provides two pieces of info: 1. proof that there is a solution 2. a solution that you can work backwards from to build
by dbmikus 24d ago
An AI-generated solution always provides two pieces of info:
1. proof that there is a solution
2. a solution that you can work backwards from to build understanding
Maybe the solution is pretty inscrutable, but it's almost always better than nothing.
So, both of these pieces of info would be at least marginally useful for advancing human knowledge.
- sashank_1509 24d agoIt demotivates mathematicians. That’s a pretty large negative!
- apetresc 24d agoThat’s a skill issue.
- nullsanity 24d agoNo, it's a motivation issue, can't you read?
- nozzlegear 24d agoWill somebody please let Professor Tao know that he's simply experiencing a skill issue?
- dayjah 24d ago* current mathematicians Were early in this cycle, we will learn to do more, and exercise our new capabilities more fluently, which in turn will create more skilled practitioners Consider the abacus, calculator, computer, etc, each of these enhanced mathematicians’ capabilities and thus outputs.
- XenophileJKO 24d agoThis feels a lot like drafters complaining that nothing will get designed when CAD starts being used.
- evenhash 24d 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.
- pixl97 24d agoI 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.
- bronson 24d agoWhat does "mathematical output of the AI" even mean? A proof? Intermediate tokens?
- __MatrixMan__ 24d agoIt's a Lean program that proves the theorem.
- vikramkr 24d agoNot 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.
- cobbal 24d agoThis is definitely true in an information theory sense: having more knowledge is always better than less knowledge. However, it may not be true in math as a social human endeavor, and having answers without interesting paths to get there may not expand human mathematics in the same way. If Fermat had a book with larger margins, would Weil have devoted so much time to proving the Taniyama-Shimura conjecture? No one can say.