3 ms·
> It would be great if someone could explain to me how AI improves this situation. It's main utility is in the search step, not the verification step. The sea
by jonahx 4mo ago
> It would be great if someone could explain to me how AI improves this situation.
It's main utility is in the search step, not the verification step. The search is the bulk of the work and creativity. Separately, as the sibling commenter pointed out, it will likely get better at the verification step as well, with integrations of tools like Lean.
> One hallucination in 300 steps of logic is enough to destroy the entire proof.
The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired.
- tacomonstrous 4mo ago>The situation with human mathematicians is not much different. Eg, Wiles original proof of Fermat's Last Theorem contained errors found by reviewers, which he later repaired. In fact, it was Wiles himself who realized there was an error.
- jonahx 4mo agoYes, at the prodding of the reviewer (from wikipedia): > After the announcement, Nick Katz was appointed as one of the referees to review Wiles's manuscript. In the course of his review, he asked Wiles a series of clarifying questions that led Wiles to recognise that the proof contained a gap. It seems likely Katz played a crucial role here. Wiles is just a prominent example. In practice, other humans often play this "verification role" for mathematicians, whether via a formal review process or informal discussion.