Slashdot Mirror
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 approves of this machine readable knowledge store.
So Godel proved that Russell was wrong, then?
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!
If you mod me Overrated, you are admitting that you have no penis.
We just need tri-state boolean logic: true, false, godel.
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..."
The enemies of Democracy are
A smug bastard who would rather point and laugh at you than educate?
How we know is more important than what we know.
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.