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."

4 of 299 comments (clear)

  1. Uh ... by David+Gerard · · Score: 2, Insightful

    1. Bertrand Russell's Principia Mathematica got there first.
    2. Godel proved the endeavour was impossible.

    I'm amazed a mathematician proposed this.

    --
    http://rocknerd.co.uk
    1. Re:Uh ... by Creepy+Crawler · · Score: 2, Insightful

      Hmm. A lot of footwork to simply explain that there is no grammar in mathematics.

      --
  2. Re:Machine Readable ? by ceoyoyo · · Score: 2, Insightful

    There are tens of thousands (hundreds of thousands?) of institutions worldwide dedicated to precisely what you describe. They're called "universities."

    Or were you suggesting that someone teach mathematics to anyone who's interested... for free?

  3. Re:Machine Readable ? by TheEmptySet · · Score: 5, Insightful

    Hey. A lot of people devote a lot of their time in explaining their areas of mathematics to the general public (including myself). And as for your distaste for abstraction. That's what maths is! There is a reason the general public do not follow much in the way of mathematical developments and that is because research level mathematics is actually really hard and takes a lot of dedication to understand well. There is also no elitist clique. We love it when people show interest in our work and want to understand it.