Achieving Mathematical Proofs Via Computers

eldavojohn writes "A special issue of Notices of the American Mathematical Society (AMS) provides four beautiful articles illustrating formal proof by computation. PhysOrg has a simpler article on these assistant mathematical computer programs and states 'One long-term dream is to have formal proofs of all of the central theorems in mathematics. Thomas Hales, one of the authors writing in the Notices, says that such a collection of proofs would be akin to the sequencing of the mathematical genome.' You may recall a similar quest we discussed."

Comments

Re:what is a central theorem?

[Bromskloss]

on the way to building a silicon mathematician.

I think we have one at our department. He's, like, very stiff.