mersenneforum.org  

Go Back   mersenneforum.org > Great Internet Mersenne Prime Search > Math

Reply
 
Thread Tools
Old 2019-09-27, 19:39   #1
ewmayer
2ω=0
 
ewmayer's Avatar
 
Sep 2002
República de California

22×32×17×19 Posts
Default Official Computerized Proving thread

OK, Vice's headline here is a bit clickbaity, more accurate would be "fears much recently published math is wrong":

Number Theorist Fears All Published Math Is Wrong - Vice.com
Quote:
Kevin Buzzard, a number theorist and professor of pure mathematics at Imperial College London, believes that it is time to create a new area of mathematics dedicated to the computerization of proofs. The greatest proofs have become so complex that practically no human on earth can understand all of their details, let alone verify them. He fears that many proofs widely considered to be true are wrong. Help is needed.

Last fiddled with by ewmayer on 2019-09-27 at 19:40
ewmayer is online now   Reply With Quote
Old 2019-09-27, 19:51   #2
chalsall
If I May
 
chalsall's Avatar
 
"Chris Halsall"
Sep 2002
Barbados

22·2,393 Posts
Default

Quote:
Originally Posted by ewmayer View Post
OK, Vice's headline here is a bit clickbaity, more accurate would be "fears much recently published math is wrong"
I don't understand the maths to the level that most of you guys do, but even this head-line managed to reach me through my usual news-feeds.

If I understand what this is saying correctly, it means that some legitimate proofs involve a great deal of compute.

Beautiful proofs are simple and obvious, written by gods on the back of napkins.

For us stupid humans, sometimes we need a large amount of deterministic help in seeing the light. (?)
chalsall is online now   Reply With Quote
Old 2019-09-28, 02:00   #3
LaurV
Romulan Interpreter
 
LaurV's Avatar
 
Jun 2011
Thailand

223408 Posts
Default

Quote:
Originally Posted by chalsall View Post
For us stupid humans, sometimes we need a large amount of deterministic help in seeing the light. (?)
Yeah, help comes in two flavors, is either someone in front of you guiding your hand/steps, or somebody behind, kicking your butt...

Important is to get out of the tunnel.

Then what?

You find yourself in a larger, longer, better lit, but still dark, another tunnel...

Then while(1).
LaurV is offline   Reply With Quote
Old 2019-09-28, 07:28   #4
Nick
 
Nick's Avatar
 
Dec 2012
The Netherlands

110100010012 Posts
Default

Here's an introduction from about 5 years ago for anyone new to the issues:
https://www.gresham.ac.uk/lectures-a...proof-by-human

It's also worth being aware that the press has a history of sensational and inaccurate reporting in this area.
Let's try and avoid that here!
Nick is offline   Reply With Quote
Old 2019-09-29, 09:25   #5
jwaltos
 
jwaltos's Avatar
 
Apr 2012
Brady

2·33·7 Posts
Default

In the mid 90's the Robbins conjecture was proven with EQP [see also Prover9]. A little earlier I was learning about theorem provers like nqthm but it was not easy. ACL2 is a system I had mentioned before within this forum and is worth a look. I posted a link to "Pluribus" which also is worth a look regarding interesting AI. The other piece for this trifecta is a working quantum computational basis. It's one thing to try to prove some lemmas and theorems and it's quite another to come up with questions that have never been asked before and attempt to prove their validity. I can follow a well commented program in more than a few different computer languages but damned if I can follow Wile's proof and others without plowing through several associated texts and reams of refereed papers.

Doron Zeilberger developed a method of telescopic combinatorial proofs and I think he has written some simple geometry provers as well. Statistical theorem proving has its niche also.


"A proof is a proof. What kind of a proof? It's a proof. A proof is a proof. And when you have a good proof, it's because it's proven."

Jean Chretien

Last fiddled with by jwaltos on 2019-09-29 at 09:49 Reason: ..good old Jean..
jwaltos is offline   Reply With Quote
Old 2019-09-29, 10:00   #6
ATH
Einyen
 
ATH's Avatar
 
Dec 2003
Denmark

23×17×23 Posts
Default

If they really want to test the software they should try it on Inter-universal Teichmüller theory which only a few people in the world claim to maybe understand.

It is needed to check the claimed proof of the abc conjecture.

I doubt the software is so advanced they can code in a theory they barely understand.

Last fiddled with by ATH on 2019-09-29 at 10:01
ATH is offline   Reply With Quote
Old 2019-09-29, 13:54   #7
CRGreathouse
 
CRGreathouse's Avatar
 
Aug 2006

10111011000012 Posts
Default

Quote:
Originally Posted by ATH View Post
I doubt the software is so advanced they can code in a theory they barely understand.
Of course not. But the real difficulty is that you need to code the entire field up to that point, so anything high up in the clouds like that stands no chance. It would take a monumental effort over decades, probably, to code everything up to that lofty level. Actually, by the time we get there, the proof will probably be understood (and known to be right or wrong) so it can be coded if appropriate.
CRGreathouse is offline   Reply With Quote
Old 2019-09-29, 19:55   #8
jwaltos
 
jwaltos's Avatar
 
Apr 2012
Brady

2×33×7 Posts
Default

"Hardware changes with the times, but best-in-class algorithms are eternal."

Source:(https://www.quantamagazine.org/mathe...iply-20190411/), last paragraph.

Following some of the links I came across wording where certain mathematical statements needed to be "translated" into other statements in order for certain results to exist. Dyson's work as well as that of Mikusinski show such "translation" explicitly. For me, proof means logical consistency but that does not mean this logic is complete. In my opinion, a "reasoning language" is only as useful as it is "self-aware." And the ability to perceive and distinguish is crucial...expressed in the ability to recognize when you're wrong and the humility to say you're sorry for wasting everyone's time.

Although the word "computerized" within the title of this thread seems a bit archaic to me, the logic employed by the computers [provers] seem to be computing forms of logic relative to their containers [Boolean systems..]. When a logical "system" is able to rewrite it's physical structure and evolve into "smarter" logic and "better designed" physical presence then that for me is a proof of concept of a good logical design.

Enriching the design of a proving system with the added feature of "intuition" would be interesting. Relative to the quote within the original post, the authors "beliefs and fears" could be intuited on a tangible basis.

Last fiddled with by jwaltos on 2019-09-29 at 20:22
jwaltos is offline   Reply With Quote
Old 2019-10-01, 05:06   #9
jwaltos
 
jwaltos's Avatar
 
Apr 2012
Brady

2·33·7 Posts
Default

Here are a couple of links that may be of interest:

https://theoremprover-museum.github.io/

https://en.wikipedia.org/wiki/AMPL#t...20Laboratories.


The second link can be used as an extension and/or a sandbox to theorem provers. I had used AMPL in the late 90's and found it useful. GAMS is another such system..just note that the word has alternative meanings.
jwaltos is offline   Reply With Quote
Reply

Thread Tools


Similar Threads
Thread Thread Starter Forum Replies Last Post
Official ARM manycore/server thread ewmayer Hardware 42 2020-07-31 13:55
Official AVX-512 programming thread ewmayer Programming 31 2016-10-14 05:49
Official Peeved Pets Thread Prime95 Lounge 32 2015-10-02 04:17
Official 'Let's move the hyphen!' thread. Flatlander Lounge 29 2013-01-12 19:29
Official Odd Perfect Number thread ewmayer Math 14 2008-10-23 13:43

All times are UTC. The time now is 23:10.

Sun May 9 23:10:17 UTC 2021 up 31 days, 17:51, 0 users, load averages: 1.94, 2.33, 2.48

Powered by vBulletin® Version 3.8.11
Copyright ©2000 - 2021, Jelsoft Enterprises Ltd.

This forum has received and complied with 0 (zero) government requests for information.

Permission is granted to copy, distribute and/or modify this document under the terms of the GNU Free Documentation License, Version 1.2 or any later version published by the Free Software Foundation.
A copy of the license is included in the FAQ.