About This Blog

Automating Invention is Robert Plotkin's blog on the impact of computer-automated inventing on the future of invention and patent law.

Click here for latest videos.

News Feeds

« U.S. Ruling on Business Method Patents | Main | The Search for Code-Free App Builders »

January 23, 2009

QED by Computer

New computer tools could revolutionize the field of mathematics by assisting in the development of nearly infallible proofs of mathematical theorems. Up until now, traditional proofs allowed many inferences to be glossed over or omitted, leaving determination of the correctness of a theorem up to the scrutiny of other mathematicians. A series of articles by leading experts published in the Notices of the American Mathematical Society describe the use of computer assistants in the development of "formal proofs" which provide checks for every logical inference in a mathematical theorem.

If computer proof assistants come into widespread use, formal proofs of the central significant theorems of mathematics may be possible. Thomas C. Hales likens this possibility to "the sequencing of the mathematical genome."

Posted by BlogAuthor1 at January 23, 2009 2:23 AM
category: Philosophy of Computing


Post a comment

Thanks for signing in, . Now you can comment. (sign out)

(If you haven't left a comment here before, you may need to be approved by the site owner before your comment will appear. Until then, it won't appear on the entry. Thanks for waiting.)

Remember me?