3 ms·
There are some parallels here to AI coding where even if the AI can write all the code, it's still valuable to have a human who can read and understand the code
by amurthy1 2mo ago
There are some parallels here to AI coding where even if the AI can write all the code, it's still valuable to have a human who can read and understand the code to verify correctness. The same is true of AI generated math proofs that humans will want to verify are around before they feed them back into the AI and build new insights.
- traes 2mo agoProof verification can be done automatically via Lean (or similar), so the parallel breaks down unfortunately. The only thing humans really need to verify is the translation of the theorem statement and the correctness of the proof checker.
- jgwil2 2mo agoThe purpose of having a human look at LLM output is not just to verify correctness but also to understand a system. The parallel to math is that the value of a proof is not just the verification of a statement but also the working out of the mathematics required to establish that truth.