[FOM] "Mere" correctness of a proof

[José Manuel Rodriguez Caballero]

David Fernandez Breton wrote:
> Although correctness in mathematics is not negotiable, and it
> constitutes a "sine qua non" of mathematical practice, I believe (and
> I'm sure others will agree) that correctness, by itself, is worth very
> little, if it's not accompanied by some aesthetic appeal and sense of
> understanding. A proof of the RH [Riemann hypothesis] of which we do not
understand anything,
> other than the fact that it is correct (as witnessed by some
> computerized proof checker) will probably not be very valuable (cf. the
> proof of the four colour theorem).

The previous reasons given by Tim and myself were rather sociological and
focused on the impact of such a proof in the mathematical community. The
following reason will be more theoretical: to have a proof of the Riemann
hypothesis, even if it is unintelligible, e.g., generated by an artificial
intelligence connected to a proof assistant, will show that Riemann
hypothesis can be proved in the type theory of the proof assistant. Indeed,
from today knowledge, nothing prevent that someday, someone will provide a
proof that the Riemann hypothesis is independent of ZFC axioms. There is a
debate about this possibility:
https://www.reddit.com/r/math/comments/1rinve/is_it_possible_for_the_riemann_hypothesis_to_be/

An interesting problem is the following: Suppose that the Riemann
hypothesis is undecidable in ZFC. Does this fact imply that the Riemann
hypothesis is undecidable in the Arithmetic Site?

References concerning the Arithmetic Site:
Paper: http://www.alainconnes.org/docs/geomarithmeticsite.pdf
Video: https://www.youtube.com/watch?v=FaGXxXuRhBI&t=1772s

Kind Regards,
Jose M.
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180904/54afa0b7/attachment.html>