Slashdot Mirror

← Back to Stories (view on slashdot.org)

Towards a Wiki For Formally Verified Mathematics

Posted by kdawson on from the preparing-the-ground-for-our-robot-overlords dept.

An anonymous reader writes "Cameron Freer, an instructor in pure mathematics at MIT, is working on an intriguing project called vdash.org (video from O'Reilly Ignite Boston 4): a math wiki which only allows true theorems to be added! Based on Isabelle, a free-software theorem prover, the wiki will state all of known mathematics in a machine-readable language and verify all theorems for correctness, thus providing a knowledge base for interactive proof assistants. In addition to its benefits for education and research, such a project could reveal undiscovered connections between fields of mathematics, thus advancing some fields with no further work being necessary."

1 of 299 comments (clear)

  1. Machine proofs are a farce by Secret+Rabbit · · Score: 0, Troll

    This is totally nuts. Machines CAN NEVER BE AS GOOD AS THE ONES THAT PROGRAM THEM. For that to be so, it'll require creativity, etc. Computers, at least now, have no such capacity. After all, how are new proof techniques supposed to be checked when they are an unknown quantity? This is total BS.

    If one wants an example of such things gone awry, you need to look no further than James Anderson's Transreals. There exists proofs that they are inconsistent at the axiomatic level, but James just states that he has a machine proof that states they are consistent and ignores the proofs completely. In fact, his response to the criticism has been the typical political speak of not actually addressing anything.

    Given the above, you'll have to excuse me while the Mathematical community at large and myself completely ignore and shun this.