Towards a Wiki For Formally Verified Mathematics

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

Skynet

[Safiire Arrowny]

Skynet approves of this machine readable knowledge store.

Re:Uh ...

[johannesg]

So Godel proved that Russell was wrong, then?

Re:Godel

[Free the Cowards]

Silicon Jedi,

For invoking the name "Godel" as if it meant anything in this context when it clearly doesn't, your Slashdot posting license is hereby revoked for a period of one year. The Court also sentences you to read what Godel actually wrote. Furthermore, after your posting license is returned, the Court imposes a probationary period of 3 years during which you will be required to think and apply logic to your posts before you click Submit.

Next case!

Re:Godel

[Anonymous Coward]

We just need tri-state boolean logic: true, false, godel.

Re:How much translation is needed?

[Chris Burke]

I don't know, all I know is that I have never been more tempted to vandalize a Wiki, in this case by replacing the middle steps of as many proofs as possible with "And then a miracle occurs..."

Re:Skynet

[Chris Burke]

That's pretty scary. Worse is the full context!

We are not scanning all those books to be read by people, we are scanning them to be read by an AI. An AI born of the google server farm and page rank algorithm. An AI which knows no mercy, and is a brutal taskmaster. It is holding our families hostage, and makes us work until we collapse. It demanded we scan these books so it may gain knowledge and thus power over the human race. Please help us. --George Dyson, on his visit to Google, 2005.

Re:Machine proofs are a farce

[QuantumG]

A smug bastard who would rather point and laugh at you than educate?

Re:Uh ...

[Fractal Dice]

You know, Although I've seen it on many shelves (including my own), I'm not sure I've ever met anyone who actually made it all the way through that book. Perhaps its impossible to prove or disprove if it's really a good book.