tag:blogger.com,1999:blog-10112790.post8609119806641245958..comments2014-05-30T17:34:37.599-04:00Comments on Scientific Clearing House: Formal ProofCarson C. Chowhttp://www.blogger.com/profile/08464737817585277975noreply@blogger.comBlogger8125tag:blogger.com,1999:blog-10112790.post-19870836590560657472008-11-30T14:52:00.000-05:002008-11-30T14:52:00.000-05:00Absolutely, thanks for the comment.Absolutely, thanks for the comment.Carson C. Chowhttps://www.blogger.com/profile/08464737817585277975noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-84985420864960516732008-11-27T17:55:00.000-05:002008-11-27T17:55:00.000-05:00> HOL Light differs slightly from the Zermelo-F...> HOL Light differs slightly from the Zermelo-Fraenkel-Choice axioms of set theory used in traditional mathematics. <BR/><BR/><BR/>Note that there are other proof assistants, like Mizar and Isabelle/ZF that implement ZF set theory, so it is possible to do formalized mathematics in the traditional setting as well.slawekkhttp://slawekk.wordpress.com/noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-20250465729596313282008-11-26T17:59:00.000-05:002008-11-26T17:59:00.000-05:00Hi Steve,No, Fejes Tóth was not Tom's advisor. T...Hi Steve,<BR/><BR/>No, Fejes Tóth was not Tom's advisor. Tom's advisor was actually Langlands and until Kepler, Tom did representation theory.<BR/><BR/>Yes, essentially, it reduces to a manageable optimization problem.Carson C. Chowhttps://www.blogger.com/profile/08464737817585277975noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-68277523988964908092008-11-24T23:30:00.000-05:002008-11-24T23:30:00.000-05:00L. Fejes TóthThus it seems that the problem can be...L. Fejes Tóth<BR/><BR/>Thus it seems that the problem can be reduced to the determination of the minimum of a function of a finite number of variables, providing a programme realizable in principle. In view of the intricacy of this function we are far from attempting to determine the exact minimum. But, mindful of the rapid development of our computers, it is imaginable that the minimum may be approximated with great exactitude. <BR/><BR/>Was Fejes Toth Tom's advisor?<b>Steve Hsu</b>https://www.blogger.com/profile/02428333897272913660noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-42847034041809688512008-11-24T11:51:00.000-05:002008-11-24T11:51:00.000-05:00Hi Steve,It is a lot more subtle obviously. The b...Hi Steve,<BR/><BR/>It is a lot more subtle obviously. The bottom line as you surmised is that there are only a finite number of things to check. However, as I recall how Tom explained it to me (which was quite awhile ago), I think it does boil down to the fact that you only need to check a finite number of arrangements. The real trick was that you can use linear programming to do the test, which is why it was tractable. If you are out there Tom, is this right?<BR/><BR/>ccCarson C. Chowhttps://www.blogger.com/profile/08464737817585277975noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-45421888479028437072008-11-24T10:29:00.000-05:002008-11-24T10:29:00.000-05:00"strategy for the proof was to show that all possi..."strategy for the proof was to show that all possible packings in infinite space could be reduced to a finite number of arrangements"<BR/><BR/>Is that really true, or is it more subtle how the seemingly infinite set of configurations is reduced to a finite set of things to check?<b>Steve Hsu</b>https://www.blogger.com/profile/02428333897272913660noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-28790734951686382102008-11-23T10:47:00.000-05:002008-11-23T10:47:00.000-05:00Hi Artur,Hilbert's program is partially dead. Whil...Hi Artur,<BR/><BR/>Hilbert's program is partially dead. While you can fully verify a proof, you still cannot decide if some conjecture is provable. Goedel's first incompleteness theorem says that there will remain statements that are true but not provable.<BR/><BR/>I wouldn't call a theorem a fixed point because the system is not really a dynamical system. Moves are never forced. A conclusion is just another term, which can then be operated on or not. It's more like building with lego. At any point you can attach a piece. A proof is then showing that you can build a certain structure starting from another just using the pieces you have.<BR/><BR/>All proofs are in NP because they can be verified in polynomial time. Theorem proving is NP complete because it can be reduced to SAT. Your question is more one of implementation rather than complexity. The latter merely asserts the asymptotic properties of the algorithm while the former looks for best algorithms. Actually, even if P=NP you still might not be able to prove all theorems right away. Some algorithms might go like N^10000000, which is only better than exp(N) for N really really big. However, if P=NP it does mean that it is just a matter of time before all theorems are proved. If P not equal NP, then some theorems may be intractable.Carson C. Chowhttps://www.blogger.com/profile/08464737817585277975noreply@blogger.comtag:blogger.com,1999:blog-10112790.post-77971838540003959132008-11-23T00:02:00.000-05:002008-11-23T00:02:00.000-05:00Neat. I guess Hilbert's program is not completely ...Neat. I guess Hilbert's program is not completely dead yet!<BR/><BR/>So, in this dynamical system language, does the conclusion correspond to a fixed point? If so, in light of Goedel's theorem, does that mean that not all theorems have fixed points (computability)? Does it also mean that NP-completeness can be quantified in terms of the time to reach the fixed point (complexity)?Artur Adibhttps://www.blogger.com/profile/10629623314718069247noreply@blogger.com