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."
Yea, this system and the system I want are two different entities. The system in question could keep each set of axioms and theories separate and accept the fact that it is essentially shooting a shotgun out into the universe of knowledge. But that isn't as particularly interesting to me as a system which will collect all of scientific knowledge. I think that the points where we see contradictions (i.e., collisions) between theories will provide very useful insight into the nature of our universe. And, it may even be the case that this is exactly the reason that quantum mechanics and Newtonian physics do not mesh.