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."
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
Godel pwns the site.
I'm not entirely familiar with machine verifiable proofs, but how much effort is needed to take a proof from www.planetmath.org and bring it up to standard for something like this? Obviously it'd depend on the thoroughness of the original proof, but I imagine a fair bit would be missing anyway. Also, would you be able to choose the axioms you're using?
Skynet approves of this machine readable knowledge store.
the wiki will state all of known mathematics in a machine-readable language
I'd suggest that most mathematics is already in a "machine-readable" language, and those machines (i.e. the ones who only post their work on pay-to-view websites) are the ones that have held back the connecting of various fields.
If they'd just make it a bit more accessible for the general public, and provide more examples of what they are doing, instead of abstracting everything and assuming everyone knew as much as them (or rather what symbols they are using to represent what they know), then maybe mathematics would be further advanced.
Just my take on it, I'm interested in maths, but resent the way mathematicians try to maintain their elitist clique.
They did what with the who in the wikihow?
What? You haven't read Diaspora by Greg Egan? Shame on you!
Sean Ellis
Follow OfQuack's antics on Twitter.
Does this mean that Isabelle needs a formal proof to prove it works?
æeee!
there are some areas like formal logic and staff which is heavily set-theoretical (like point-set topology) where automated provers are already available. you probably can add most of the algebra as well. OTOH, things like analysis (real, complex, functional) is much harder to formalize, many proofs end up with "now take epsilon to 0", or "take n to infinity", you have to deal with countable vs uncountable infinities. I'm not saying it's impossible to formalize, only that that's much harder.
That sounds great, but when will there be a computer which can solve my real-life math problems which mostly revolve around when will I pass Bob if Bob is driving at a speed in miles per hour from a place to a place at a time and I start driving toward the first place from the second place at a speed in kilometers per hour at a time? My current method of polling 4th graders isn't working very well.
I played with the idea about making such a project a year ago, with dependencies between the lemma/theorems etc. in machine-readable format, but had no clue how to represent the understanding and terms of math in a consistent way. I'm interested in how they do that here...
NB: The message above might reflect my opinion right now, but not necessarily tomorrow or next year.
without EMACS? Now that is progress.
How we know is more important than what we know.
Can't you derive an infinite or at least an enormous number of true theorems from the existing ones? Do they and if, how do they remove "duplicates"/"extras" that are not theorems, much more corollaries? :-/ no?
As pure mathematicians they might be interesting in doing so
NB: The message above might reflect my opinion right now, but not necessarily tomorrow or next year.
My experience with math professors is that most of them are able to present clear explanations of the subjects they're teaching without referring extensively to topics that are more advanced than the topics at hand.
On wikipedia, however, "obtuse/esoteric dialogue" seems to be the norm, and I have very rarely been able to understand a math article about a topic that I didn't already understand. I hope that this trend will eventually correct itself by better editing.
... laughs at your difficulties.
(but is afraid of zombie Kurt Gödel.)
Tweet, tweet.
Formally verified mathematics has been around for decades; it's just hard. Putting it into a wiki won't make it any easier.
Will there be some preferences where I can decide if I assume the axiom of choice or not? The content must surely vary accordingly? Seriously though, this does seem like an interesting project but a wiki is hardly the correct format if the proofs are all going to be "machine readable" and more importantly "machine verifiable". I can't help but foresee several years of work going into converting the very simplest of theorems into "machine readable" format long before anything interesting gets included. Must confess I can't help thinking that AI just isn't up to it, and there isn't enough Human Intelligence willing or able to commit the millions of hours required to actually make something like this work.
One of the criticisms of mathematics is that mathematicians claim truth and rigour, yet in practise their proofs are often quite sloppy. In other words, most proofs are convincing rather than rigorous. Thus some have suggested that mathematics is made up of opinions rather than logically true assertions.
Some "scholars" from the humanities have used this to suggest we develop a postmodern, liberatory mathematics, freed from the tyranny of logical proof, and thus from the oppressive hegemony of the modern militaristic patriarchy.
This project might help to stem such blather. Although, as they say, you can't reason someone out of a position if they never reasoned themselves into it in the first place.
I sounds like a great idea. So, umm, do it.
How we know is more important than what we know.
davejenkins.com |
Oh it sounds like a great idea now, technology able to reveal previously undiscovered connections.
But then they'll finish it, call it the Intersect, and it'll accidentally get downloaded into the brain of a computer repair tech. Then what?
"thus advancing some fields with no further work being necessary."
And presumably with no need for further mathematicians.
The Chinese will be furious.
frdcsa.org frd stands for Formalized Research Database. been doing this since 2001. there is also FDL (formal digital library)
http://frdcsa.org/
This is totally nuts. Machines CAN NEVER BE AS GOOD AS THE ONES THAT PROGRAM THEM. For that to be so, it'll require creativity, etc. Computers, at least now, have no such capacity. After all, how are new proof techniques supposed to be checked when they are an unknown quantity? This is total BS.
If one wants an example of such things gone awry, you need to look no further than James Anderson's Transreals. There exists proofs that they are inconsistent at the axiomatic level, but James just states that he has a machine proof that states they are consistent and ignores the proofs completely. In fact, his response to the criticism has been the typical political speak of not actually addressing anything.
Given the above, you'll have to excuse me while the Mathematical community at large and myself completely ignore and shun this.
Including only formally verifiable theorems (and preferably the wiki will have a built-in mechanism to automatically check all submitted theorems with no human intervention) will make impossible vandalism or honest mistakes in the form of errors.
But, this is far from having a neutral, impartial wiki. A theorem prover can prove an infinite number of true theorems, but almost all of them will be useless. It still takes human involvement to judge a theorem by its importance, whether in the form of inherent importance to mathematics, some empirical usefulness, relevance to another theorem (as lemmas are), some distinguishing or unique feature not covered in a previous case, or simply a particular example mathematical beauty.
This kind of selection is inherently subjective - if machines could do it, we wouldn't need human mathematicians. But this also means there will surely be debates about what kind of content is important enough to include.
Plus, of course, all your theorems will depend on your set of axioms and rules of inference, from accepting/rejecting the Axiom of Choice, to proponents of non-classical logic.
Choice of wording, structure, organization, categorization, etc. is also up in the air, and there will definitely not have a single opinion about the right way to do any of that.
Machines may prove the theorems, but it'll be humans who ultimately write the wiki. Sure, that wiki might be more neutral, impartial, and formal than Wikipedia. But it certainly won't completely lack ambiguity and subjectiveness that are natural to humans, which is both a strength and a weakness.
I won't believe this site works as claimed until I see it on vdash.org.
If this worked couldn't you just submit all possible strings of text increasing in length to proof checker until you proved anything that was likely to be useful.
Wouldn't this project be another "armageddon" machine (LHC..)? What if someone finds a bug in it 25 years from now? A bug that generates a contradiction? It would prove EVERYTHING to be TRUE (and FALSE). OHH GOD! STOP IT!
Wouldn't it be better to get something like an ajax version of http://metamath.org/ up?
Just for the record, if you're dealing with "machine readable language", what you want is the Turing Halting Problem, which is essentially the same mathematical derivation Godel used for theorems, but applied to algorithms.
I'd like to see the theorems turned into code turned into music. Or, rather, Id like to hear the theorems turned into code turned into music.
It is a much better book if you skip the Achilles, Tortoise, etc. stories. Read them only if you can't understand the math without the analogies the stories provide. GEB was a huge help in understanding what Godel was talking about for me.
What I was left wondering after finishing the book is whether there are any interesting truths that lie outside those provable by Peano arithmetic about Peano arithmetic.
Maybe they can pick up some caveats from the Bourbaki fraternity.
http://en.wikipedia.org/wiki/Bourbaki
An interesting article (well worth reading) is here: http://planetmath.org/encyclopedia/NicolasBourbaki.html
time time everywhere and not a second to spare
Has anybody proven that?
thegodmovie.com - watch it
Aren't all theorems supposed to be true? Isn't this like saying "ATM machine"?
Prisencolinensinainciusol. Ol Rait!
Kurt GÃdel (b. 1906, d.1978) made significant contributions to mathematical logic, set theory, and philosophy, but he is most widely recognized for his incompleteness theorems, arguably the most profound results in logic since Aristotle. He proved, in 1931, that no formal mathematical system can prove all mathematical truths. Put more crudely, he proved that truth is a stronger criterion than proof. To get a taste for this claim, consider this light-hearted extract from the essay, "Godel's second incompleteness theorem explained in words of one syllable", by George Boolos (1994):
Quote:
First of all, when I say "proved," what I will mean is "proved with the aid of the whole of math." Now then: two plus two is four, as you well know. And, of course, it can be proved that two plus two is four (proved, that is, with the aid of the whole of math, as I said, though in the case of two plus two, of course we do not need the whole of math to prove that it is four). And, as may not be quite so clear, it can be proved that it can be proved that two plus two is four, as well. And it can be proved that it can be proved that it can be proved that two plus two is four. And so on. In fact, if a claim can be proved, then it can be proved that the claim can be proved. And that too can be proved.
Now: two plus two is not five. And it can be proved that two plus two is not five. And it can be proved that it can be proved that two plus two is not five, and so on.
Thus: it can be proved that two plus two is not five. Can it be proved as well that two plus two is five? It would be a real blow to math, to say the least, if it could. If it could be proved that two plus two is five, then it could be proved that five is not five, and then there would be no claim that could not be proved, and math would be a lot of bunk.
So, we now want to ask, can it be proved that it can't be proved that two plus two is five? Here's the shock: no, it can't. Or to hedge a bit: if it can be proved that it can't be proved that two plus two is five, then it can be proved as well that two plus two is five, and math is a lot of bunk. In fact, if math is not a lot of bunk, then no claim of the form "claim X can't be proved" can be proved.
So, if math is not a lot of bunk, then, though it can't be proved that two plus two is five, it can't be proved that it can't be proved that two plus two is five.
By the way, in case you'd like to know: yes, it can be proved that if it can be proved that it can't be proved that two plus two is five, then it can be proved that two plus two is five.
This is PRECISELY the problem with metamath.
There needs to be higher level block that can be reused (and can always be expanded through variable substitution)
Do we imagine programming today with assembler ?
it is the same for formalized math.
We need a way
- to pack proof and add a title (for instance use in a proof "this is true by compactness".
- to have and publish libraries of concept
It is exactly like programming..
Mathematician have neglected it up to now but this is a CARDINAL mistake, as it has the potential to make self adaptive lessons for instance, have automatic exercises generation etc, etc....
This is a tremendously exciting project that can completely change the way math is learned and generate a true LEAP in our collective mathematical abilities.