On Thu, Feb 20, 2014 at 9:31 AM, Bruno Marchal <marc...@ulb.ac.be> wrote:
> > On 19 Feb 2014, at 19:13, Telmo Menezes wrote: > > "If no human can check a proof of a theorem, does it really count as > mathematics? That's the intriguing question raised by the latest > computer-assisted proof. It is as large as the entire content of Wikipedia, > making it unlikely that will ever be checked by a human being." > > > http://www.newscientist.com/article/dn25068-wikipediasize-maths-proof-too-big-for-humans-to-check.html#.UwTytEJdV69 > > This reminded me of something that Bruno mentions frequently: the idea of > deriving physics from the natural numbers, addition and multiplication. > Should we expect wikipedia-size proofs (or worse)? > > > Hi Bruno, > Er well, people seems not quite aware of this, but the physics has already > been derived, and it would take 50 pages, when done starting from zero, but > it is shortened a lot by using Solovay's completeness theorems (on G and > G*). > > Of course, the physics obtained might seem a bit abstract, and it remains > many open problems. But the equation are there, and it remains only > mathematical problems to solve. > > It would be astonishing that the first interview of the machine gives the > correct physics, but up to now, it fits, and this at a place where many > logicians predicted it would be miraculous that it would not be > contradicted immediately. > I have to admit, I think I follow the main ideas you've been explaining on the mailing list, but here you just sound mysterious... Have you published any of this? > That's why they push me to publish and do a PhD thesis. > Of course, comp can be false, and this might only be a bad lucky > coincidence. This we can always say for any theory. > > I am actually explaining to Liz and others, how the physics is extracted > (UDA explains already how physics needs to be redefine, and AUDA just do > the math of that redefinition). I have to explain a bit of modal logic > before, just to be able to give the enunciation of Solovay theorems. > Ok, I've been silently following your modal logical class as time permits. Thanks for that, by the way! Telmo. > > Best, > > Bruno > > > > Cheers, > Telmo. > > -- > You received this message because you are subscribed to the Google Groups > "Everything List" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to everything-list+unsubscr...@googlegroups.com. > To post to this group, send email to everything-list@googlegroups.com. > Visit this group at http://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/groups/opt_out. > > > http://iridia.ulb.ac.be/~marchal/ > > > > -- > You received this message because you are subscribed to the Google Groups > "Everything List" group. > To unsubscribe from this group and stop receiving emails from it, send an > email to everything-list+unsubscr...@googlegroups.com. > To post to this group, send email to everything-list@googlegroups.com. > Visit this group at http://groups.google.com/group/everything-list. > For more options, visit https://groups.google.com/groups/opt_out. > -- You received this message because you are subscribed to the Google Groups "Everything List" group. To unsubscribe from this group and stop receiving emails from it, send an email to everything-list+unsubscr...@googlegroups.com. To post to this group, send email to everything-list@googlegroups.com. Visit this group at http://groups.google.com/group/everything-list. For more options, visit https://groups.google.com/groups/opt_out.
