mersenneforum.org > Math Official Computerized Proving thread
 Register FAQ Search Today's Posts Mark Forums Read

2019-09-27, 19:39   #1
ewmayer
2ω=0

Sep 2002
República de California

22×32×17×19 Posts

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

2019-09-27, 19:51   #2
chalsall
If I May

"Chris Halsall"
Sep 2002

22·2,393 Posts

Quote:
 Originally Posted by ewmayer 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. (?)

2019-09-28, 02:00   #3
LaurV
Romulan Interpreter

Jun 2011
Thailand

223408 Posts

Quote:
 Originally Posted by chalsall 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).

 2019-09-28, 07:28 #4 Nick     Dec 2012 The Netherlands 110100010012 Posts 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!
 2019-09-29, 09:25 #5 jwaltos     Apr 2012 Brady 2·33·7 Posts 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..
 2019-09-29, 10:00 #6 ATH Einyen     Dec 2003 Denmark 23×17×23 Posts 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
2019-09-29, 13:54   #7
CRGreathouse

Aug 2006

10111011000012 Posts

Quote:
 Originally Posted by ATH 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.

 2019-09-29, 19:55 #8 jwaltos     Apr 2012 Brady 2×33×7 Posts "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
 2019-10-01, 05:06 #9 jwaltos     Apr 2012 Brady 2·33·7 Posts 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.

 Similar Threads Thread Thread Starter Forum Replies Last Post ewmayer Hardware 42 2020-07-31 13:55 ewmayer Programming 31 2016-10-14 05:49 Prime95 Lounge 32 2015-10-02 04:17 Flatlander Lounge 29 2013-01-12 19:29 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