Towards a Wiki For Formally Verified Mathematics 299
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."
Re:Uh ... (Score:3, Interesting)
The system proposed however, might find things that are true that people haven't thought about proving yet. I'm sure a mathematician could come along and give a more complete answer.
Re:Skynet (Score:5, Interesting)
Re:How much translation is needed? (Score:3, Interesting)
It's rather a lot of work to prove that 2+2=4 if you start from basics by hand too.
The link you provided looks like it's the LONGEST path they could find. Not the shortest. Plus, from a quick reading, it looks like they were actually proving that (2+0i) + (2+0i) = (4+0i), which is a little bit different.
Re:How much translation is needed? (Score:3, Interesting)
My six year old daughter has proved to my satisfaction that 2+2=4, simply by counting on her fingers.