20190927, 19:39  #1  
∂^{2}ω=0
Sep 2002
República de California
2^{2}×3^{2}×17×19 Posts 
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:
Last fiddled with by ewmayer on 20190927 at 19:40 

20190927, 19:51  #2  
If I May
"Chris Halsall"
Sep 2002
Barbados
2^{2}·2,393 Posts 
Quote:
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. (?) 

20190928, 02:00  #3  
Romulan Interpreter
Jun 2011
Thailand
22340_{8} Posts 
Quote:
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). 

20190928, 07:28  #4 
Dec 2012
The Netherlands
11010001001_{2} Posts 
Here's an introduction from about 5 years ago for anyone new to the issues:
https://www.gresham.ac.uk/lecturesa...proofbyhuman 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! 
20190929, 09:25  #5 
Apr 2012
Brady
2·3^{3}·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 20190929 at 09:49 Reason: ..good old Jean.. 
20190929, 10:00  #6 
Einyen
Dec 2003
Denmark
2^{3}×17×23 Posts 
If they really want to test the software they should try it on Interuniversal 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 20190929 at 10:01 
20190929, 13:54  #7 
Aug 2006
1011101100001_{2} Posts 
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.

20190929, 19:55  #8 
Apr 2012
Brady
2×3^{3}×7 Posts 
"Hardware changes with the times, but bestinclass algorithms are eternal."
Source:(https://www.quantamagazine.org/mathe...iply20190411/), 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 "selfaware." 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 20190929 at 20:22 
20191001, 05:06  #9 
Apr 2012
Brady
2·3^{3}·7 Posts 
Here are a couple of links that may be of interest:
https://theoremprovermuseum.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. 
Thread Tools  
Similar Threads  
Thread  Thread Starter  Forum  Replies  Last Post 
Official ARM manycore/server thread  ewmayer  Hardware  42  20200731 13:55 
Official AVX512 programming thread  ewmayer  Programming  31  20161014 05:49 
Official Peeved Pets Thread  Prime95  Lounge  32  20151002 04:17 
Official 'Let's move the hyphen!' thread.  Flatlander  Lounge  29  20130112 19:29 
Official Odd Perfect Number thread  ewmayer  Math  14  20081023 13:43 