[FOM] "Mere" correctness of a proof

[Joe Shipman]

As far as I can tell, Connes’s work is formalizable in ZFC+Inacc, which is much weaker than the full Grothendieck Universes axiom. By an obvious metatheorem  any number-theoretic result that follows from the Universes axiom follows from the weaker axiom that there is an inaccessible limit of inaccessibles, but not necessarily from a single inaccessible; however Connes’s “Arithmetic Site” depends only on the notion of Grothendieck topos, which needs only one inaccessible. Many of the properties of Grothendieck topoi can be proven in weak theories, see McLarty’s remarks here:

https://ncatlab.org/nlab/show/Grothendieck+topos

so I think it likely that everything Connes has done is a theorem of ZFC, but whether you can get his “Arithmetic site” framework without needing an inaccessible is a question for McLarty or some other specialist.

— JS

Sent from my iPhone

> On Sep 4, 2018, at 3:22 AM, José Manuel Rodriguez Caballero <josephcmac at gmail.com> wrote:
> 
> 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.
> 
> _______________________________________________
> FOM mailing list
> FOM at cs.nyu.edu
> https://cs.nyu.edu/mailman/listinfo/fom
-------------- next part --------------
An HTML attachment was scrubbed...
URL: </pipermail/fom/attachments/20180904/a1bc728f/attachment.html>