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
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.
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.
They didn't claim the site was "complete". Anyway, if they only include constructive proofs then Godel's Theorem is not relevant
Does this mean that Isabelle needs a formal proof to prove it works?
æeee!
There are tens of thousands (hundreds of thousands?) of institutions worldwide dedicated to precisely what you describe. They're called "universities."
Or were you suggesting that someone teach mathematics to anyone who's interested... for free?
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.
"Just my take on it, I'm interested in maths, but resent the way mathematicians try to maintain their elitist clique."
LOL. That's the funniest thing I've read all day. Thanks for that.
We know where leadership by an anti-intellectual "strongman" who scapegoats minorities and likes boisterous rallies goes
I believe a lot of the symbols and obtuse/esoteric dialogue is not really meant to preserve an elitist clique (although being a math minor I think I can sympathetic with your sentiment - at times to me it felt like that, but mostly when I didn't understand something or got a bad grade on an exam, which happens to even the brightest sometimes), because lets be honest, even the best math professors don't make huge gobs of money; but they are simply presented as they are , without explanation, for sake of brevity and clarity. The abstractions are useful because they provide succinct methods to discuss complex subjects, but they aren't useful because they obfuscate the meaning of what they are trying to discuss.
That being said, I really like this idea. It would be nice to have a easily accessed database containing all of proven mathematics. A "mathematics wiki" would let you click on a symbol you might not know, and take you to an explanation for that symbol.
That being said, there really is no substitute for a good math teacher.
We just need tri-state boolean logic: true, false, godel.
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.
Hey. A lot of people devote a lot of their time in explaining their areas of mathematics to the general public (including myself). And as for your distaste for abstraction. That's what maths is! There is a reason the general public do not follow much in the way of mathematical developments and that is because research level mathematics is actually really hard and takes a lot of dedication to understand well. There is also no elitist clique. We love it when people show interest in our work and want to understand it.
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.
Disclosure: I am a mathematician. I also graduated from Harvard, and I know Cam Freer personally.
You make several interesting but separate points in your post. Let me respond to them one at a time. Regarding pay-to-view websites, I can assure you that many mathematicians are just as unhappy as you are with the lack of public access to publications. This issue is larger than just mathematics (see for example musicians vs. RIAA, which is essentially same issue), and to pin the blame on mathematicians is unfair. This is a problem that society as a whole needs to solve in all its incarnations.
About making mathematics more accessible to the public, I agree that this step is necessary for ethical and practical reasons, and it's one of the reasons why I left a pure research position (with no teaching responsibilities) in exchange for a research position having some teaching responsibilities. However, I really doubt that public education would result in mathematics being further advanced. The cutting edge of new mathematics today is so far beyond the pale of the public that even a herculean effort at education won't be enough to bring very many people into the fold. There is a saying that the more you know, the more you know you don't know, and having been through a Ph.D program I can assure you that what you perceive as elitism is nothing of the sort -- the gap between current research and the general public is simply too wide for even the best educational efforts to bridge.
In fact, it's not even clear to me that increasing the rate of advancement of mathematics is the right goal. Perhaps we should even be holding back the development of new mathematics to give the public a chance to catch up with what we've done.
The project being discussed won't do any of these things. It won't make mathematics more accessible; anyone who's ever seen a machine-verifiable proof knows that they're even more obfuscated than perl code. It won't affect the overall rate of advancement in mathematics, because writing machine-verifiable proofs is much slower than writing standard mathematical proofs. It will of course increase our knowledge in the area of machine-verified proofs, but it's hard to argue that this area of mathematics is any more important than any other area like number theory. If you want to target the general public, the best way is still via sites like Wikipedia or Planetmath.org where the focus is on human-readable presentation.
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.
Dude, the mathematical preprint archive has been online and publicly available before most people had even heard of the internet. As for the abstraction, it's the very heart of mathematics - we'd very much like to get rid of it, but we *can't*, because it's what mathematics *is*.
I am trolling
I think I speak for everyone when I say: you're an idiot.
At least you've managed to find Slashdot, well done.
How we know is more important than what we know.
instead of abstracting everything and assuming everyone knew as much as them [...] resent the way mathematicians try to maintain their elitist clique
Umm... parent article is so many flavors of wrong I don't know where to start, so I'll just tick off some things:
In summary: maintaining our elitist clique takes no effort whatsoever. And if you've got an allergy to abstract thought, then maybe you're just not 37337 enough to join us...
The abstractions are useful because they provide succinct methods to discuss complex subjects, but they aren't useful because they obfuscate the meaning of what they are trying to discuss.
Or..., maybe the concepts really are abstract. How can you obfuscate the meaning of an abstract entity? It is, by definition, abstract. They have to choose something to represent such concepts and they typically choose symbols from a few well-known and ancient languages.
And for not saying why, that makes you what again?
I won't believe this site works as claimed until I see it on vdash.org.
A smug bastard who would rather point and laugh at you than educate?
How we know is more important than what we know.
Machines CAN NEVER BE AS GOOD AS THE ONES THAT PROGRAM THEM.
Sure they can and you don't even really need to "program" much into them, just look at biology and evolution.
You mean like this?
Warning: Apple/Nintendo fangirl. Likes her electronics cute & cuddly. May be rabid.
Apply logic to a post? On Slashdot? You must be new here.
McCain/Palin '08. Now THAT's hope and change!
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!
I should have clarified my statement - it was typed in haste. I meant to say "the symbols are chosen to provide succinct methods to discuss complex subjects, rather than to obfuscate the meaning of what they are trying to discuss."
I agree with you. Some math concepts really are abstract. My use of "but" was in error.
Machines CAN NEVER BE AS GOOD AS THE ONES THAT PROGRAM THEM.
My mother has been saying this about me for years.
I was taught to respect my elders. The trouble is, it's getting harder and harder to find some.
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
Rather someone who doesn't know the limitations of a computer (they do have limitations you know) and doesn't have anything of substance to say.
I'll never understand why some people think that because its done on a computer, it makes it better. There are always bugs and because of that, it's no more infallible than humans. It'll just make the mistakes faster and *much* harder to detect.
Overconfidence never leads to good places.
Wholly out of context Batman!
Overconfidence never leads to good places.
How sure are you about this?
I want this account deleted.
You're just not very imaginative, living things are really no different from machines. So unless you believe everything was made by god it's already quite evident that relatively simple machines (cells) can without prior design create intelligent beings. In other words it not that hard to make machines that are better than their creators assuming you have sufficiently good technology.
Rather someone who doesn't know the limitations of a computer (they do have limitations you know) and doesn't have anything of substance to say.
You're the only one here who seems to not understand the limitations of either computer or humans.
Overconfidence never leads to good places.
Quite true, human confidence does prevent automation of many areas due to a false belief that humans are better.
I'll never understand why some people think that because its done on a computer, it makes it better. There are always bugs and because of that, it's no more infallible than humans. It'll just make the mistakes faster and *much* harder to detect.
Many computer programs are a lot less error prone than humans as even something as simple as simple mathematics would show (just give them enough numbers that are large enough). There is nothing that says computer bugs have to appear just as often as human fuckups. Computer code will pretty run the same every time which means it has to only be debugged at one point while humans can make a mistake even if they did the exact same thing correctly 10000 times.
Has anybody proven that?
thegodmovie.com - watch it
You're cherry picking your data i.e. simple arithmatic is _not_ what we're talking about. What we /are/ talking about is something that is exceedingly complicated and dynamic that requires creativity. And that is exactly the type of thing that computers are bad at. If you understood something about higher Mathematics you wouldn't be making such asinine statements.
Btw, I have both a Programming Diploma AND a Degree in Mathematics. I've also did research in a Physics department as a student which involved numerical analysis and have talked to several people regarding automated proof checkers/creators. The theory behind these things, never mind there practical implementations are *far* to immature to be practical. Not to mention that it is questionable if they are even feasible to create on a fundamental level.
How is it that you've missed my point even when I stated it? Are you trying to be obtuse for a purpose? Because, my reply indicated that I knew what you were talking about, but that YOU took what my obvious point what out of context. Would you care to actually contribute to the conversation? Or are you just going to continue to 'not get it'?
I could add on, "in the end." Would that satisfy your nit-picky-ness? Because, I've *never* heard of overconfident people not getting screwed by there overconfidence at some point (usually sooner rather than later).
Now, a question: What does this have to do with the topic at hand, or the point that I was making? How would this "sloppy" wording effect what I'm saying in any significant way?
Heh you Godel'd him up good.
I have discovered a truly remarkable sig which this post is too small to contain.
Aren't all theorems supposed to be true? Isn't this like saying "ATM machine"?
Prisencolinensinainciusol. Ol Rait!
"A lot of people devote a lot of their time in explaining their areas of mathematics to the general public (including myself). And as for your distaste for abstraction."
It's not the abstraction that's hard, it's the divorced nature of mathematics from the physics of the everyday world, I've been studying physics again in my off time and I am certain that math and physics are the same subject and should be studied as a unified subject, not divorced as they currently are in most schools around the world.
Not only that, the actual number systems themselves make math a lot harder then it is for some people. I've been experimenting and researching numeral systems that use geometric patterns, and many mathematical abstractions become infinitely easier when you use shapes and color as represnetations for your numerals, and it makes addition and subtraction (of some kinds) that much easier to see at a glance, instead of playing with rather clumsy arabic script.
If we think about it from a physics standpoint, all truth is derived from information from the environment is bombarding us with, is math really just inequalities in the information our body is receiving? I have to wonder, consider "A house" and "1 house" technically you could do computations with "a" and not lose any meaning whatsoever.
"Amazon.com Review
George Lakoff and Mark Johnson take on the daunting task of rebuilding Western philosophy in alignment with three fundamental lessons from cognitive science: The mind is inherently embodied, thought is mostly unconscious, and abstract concepts are largely metaphorical. Why so daunting? "Cognitive science--the empirical study of the mind--calls upon us to create a new, empirically responsible philosophy, a philosophy consistent with empirical discoveries about the nature of mind," they write. "A serious appreciation of cognitive science requires us to rethink philosophy from the beginning, in a way that would put it more in touch with the reality of how we think." In other words, no Platonic forms, no Cartesian mind-body duality, no Kantian pure logic. Even Noam Chomsky's generative linguistics is revealed under scrutiny to have substantial problems."
I've been studying this -- see here:
http://www.amazon.com/Molecule-Metaphor-Neural-Language-Bradford/dp/0262562359/
http://www.amazon.com/Metaphors-We-Live-George-Lakoff/dp/0226468011/
http://www.amazon.com/Philosophy-Flesh-Embodied-Challenge-Western/dp/0465056741/
I personally thing neurological sciences are going to have a lot to say about mathematical knowledge and many mathematicians and math buffs are not going to like it.
Quotes:"Thought and language are neural systems, they work by neural computation, not formal symbol manipulation." -- Page 8, embodied processing. (Molecule to metaphor)
"Language is inextricable from thought and experience" - Page 1. (molecule to metaphor)
If we never used the mathematics out of context a lot of ideas developed in physics would still be just that. Statistics (used for example in the study of cancer) would lose out greatly if Newton's theory of infinitesimals had not been developed out of its physical context context into 'calculus' and then applied to probability density functions.
"Mathematics in necessarily abstract. It is the science in which one disconnects interesting patterns from their context and studies them in their own right. A great deal of effort also goes in to applying general mathematical knowledge in a particular context."
You're not grasping what I'm saying, I'm saying the expression of math - i.e. the current symbolic form it takes, can be expressed in many different ways.
See here:
http://www.amazon.com/Where-Mathematics-Comes-Embodied-Brings/dp/0465037712/
Regardless of this person's vanity whoring, he's right. Any Input based medium can only contain/compute computations that are at one point input by a "user". The only benefit a computer has is parallel processing and the ability to more QUICKLY render sumations. Thus a computer is and will always be at a level where it can not create, only calculate. I'd say you define intelligence or creativity differently than most.
"This is the value of a summer spent and a winter earned"
the current symbolic form it takes, can be expressed in many different ways.
I heartily agree with this. Different forms serve different purposes.
What I was worried about was your previous suggestion that physics and mathematics be unified. Definitely too much mathematics has been removed from school physics and this ruins it. Moreover physical applications would show kids why they should care about mathematics. What they should begin to notice though is that the things they are learning are useful outside of physics. And they should also learn some things which they will be hard pressed to find direct physical applications for at their level (elementary number theory, probability theory).
I propose instead that the application of mathematical ideas in Physics, Biology, Chemistry, Geography,... (heck, everything) be emphasized more in school. And that mathematics lessons teach enough to make this possible.
And that quicker can quickly become not quicker when the basic rules are too basic to make it feasible to enter the theorem/proof in a timely manner. Not to mention that the input will suffer from human error on entry. So, the proof might be correct, but the come out as incorrect if (really when) the theorem is incorrectly entered. And of course, vis versa. And lets be honest. When we have fairly high error rates on simple data entry (e.g. numbers), how much higher is that going to be when we have something as complicated as this?
I also wouldn't say that I define creativity different than most. More along the lines that I have knowledge about a topic that most don't understand. So, most will not appreciate what is meant by creativity in Mathematics when most people don't understand just how creative one has to be to do higher Mathematics. This is probably so because the vast majority of people have only heard of Analysis (IF they've heard of it) and have never seen what it really is (similarly for other fields in higher Maths).
How many formal proof languages have you seen? Most of them are designed for software verification, not formalized mathematics. They are optimized to make it easier for the author, not for the reader. Vdash will (probably) use Isar which is as easy to read for a mathematician as a standard proof. There may be an excessive amount of detail that sometimes obfuscates the big picture, but there are ways to deal with that, too.
I definitely think we were always on the same page, just we weren't hearing one another :)
What I meant by "physics" was not the 'stuffy' stuff, I meant simple things in general terms - i.e. what everybody understands naturally. Life has existed for many years and many academics like to 'hold truth' bondage saying 'this is the only valid form of knowledge', and I find it disheartening because we shut down curiousity in kids, and because many academics and working mathematicians, etc, are outright incorrect. I am reminded of George cantor and what he had to endure amongst 'the most learned'.
(wikipedia)
"The objections to his work were occasionally fierce: Poincaré referred to Cantor's ideas as a "grave disease" infecting the discipline of mathematics,[6] and Kronecker's public opposition and personal attacks included describing Cantor as a "scientific charlatan", a "renegade" and a "corrupter of youth."[7] Writing decades after Cantor's death, Wittgenstein lamented that mathematics is "ridden through and through with the pernicious idioms of set theory," which he dismissed as "utter nonsense" that is "laughable" and "wrong".[8] Cantor's recurring bouts of depression from 1884 to the end of his life were once blamed on the hostile attitude of many of his contemporaries,"
How many formal proof languages have you seen? Most of them are designed for software verification, not formalized mathematics. They are optimized to make it easier for the author, not for the reader.
Indeed, write-only code is a key aspect of perl which is shared by every formal proof language.
Vdash will (probably) use Isar which is as easy to read for a mathematician as a standard proof.
In order for this claim to be true to the extent that it would affect my assertion about advancing (or not advancing) the development of new mathematics, one would at a minimum need to be able to efficiently write existing proofs in the formal language (surely one cannot hope to accelerate the discovery of new proofs if even the existing literature cannot be efficiently handled). That means formal proofs for things like Fermat's Last Theorem, Poincare Conjecture, and so on, which I honestly don't ever expect to see in my lifetime.
I don't quite follow your reasoning. In order to convince you that some proof languages are readable I would need to be able to write formal proofs efficiently? Ease of writing formal proofs is not much related to readability. As I mentioned, languages that are designed to make writing the proofs easier tend to be less readable. For some examples of machine verified proofs that I consider readable you can look at the Tiddly Formal Math site (disclaimer: I am the author of that site). As for what will be formalized in someone's lifetime it's a moving target. People used to say that the prime number theorem will not be formalized in their lifetimes and many were wrong. I am happy that the proofs being mentioned in this type of argument now are much more recent. I think formalizing large areas of mathematics will advance the development of new mathematics in about the same extent as development of modern foundations of mathematics at the end of XIX century. It was not obvious to see at that time as well why there was even a need, and how it would help.
I am confident you do not have a sense of humor.
The point is that you come off as very confident (overly so maybe?) that you are absolutely correct. Its funny because you are also bent on the notion that overconfidence will screw you.
Type LOL and let it slide not everyone gets infinite recursion the first time around.
I want this account deleted.
I don't quite follow your reasoning. In order to convince you that some proof languages are readable I would need to be able to write formal proofs efficiently? ... As I mentioned, languages that are designed to make writing the proofs easier tend to be less readable.
Readability and writeability are separate and diametrically opposed issues. Writeability is necessary in order to speed up the development of new mathematics. Readability is necessary in order to improve the general public's understanding of and accessibility to the project. We apparently both agree that readability and writeability are conflicting goals. I am of the opinion that machine readable proofs are currently inadequate on both counts, i.e. machine readable proofs are not useful for developing new math, and they are also not useful for teaching mathematics to the general public. You on the other hand seem to be convinced that machine readable proofs are adequate on both counts, despite the conflicting nature of these goals.
I hope that the above accurately summarizes our positions. If not, feel free to correct any mistakes that I have made.
Not exactly. My opinion is that readability and writeability are orthogonal in the design of a formal proof language. For most formal proof languages the design effort was invested in writeability because those languages were intended to be used for formal verification of software. However, mathematicians are not only interested in the fact that the assertion of a theorem is true, but also want to know why it is true, i.e. they want to be able to read the proofs. There is a line of formal proof languages whose design goal is readability (Mizar, Isar and the declarative proof language for COQ ). After getting used to, proofs in those languages are as readable as standard (informal) proofs.
Well, if you phrase it this way I agree. Writing formal proofs will always be more difficult than writing the standard ones. This is because they contain much more information. It is not useful for a mathematician to write his/her proofs in a formal proof language before publication. In most cases it is not even practically possible because there is not enough background in formalized form. So, if you are a mathematician, formalized mathematics will not be of much use. It will not advance your career. It may inhibit it as it is a bit addictive and may consume the time you should spend writing publications and grant proposals. It is also not useful for educating general public. It typically requires some background in the foundations, like set theory. General public doesn't know set theory. General public doesn't know how to add fractions. So what is formalized mathematics good for? I personally do it for fun and as expression of creativity. I think it may be useful for getting more information about existing mathematics. For example, take the role of the axiom of choice in the construction of Lebesque measure. Since in ZF you can not prove that real numbers are not a countable union of countable sets, you can not construct the Lebesque measure (or any nontrivial measure on real numbers that assigns zero to all singletons) without using the axiom of choice somewhere. Where exactly is it used? What can you get without it? It would be very easy to find out if we had a formalized construction. Another use of formalized mathematics could be learning mathematics not by the "general public" but by the students of mathematics. We may disagree on that since you don't believe that formal proofs can be made readable. But I think they can, and if they are structured well, as Isar allows, the machine can display the desired level of detail, zoom in if some step is not clear and zoom out if some part is (seems) obvious. This use is more about knowledge representation than correctness of proofs.