The Human Obsession With "Formal Proofs" is a Waste of Time
math.rutgers.edu
math.rutgers.edu
Not surprisingly, the formalist program was also more fruitful for endeavours like computational logic and the theory of computation, which resonate with the formalist tenet that mathematics is just the manipulation of strings of abstract symbols according to specific rules.
This http://en.wikipedia.org/wiki/Brouwer-Hilbert_controversy gives some of the context.
Tom Hales cleverly reduced the Kepler Conjecture to the solution thousands of linear programming problems: if all the solutions are bigger than something, the kepler conjecture is true. Then he had a computer solve the LP problems, and the result was that Kepler was true.
However, his solution was informal in the following sense; he didn't have a rigorous proof that the solution of the LP problems was accurate, nor were his programs proven correct. Now he is attempting to redo the proof in HOL, a formal theorem proving system.
More background: no math paper is completely formal. All involve some handwaving, especially the 200 page monsters that appear in Annals of Math. An example from a paper I'm currently writing: "It can be easily seen by elementary calculus arguments that..."
Doron is arguing that the mathematical community is holding Hale's computer proof to a higher standard than it would hold a comparable 200 page human-written paper. Basically, he is claiming that we should accept an informal computer-assisted proof just like we would accept an informal human-written proof.
In many cases theories become simpler not more complicated with constructive foundations for mathematics, (for instance, synthetic differential geometry is a much more elegant way of doing geometry). Modern categorical foundations for mathematics, using topos theory, has intuitionistic logic as its natural language.
It is exactly constructive foundations of mathematics which is related to foundations of programming languages, and this in many cases is formalized via the Curry-Howard correspondence which takes programs to proofs and vice versa.
http://math.andrej.com/2008/08/13/intuitionistic-mathematics...
Algorithms are _meaningless_ without accompanying proofs. There should be --- and is --- a continuum of formality. The 20th Century has been unique in recognizing the fallacies and contradictions of completely informal reasoning; why give up when we're finally ahead?
Most of what we write as coders (and in fact, most of what the world runs on) are algorithms without proofs which "mostly" work.
In fact, you could call almost all of our strategies in social interactions "heuristic algorithms"!
So many areas of life cannot easily be mathematically analyzed. Hence, our brain resorts to algorithms which work "most" of the time, which is luckily usually sufficient for survival.
I found an abstract (http://www-abc.mpib-berlin.mpg.de/users/ptodd/SimpleHeuristi...) but it's a bit dry. The actual book is a lot more readable.
But if I were writing flight control software, I'd take the time to formally prove tings, I'd even write the speck in Z.
Given that algorithms can have undecidable outcomes, its hard to even tell what a meaningful description of such algorithms in terms of proof even entails.
Modern theorem provers are also pretty awesome in that they can often, using the correspondence between formal proofs and programs (the Curry-Howard isomorphism for those interested), turn a proof that some unspecified function F, say, sorts a list into a Haskell/ML implementation of a function satisfying that proof.
And in case you think that B-T is irrelevant, informal reasoning about infinities produced all sorts of results that caused people problems. Formal reasoning about infinities gave us calculus for real, that works wherever it's known to work. And I use infinities on a daily basis designing and implementing systems to assist with tasks similar to air traffic control and automated target tracking.
Computers can be used to explore and experiment with numbers, geometry and some structures, and will probably one day be able to assist with exploring more abstract concepts, but as things stand today, there's a great deal of mathematics that no one can see how to do with computers.
To say otherwise is to demonstrate ignorance of both fields.
But what the author describes as the Hilbet-Bourbaki method is simply what math is. Any mathematician will tell you that if you're not proving theorems then you're not really doing math.
Anyway, what good is a computer proof if it doesn't provide any insight ? (which is usually the case). A good proof usually illuminates why some mathematical statement is true, and that is why computer proofs are usually looked upon with suspicion by many mathematicians.
After all, a computer simply churning out the answer (42 ?) doesn't advance the state of human knowledge at all.
Further, formal computer proofs are rarely wholly generated by computer. Rather the user specifies goals and tactics which the computer verifies or refutes. If one is using a reasonably powerful logic (ie first-order and not propositional) there are only relatively small tasks that can be automated. Hence, the result is often equivalent, or, at least, close to a human generated proof in terms of what is illuminated about the mathematical statement, but every step is necessarily valid.
Further, there is a field of modern mathematical logic called proof mining which concerns itself with the analysis of fully formal proofs and can often obtain illuminating details from a formal proof that wouldn't be possible from an informal equivalent.
This isn't to say that all mathematics should be formal in the sense indicated, but just to point out that it remains an interesting endeavor that is worth keeping an eye on. Also, note that the author /does/ think that formal verification of this sort can be useful for software development which is indeed what formal methods are mostly used for these days.
"and I believe that mathematicians who continue to do pure human, pencil-and-paper, computer-less, research, are wasting their time."
"The axiomatic method is not even the most efficient way to prove theorems in Euclidean Geometry."
The author is disagreeing with math as practiced by most mathematicians: proof using only pencil, paper and coffee.
BTW, formalism is only a fairy tale mathematicians tell their children when putting them to bed at night. In our hearts, we're all closet platonists.
More quotes:
"and I believe that mathematicians who continue to do pure human, pencil-and-paper, computer-less, research, are wasting their time." If they learned how to program, in, say, Maple, and used the same mental energy and ingenuity while trying to use the full potential of the computer, they would go much further.
I.e., human + computer >> human.
"The axiomatic method is not even the most efficient way to prove theorems in Euclidean Geometry." Thanks to Rene Descartes, every theorem in Euclidean Geometry is equivalent to a routine identity in high-school algebra,
I.e., verifying algebraic identities is easier than euclidean proofs, especially if done by maple.
His main argument is simply that computer-assisted proofs should not be held to a higher standard than human-only proofs.
If something like that has been discovered, fine, use it, and solve geometry problems in that way in the future. But how would that have been discovered without doing classical mathematical proofs? I don't think that some problems can be solved algorithmically proves that the same holds for all problems.
Most students do not need to be concerned with (and indeed, are not instructed in) formal proofs. But, if we are going to push math forward, we need to lay a solid foundation of axioms and proofs.