Re:Post-human mathematics
by johncolanduoni on Monday November 23, 2015 @01:13PM
(#10616110)
> If a computer proves the Riemann Hypothesis in such a way that no one can understand it, but it spits out a Coq document that everyone can load and verify, will people consider the problem solved?
We've already seen this play out to a certain degree with the proof of the four color theorem[1]. Basically, the problem was reduced to checking about 2000 specific graphs (the checked property was more complex than simple colorability). The reduction part was very complex but still checked by humans, but checking the ~2000 graphs was a computationally expensive process that took computers thousands of hours to complete, which was completely infeasible for direct human verification. There was a lot of controversy over whether this counted as a proof. Since then the proof has been simplified to 600 special cases and run through a proper proof assistant (Coq), so it is now pretty widely accepted as proved.
It's not quite analogous since the core of the proof was still human created and checked, and the basic form of the computer generated portions was well understood (i.e. the kinds of steps they used). There is some extra doubt involved when this is not the case, since it's possible the computer came up with a novel proof of inconsistency if we don't know at all how the individual parts of the proof work.
We've already seen this play out to a certain degree with the proof of the four color theorem[1]. Basically, the problem was reduced to checking about 2000 specific graphs (the checked property was more complex than simple colorability). The reduction part was very complex but still checked by humans, but checking the ~2000 graphs was a computationally expensive process that took computers thousands of hours to complete, which was completely infeasible for direct human verification. There was a lot of controversy over whether this counted as a proof. Since then the proof has been simplified to 600 special cases and run through a proper proof assistant (Coq), so it is now pretty widely accepted as proved.
It's not quite analogous since the core of the proof was still human created and checked, and the basic form of the computer generated portions was well understood (i.e. the kinds of steps they used). There is some extra doubt involved when this is not the case, since it's possible the computer came up with a novel proof of inconsistency if we don't know at all how the individual parts of the proof work.
[1]: https://en.wikipedia.org/wiki/Four_color_theorem