Re:The Human Obsession With "Formal Proofs" is a Waste of Time
by yummyfajitas on Tuesday February 17, 2009 @07:26PM
(#485200)
I think it's more a "Humans vs Computers" debate. Some background:
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.
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.