tag:blogger.com,1999:blog-27705661.post5075921298711934456..comments2021-11-21T12:00:56.420+00:00Comments on Process Algebra Diary: Desperately Seeking Mathematical TruthLuca Acetohttp://www.blogger.com/profile/01092671728833265127noreply@blogger.comBlogger7125tag:blogger.com,1999:blog-27705661.post-68820095909826294892009-01-21T15:55:00.000+00:002009-01-21T15:55:00.000+00:00D. Zeilberger thinks "The Human Obsession With "Fo...D. Zeilberger thinks "The Human Obsession With "Formal Proofs" is a Waste of the Computer's Time, and, Even More Regretfully, of Humans' Time".<BR/><BR/>http://www.math.rutgers.edu/~zeilberg/Opinion94.htmlAnonymousnoreply@blogger.comtag:blogger.com,1999:blog-27705661.post-9485317202181732712008-11-10T13:13:00.000+00:002008-11-10T13:13:00.000+00:00The December 2008 issue of the Notices of the AMS ...The December 2008 issue of the Notices of the AMS has some good articles on the subject.<BR/><BR/>http://www.ams.org/notices/200811Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-27705661.post-48396059118209711742008-08-19T13:13:00.000+00:002008-08-19T13:13:00.000+00:00As a PS to my post above, process algebra has plen...As a PS to my post above, process algebra has plenty examples of proofs being improved over time too.<BR/><BR/>* Take for example recursive definitions of processes. If I remember correctly, Milner used process equations A = P. Later he moved to equations A(x1, ..., xn) = P with the free names of P being a subset of {x1, ..., xn}. The original formulation can cause inconsistency in some boundary cases, but in all the cases that humans are interested in, the problem doesn't matter and the latter, more stringent definition is expressive enough. (The thorny issue of alpha-conversion can be mined for more examples of this -- interestingly, the full problem of alpha-conversion has not been solved fully).<BR/><BR/>* Milner used the notion of weak bisimulation up to weak bisimulation to prove some theorems. It was later shown inconsistent. But the problem was fixable.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-27705661.post-36063704725242998382008-08-04T14:43:00.000+00:002008-08-04T14:43:00.000+00:00I think the original author (Nathanson) makes too ...I think the original author (Nathanson) makes too strong a distinction between theorems that are true, and those that are false. The history of mathematics is full with theorems that are false if one takes their claims literally. Similarly, the history of mathematics is replete with proofs that have serious gaps. Nathanson's example of the first proposition in Book I of Euclid's Elements ("On a given finite straight line to construct an equilateral triangle") is instructive here. The problem was overcome in some sense only about 2000 year after Euclid, by Hilbert's new axiomatisation of geometry. What Hilbert did was essentially to add new axioms, i.e. additional assumptions. This is very common in mathematics: a proof is faulty, even though it has been vetted by mathematical experts, but by adding a few simple and additional assumptions that do not stand in the way of applications of the theorem, that theorem can still be proven (other examples (1) the development that lead to axiomatic set theory that is the current most widely accepted foundation of mathematics, in particular the invention of the axiom of choice, (2) the development of calculus, with its move from continuity/convergence to uniform continuity/convergence). What does this show?<BR/><BR/><BR/>* It shows that the established process of refereeing is sufficient to weed out egregious errors, but not to prevent all errors.<BR/><BR/>* Moreover, the remaining errors tend to be fixable. The remaining errors will be weeded out more and more, the more a mathematical construction is used in other contexts.<BR/><BR/>Hence mathematical trust (like all trust) increases with time. This mirrors the experience in other scientific fields. In physics, an experiment, a theory establishes itself by being repeated by researchers other than the originators, and by making predictions that are different from those which it was intended to make.<BR/><BR/>What is the role of interactive theorem provers here?<BR/><BR/>* They complement the refereeing process. They are very good at things human referees are bad at, namely at going through large, boring and repetitive parts of proofs that are increasingly cropping up in proofs (e.g. Four Colour Theorem, Hales's proof of the Kepler conjecture etc). They are bad at creative invention which is something humans see themselves as being good at.<BR/><BR/>* Moreover, and crucially, their work is repeatable. Everybody can check at home if Gonthier's formalisation proves the Four Colour Theorem, we no longer have to rely on Gonthier's claim that he checked everything.<BR/><BR/>* Finally, and in the long run probably most importantly, they can be reused. Humanity is building up a library of formalised proofs which can be used in novel context to formalise more proofs.<BR/><BR/>All of this adds a novel dimension of certainty to mathematical proofs. I envision that in 50 years from now, a result will not be accepted unless it has a formal proof.<BR/><BR/>We are not there yet, proof assistants are still to difficult to use. In essence you need to spend a few years learning how to use these things before you can be very efficient, but I expect that problem to be overcome. This will be a great benefit to science.<BR/><BR/>An interesting question arises from the rise of zero-knowledge proofs. What would happen if scientist publish their results only as zero-knowledge proofs, so as to keep a competitive advantage over their colleagues? Scientific communication as we know it may come to an end to everybody's detriment.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-27705661.post-80750567241372935522008-07-30T20:00:00.000+00:002008-07-30T20:00:00.000+00:00thanks for the post.this is why i think alternativ...thanks for the post.<BR/><BR/>this is why i think alternative proofs are very very important (and should be published in journals more often).Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-27705661.post-91136469843459183782008-07-30T08:05:00.000+00:002008-07-30T08:05:00.000+00:00Well, I believe it should happen eventually. I als...Well, I believe it should happen eventually. I also think that technically it's not that much of a problem. <BR/><BR/>In principle, proofs (unlike programs) are *made* to be verifiable. So, if proof is written in some formal language, it can be verified in straightforward manner. Moreover, such languages exist and are used in *practice*. I know at least one - TLA+, Temporary Logic of Actions (http://research.microsoft.com/users/lamport/tla/tla.html),<BR/>which is rather popular in specification, verification and formal reasoning about discrete dynamic systems.<BR/><BR/>So, most of required components are out there. What we really need to make it work is 1) unified approach, ideally it would be one standardized "proof language", 2) fine selection of software tools, available for everyone, 3) support from the society.<BR/><BR/>I can vividly imagine how it's going to be. We use "includes" instead of bibliographical references. Archives and journals do not accept papers, which are not written in formal languages. Paper reviewing becomes an order of magnitude simpler - all proofs are verified automatically on the server during submission. Papers are automatically generated from comments in proof source code. Arguments in natural language tend to become more sloppy - no reason to formalize here, check the source code if you like. Automatic generation of proofs is gaining popularity.Anonymousnoreply@blogger.comtag:blogger.com,1999:blog-27705661.post-7143323439598198802008-07-29T18:59:00.000+00:002008-07-29T18:59:00.000+00:00An oldie, but a classic:http://doi.acm.org/10.1145...An oldie, but a classic:<BR/><BR/>http://doi.acm.org/10.1145/512950.512970<BR/><BR/>"Social processes and proofs of theorems and programs" (DeMillo/Lipton/Perlis)Suresh Venkatasubramanianhttps://www.blogger.com/profile/15898357513326041822noreply@blogger.com