Official Computerized Proving thread

ewmayer · 2019-09-27, 19:39

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.

chalsall · 2019-09-27, 19:51

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. (?)

LaurV · 2019-09-28, 02:00

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).

Nick · 2019-09-28, 07:28

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!

jwaltos · 2019-09-29, 09:25

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

ATH · 2019-09-29, 10:00

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.

CRGreathouse · 2019-09-29, 13:54

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.

jwaltos · 2019-09-29, 19:55

"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.

jwaltos · 2019-10-01, 05:06

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.

2019-09-29, 09:25	#5
jwaltos Apr 2012 Brady 2⁷×3 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 110001010111₂ 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, 19:55	#8
jwaltos Apr 2012 Brady 2⁷×3 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

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

2019-09-28, 07:28	#4
Nick Dec 2012 The Netherlands 2×23×37 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-10-01, 05:06	#9
jwaltos Apr 2012 Brady 2⁷×3 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.