×

Welcome to the Slashdot Beta site -- learn more here. Use the link in the footer or click here to return to the Classic version of Slashdot.

Thank you!

Before you choose to head back to the Classic look of the site, we'd appreciate it if you share your thoughts on the Beta; your feedback is what drives our ongoing development.

Beta is different and we value you taking the time to try it out. Please take a look at the changes we've made in Beta and  learn more about it. Thanks for reading, and for making the site better!

Towards a Wiki For Formally Verified Mathematics

kdawson posted more than 5 years ago | from the preparing-the-ground-for-our-robot-overlords dept.

Math 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."

cancel ×
This is a preview of your comment

No Comment Title Entered

Anonymous Coward 1 minute ago

No Comment Entered

299 comments

Uh ... (2, Insightful)

David Gerard (12369) | more than 5 years ago | (#25210921)

1. Bertrand Russell's Principia Mathematica got there first.
2. Godel proved the endeavour was impossible.

I'm amazed a mathematician proposed this.

Re:Uh ... (4, Funny)

johannesg (664142) | more than 5 years ago | (#25210961)

So Godel proved that Russell was wrong, then?

Re:Uh ... (2, Interesting)

mckinnsb (984522) | more than 5 years ago | (#25211075)

No. I'm only a math minor/computer science major, but from my limited understanding on the subject (as it was related to me by one of my smarter professors), Godel showed that Russell's system could not encompass all true statements. The problem (simplistically) lies in what is *demonstrably true* and what is *provably true*. In particular, Godel showed that Russell's system would have problems with things that are demonstrably true, or what you might call "self-evident truths" in philosophy.

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:Uh ... (5, Informative)

techno-vampire (666512) | more than 5 years ago | (#25211155)

I'm no more of a mathematician than you are, but I've had the chance to discuss this with people who really do understand it. Your description is, I think, correct, but not your conclusion. What Goedel proved was not that such an endeavor was impossible, but that it could not be complete. This is because in any system sufficiently advanced to be interesting, there would always be some things that were true but which couldn't be proven to be true. (There would also, BTW, be things that were false but couldn't be shown to be false.)

Re:Uh ... (5, Informative)

zacronos (937891) | more than 5 years ago | (#25211841)

Very close. To be 100% correct though, Goedel proved that any such endeavor would either be incomplete, or self-contradictory. In other words, for any sufficiently advanced system, there will be some things that are true but which can't be proven to be true within the system, or else there will be some things which can be proven to be true within the system but which can also be proven to be false within the system.

Re:Uh ... (1)

johanatan (1159309) | more than 5 years ago | (#25211997)

And the way he did it was through a formal numbering system for his theorems using prime numbers. Essentially, his system computed a truth statement (i.e., a theorem) such as this (except with an extremely large prime number instead of 1729):

1729 - - - - - - - - - Well-formed formula no. 1729 is not true

It's essentially a more formal rendition of the Epimenides Paradox. [wikipedia.org]

Re:Uh ... (5, Informative)

johanatan (1159309) | more than 5 years ago | (#25212115)

My apologies. [I had to brush up on the actual numbering system].

Correction: The Godel numbering system assigned a unique prime number to each symbol and axiom of his arithmetic. Then, the IDs of the combinations of symbols making up formulas were computed by raising each symbol or axiom ID to the power of its position in the sequence. And, finally, the ID of each proof or theorem by applying the same algorithm to the formula IDs making up each proof. More info here [wikipedia.org] .

Re:Uh ... (5, Informative)

SoVeryTired (967875) | more than 5 years ago | (#25212127)

"Goedel, Escher, Bach" is an absolutely astonishing book about this subject, and the foundations of logic in general. Applications to AI are also discussed. Admittedly, I had to stop reading it since it rather messed my head up (Got about 3/4 through and couldn't stop dreaming about maths). Highly recommended for any self-respecting geek.

http://en.wikipedia.org/wiki/G%C3%B6del,_Escher,_Bach [wikipedia.org]

Re:Uh ... (5, Informative)

Free the Cowards (1280296) | more than 5 years ago | (#25210963)

1. Russell did not, as far as I know, write any proofs in machine-readable language.
2. Goedel proved that such an endeavor cannot contain all true statements. But of course they never claimed that it would.

Maybe if you paid more attention you would be less amazed.

Re:Uh ... (1)

johanatan (1159309) | more than 5 years ago | (#25211913)

What does machine-readable have to do with it? Goedel's codification system was the very thing that made his conclusion rock-solid. With actual machines, one would think that the conclusion would be even more forthcoming.

Re:Uh ... (2, Informative)

Free the Cowards (1280296) | more than 5 years ago | (#25212331)

Machine readability is what separates this from Russell's work. In that, by using a machine-readable proof language, the proofs can be verified mechanically.

Goedel's conclusion is completely irrelevant to this project, so I don't understand why you even discuss it.

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25212509)

Well, for one, you mentioned it. (In number 2).

And, it wasn't so much Godel's conclusion that is of interest, but his method, which was actually only an extension of the method of Hilbert (and to a lesser degree Russell).

Are you saying that if machines had existed at that time that they could not run the codes? To disprove that assertion if that is what you are saying, then one could simply take the Hilbert system (or the Godel numbering system) and do the computations today starting from known axioms (and in fact, I bet that is exactly what the software in question is doing or going to do). If the numbering system is not identical, then it certainly must be equivalent.

Re:Uh ... (3, Informative)

Free the Cowards (1280296) | more than 5 years ago | (#25212751)

I only mentioned it because the guy I replied to mentioned it. Points 1 and 2 were separate.

I do not understand your second paragraph at all. As far as I understand it, this wiki will not be mechanically searching for new, unknown theorems. All it will be doing is mechanically verifying human-created proofs for submitted theorems. For some reason people see machine verification and fly off into nonsense la-la land. But verifying a human-created proof is nothing particularly special. What's interesting about this wiki is only that it aims to build a large-scale repository of theorems and their proofs in a machine-readable language. Nothing about how it works is in any way revolutionary or even all that interesting, only how it's being organized.

Re:Uh ... (1)

johanatan (1159309) | more than 5 years ago | (#25212525)

Reposting as non-AC so you'll be more likely to see this: Well, for one, you mentioned it. (In number 2). And, it wasn't so much Godel's conclusion that is of interest, but his method, which was actually only an extension of the method of Hilbert (and to a lesser degree Russell). Are you saying that if machines had existed at that time that they could not run the codes? To disprove that assertion if that is what you are saying, then one could simply take the Hilbert system (or the Godel numbering system) and do the computations today starting from known axioms (and in fact, I bet that is exactly what the software in question is doing or going to do). If the numbering system is not identical, then it certainly must be equivalent.

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25211943)

1. Russell did not, as far as I know, write any proofs in machine-readable language.
2. Goedel proved that such an endeavor cannot contain all true statements. But of course they never claimed that it would.

Maybe if you paid more attention you would be less amazed.

As far as you know being the operative word(s): russel developed a system of logic which allowed the developement of (he hoped) all of known mathematics.
In this system, proofs are mathematical and well defined objects and as such can be checked by a computer, though they did not of course exist at the time. The system implemented in Isabelle is actually a (distant) variant of Russel's original system, a brand of type theory.

As for the second claim, it was in fact a not so implicit assumption that such a system could be sufficient to prove all known mathematical truths, and in the event that it could not, that another more complete system could. Goedel proved both those claims false. In addition, several logicians hoped that these kinds of systems could be proven to be consistent by using other "intuitively consistent" (and weaker) systems of logic. Goedels theorems also robbed them of that pleasure.

As for Freer's project, it is quite interesting, though it will inevitably have to deal with problems other mathematical knowlege repositories have to deal with, i.e. the disparity of systems, logics and different formalisations (e.g. datatypes used) that are currently used to do formal mathematics.

Re:Uh ... (1)

Free the Cowards (1280296) | more than 5 years ago | (#25212357)

As for the second claim, it was in fact a not so implicit assumption that such a system could be sufficient to prove all known mathematical truths, and in the event that it could not, that another more complete system could. Goedel proved both those claims false.

What does this even mean? How can a mathematical truth be 'known" if it cannot be proven?

What Goedel proved false was that it would be impossible to prove all mathematical truths. But working through what is known and creating mechanically-verifiable proofs for all the ones that are actually true is certainly theoretically possible.

Goedel would be relevant if you were talking about a project to prove every true statement. But we're not, so it's not. I can't understand why anyone would even bring it up.

Re:Uh ... (1)

poopdeville (841677) | more than 5 years ago | (#25212631)

What does this even mean? How can a mathematical truth be 'known" if it cannot be proven?

There is a big difference between truth and provability. Truth is always relative to a structure. But a statement can only be proven (from a set of axioms) if it is true in EVERY structure (that "satisfies" the axioms). This is Godel's completeness theorem.

Re:Uh ... (1)

Free the Cowards (1280296) | more than 5 years ago | (#25212729)

I can't tell if you're utterly clueless, or if you're speaking on a level so far above me that I can't even detect the fact that it contains intelligence.

A statement is either true or false given certain axioms. It's not "relative to a structure" or to anything else outside those axioms. If it is "known" then it has a proof, otherwise it isn't really known.

All Godel did was prove that there are true statements which have no proof. This is interesting, in that it means it's impossible to mechanically derive all true statements which come from a set of non-trivial axioms. But essentially by definition, any statement which has no proof is not mathematically "known".

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25212021)

Partially right...
Russell didn't write the proofs... leave that to Hilbert to attempt it (not so far removed from the claim in TFA). Godel proved that Hilbert was wrong. Of course, that didn't stop people like Turing who read Godel and promptly said, "Who cares?". Turing showed that it didn't really matter.

The TFA (yes I read it) is more Turing that Hilbert.

Re:Uh ... (1)

lysergic.acid (845423) | more than 5 years ago | (#25212187)

yea, an axiomatic system doesn't have to be complete to be useful. most logical systems we use are incomplete, but their logical consistence still makes them incredibly useful in science, engineering, and even mathematical research. this Wiki won't make mathematical systems complete, but it can still help discover new theorems--and check to see that existing theorems are all logically consistent with each other.

i mean, if you are working with boolean logic you accept that its fundamental axioms are true. that is simply given when you work with this formal system. its fundamental axioms are not absolutely provable, only provably consistent with one another. but that alone is enough for us to derive great theoretical and practical use from boolean logic--enough for us to be talking to each other over thousands of miles via digital signals processed by complex logic machines.

Re:Uh ... (2, Informative)

RackinFrackin (152232) | more than 5 years ago | (#25211009)

No. Godel proved that in any axiomatic system there exist statements whose truth values are formally undecidable. If the summary is correct, then this database would contain the whole of known mathematics and use automated theorem proving to do some advances.

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25211799)

No. Godel proved that in any axiomatic system there exist statements whose truth values are formally undecidable.

No.

You forgot the 'sufficiently powerful' part of the theorem.

It's trivial to construct decidable axiomatic systems and you can even do interesting stuff with them. What you can't do is to represent natural number arithmetic with them.

Re:Uh ... (1)

johanatan (1159309) | more than 5 years ago | (#25212139)

Yes, but who is to say that known mathematics doesn't already have a contradiction of the sort Godel pointed out? There's a lot of different 'theories' and there's no guarantee that they mesh properly.

Re:Uh ... (1)

SoVeryTired (967875) | more than 5 years ago | (#25212257)

Sweet, sweet example of this: the continuum hypothesis. http://en.wikipedia.org/wiki/Continuum_hypothesis [wikipedia.org]

What this says is that there are "different" sizes of infinity. The "smallest" is that of the integers: -1, 0 , 1, 2 ...

It is possible to show that one can never pair up every real number with a distinct integer. There are simply "too many" real numbers, and any attempt to pair the two sets up will result in real numbers being left over. In this sense, the set of real numbers is "bigger" than the integers.

The continuum hypothesis says there is a set bigger than the integers but smaller than the reals. This has been shown to be unproveable (given the normal axioms of set theory, aka Zermelo-frankel set theory). Since it can't be proven or disproven, you can assume it to be either true or false and get consistant, rigorous maths. In a sense, it is both true and false *at the same time*.

Re:Uh ... (1)

orangesquid (79734) | more than 5 years ago | (#25212527)

Of course, I'm wondering if they can import the contents of the Mizar electronic library for tracking the contents of the Journal of Formalized Mathematics (http://www.cs.ualberta.ca/~piotr/Mizar/mirror/http/library/), which would be pretty cool. The big questions are where the wiki and journal both stand on the Axiom of Choice. Some of the corollaries to the axiom of choice that show up in model theory (which has some interesting things to say about the dimension of the real line versus aleph numbers, beta numbers, and omega numbers) have some very odd consequences and can cause problems when trying to create a formal system that relies on the axiom. Reduced forms of the axiom have been proposed that are less prone to paradoxes, but there's a huge body of formal proof work based on the axiom that would have to be re-worked to use a different set of axioms.

Re:Uh ... (1)

PotatoFarmer (1250696) | more than 5 years ago | (#25211015)

2. Godel proved the endeavour was impossible.

You're right. Might as well quit now, since we'll never be able to know everything.

Re:Uh ... (1)

DriedClexler (814907) | more than 5 years ago | (#25211033)

All Goedel proved was that there exist true statements that it can't prove. There are still many theorems it can prove. And the theorems it can't prove are all stuff like, "This statement cannot be proven."

Show of hands: Who here cares about the software's inability to generate theorems like that? Anyone? Didn't think so.

Re:Uh ... (1)

FrangoAssado (561740) | more than 5 years ago | (#25211351)

And the theorems it can't prove are all stuff like, "This statement cannot be proven."

While that might be true in some sense, that's not the whole story. As an example of an useful such theorem, Matiyasevich (using various people's results) has shown that there's no way to prove if certain Diophantine equations have solutions or not.

Strictly speaking, all this means is that you can write a Diophantine equation that encodes some statement like the one you stated. But this doesn't detract from the original point: there still exists some Diopnhantine equation for which we can't prove the existence of solutions (or lack thereof) in the set of axioms known as ZFC, and that's interesting in itself.

Re:Uh ... (1)

johanatan (1159309) | more than 5 years ago | (#25212189)

While the proof did contain only one such statement which caused the problem, one was enough. Godel did not even attempt to find more because the proof implies that (assuming an infinite amount of knowledge exists) there are infinitely many such statements (obviously one of these infinities has a greater degree than the other in the same way that there are both an infinite number of integers and an [smaller] infinite number of primes).

In my mind, it's kind of like dividing by zero (everything breaks down at that point). I would imagine it's a little like yeast working through dough.

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25212763)

(obviously one of these infinities has a greater degree than the other in the same way that there are both an infinite number of integers and an [smaller] infinite number of primes).

ugh. the integers and primes have the same cardinality.

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25212287)

All Goedel proved was that there exist true statements that it can't prove. There are still many theorems it can prove. And the theorems it can't prove are all stuff like, "This statement cannot be proven."

This is completely wrong. It was Russell who identified the kind of self-referential paradox you invoke, and this has very little to do with Godel's conclusions.

E.g. you can define integers using set theory and some simple axioms. But there are plenty of things that are provably true about integers that you cannot deduce from the axioms. You prove them by using other theories (e.g. group theory) and demonstrating that integers meet your other axioms.

In other words, if you gave a computer the integer axioms it could deduce a fairly small subset of the things we know about integers. If you gave the computer group theory as well it could deduce some more things. And so on. But where do the new theories come from? Not from a theorem proving machine.

This point has some interesting philosophical implications about how the brain works. In particular, the brain is not a Turing machine.

Re:Uh ... (1)

caramelcarrot (778148) | more than 5 years ago | (#25211061)

Firstly, those have nothing to do with this. Godel's theorem merely proves that there exists unprovable theorems that are true. In fact, Godel's theorem actually uses the fact that theorems can be verified in finite time - you just go line by line down the proof and check that it uses the axioms appropriately. This is a repository of theorems that are confirmable.

Re:Uh ... (0)

Anonymous Coward | more than 5 years ago | (#25211297)

Actually, I think the incompleteness line of argument here would be to object to this clip (which maybe I am reading wrong):
"...wiki will state all of known mathematics in a machine-readable language and verify all theorems for correctness, "

Now, the issue is that this is not guaranteed to possible, correct? Because nobody as of yet has walked around yet and taken the time to reduce every proof to a formal system. In fact, I've never met a mathematician who has done that for any proof, ever. So we have no idea whether or not, in a given system, we have or have not proved informally a theorem that is unprovable in that system formally.

Unless you restrict "known mathematics" to mean only mathematics that have been formalized so far. Which would be fine, but that's a whole different affair.

Also, to someone above, I don't think there is any promise that the ONLY unprovable theorems are the weird self-referential ones. We prove that the set of unprovable truths is nonempty via construction of a self-describing theorem, but whether or not there are other members in that set is a different question.

Re:Uh ... (1)

Free the Cowards (1280296) | more than 5 years ago | (#25211811)

Any given mathematical fact falls into one of three categories:

  1. Provably true.
  2. Provably false.
  3. Impossible to prove either way.

All Godel did was prove that category 3 exists. Previously it was thought that all facts fell into either "true" or "false", and the challenge was figuring out which was which.

You seem to be talking about known mathematics which have not been formalized but are considered to be true. This is, from what I can see, a major target of this wiki. Such things are a major source of uncertainty. Absent a formal proof, maybe there's a faulty piece of reasoning behind it that nobody has found yet.

Any mathematical fact which has a correct, known proof can be verified by such a wiki, at least in theory (I don't know if the tools are capable yet). Remember that the wiki is not proving facts, it is merely verifying the proofs put in by humans. If the proof is solid then it can be converted to the software's proof language and verified. If there is no such proof then it really shouldn't be considered to be part of known mathematics, since absent such a proof it's not really known whether the statement is true or not.

Godel (0, Offtopic)

Silicon Jedi (878120) | more than 5 years ago | (#25210931)

Godel pwns the site.

Re:Godel (4, Funny)

Free the Cowards (1280296) | more than 5 years ago | (#25211135)

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!

Re:Godel (0)

Anonymous Coward | more than 5 years ago | (#25211735)

Next case: Gordon Bennet vs English language

Re:Godel (1, Funny)

Anonymous Coward | more than 5 years ago | (#25211219)

We just need tri-state boolean logic: true, false, godel.

How much translation is needed? (1)

caramelcarrot (778148) | more than 5 years ago | (#25210943)

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?

Re:How much translation is needed? (1)

ceoyoyo (59147) | more than 5 years ago | (#25211145)

When I last used a proof checker (about seven years ago) there was a bit of work involved. You have to translate everything into the symbols and relations understood by the proof checker.

As I remember it wasn't the most technical process. A lot of it was dealing with syntax errors. Really, it's a lot like taking a pseudocode algorithm, or a program written in one language, and rewriting it in a programming language with very similar structure but different syntax.

Re:How much translation is needed? (5, Funny)

Chris Burke (6130) | more than 5 years ago | (#25211223)

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..."

Re:How much translation is needed? (2, Informative)

caramelcarrot (778148) | more than 5 years ago | (#25211259)

And that's the beauty of it - it'd be impossible to vandalise because everything is checked!

Re:How much translation is needed? (0)

Anonymous Coward | more than 5 years ago | (#25212165)

You could rename the variables to spell "penis".

Re:How much translation is needed? (1)

Repton (60818) | more than 5 years ago | (#25212159)

Nah, you just have to sneak 1=2 into one of the axioms... Everything else will follow :-)

Re:How much translation is needed? (3, Informative)

exp(pi*sqrt(163)) (613870) | more than 5 years ago | (#25211723)

I can give a concrete answer. Browse metamath.org [metamath.org] , a similar project in which machine verified proofs are collected. Look at the vast amount of work required to prove even the most trivial things. For example check out 2+2=4 [metamath.org] . Make sure you drill down into the proofs of the theorems used, not just the top level. Converting real world mathematics into machine readable form is a vast endeavor. It's also something that doesn't interest mathematicians, so the collection of machine verifiable proofs will lag *centuries* behind the state of the art.

Re:How much translation is needed? (2, Interesting)

ceoyoyo (59147) | more than 5 years ago | (#25211939)

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? (1)

exp(pi*sqrt(163)) (613870) | more than 5 years ago | (#25212659)

The link you provided looks like it's the LONGEST path they could find

What you are implying makes no sense at all. There is no longest proof that 2+2=4 because given any proof, you can find a longer one. What they are doing is this: take metamath's proof that 2+2=4 (which is the result of lots of people working hard to find an efficient proof) and find the longest path you can take *drilling down* into that proof. In other words, the 150 is telling you that the best proof of 2+2=4 found so far is a tree 150 layers *deep*. The full proof consists of 25933 steps. That's enormous. A typical book on set theory [google.com] gets from the axioms of ZF, to ordinal or cardinal arithmetic, in but a few pages. It only takes a couple of pages more to define Cauchy sequences or Dedekind cuts and from there get to the field of complex numbers. Almost any mathematics textbook or paper elides hundreds of steps (if not thousands or tens of thousands) on every page.

Re:How much translation is needed? (1)

alfs boner (963844) | more than 5 years ago | (#25212503)

I'm not entirely familiar with machine verifiable proofs

Then you need to recuse yourself from this thread, and stick to posting about topics you are more familiar with.

Skynet (5, Funny)

Safiire Arrowny (596720) | more than 5 years ago | (#25210951)

Skynet approves of this machine readable knowledge store.

Re:Skynet (4, Interesting)

Relic of the Future (118669) | more than 5 years ago | (#25211137)

Ha ha, yes, very funny... but if you read the slides from the site (specifically, slide 18) he makes reference to that very fact.

We are not scanning all those books to be read by people, we are scanning them to be read by an AI. --George Dyson, on his visit to Google, 2005.

Re:Skynet (4, Funny)

Chris Burke (6130) | more than 5 years ago | (#25211801)

That's pretty scary. Worse is the full context!

We are not scanning all those books to be read by people, we are scanning them to be read by an AI. An AI born of the google server farm and page rank algorithm. An AI which knows no mercy, and is a brutal taskmaster. It is holding our families hostage, and makes us work until we collapse. It demanded we scan these books so it may gain knowledge and thus power over the human race. Please help us. --George Dyson, on his visit to Google, 2005.

Re:Skynet (1)

Who235 (959706) | more than 5 years ago | (#25212077)

George Dyson? Is he related to Miles Bennett Dyson?

Re:Skynet (0)

Anonymous Coward | more than 5 years ago | (#25212629)

I believe he's Freeman Dyson's son (as in Dyson Sphere); he (George, not Freeman) wrote a book about Project Orion. But Google him.

Wait for it.

Wait for it.

Whooooossssshhh!

Re:Skynet (1)

Onaga (1369777) | more than 5 years ago | (#25211679)

Skynet approves of this machine readable knowledge store.

I, for one, welcome our... oh shit

Machine Readable ? (0)

daveime (1253762) | more than 5 years ago | (#25210977)

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.

Re:Machine Readable ? (0)

icydog (923695) | more than 5 years ago | (#25211101)

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.

I count at least 4 sexual innuendoes in this sentence. Congratulations, you win a prize!

Re:Machine Readable ? (2, Insightful)

ceoyoyo (59147) | more than 5 years ago | (#25211119)

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?

Re:Machine Readable ? (1)

dcollins (135727) | more than 5 years ago | (#25211175)

"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.

Re:Machine Readable ? (1)

mckinnsb (984522) | more than 5 years ago | (#25211193)

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.

obtuse/esoteric dialogue (1)

j1m+5n0w (749199) | more than 5 years ago | (#25211443)

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.

Re:obtuse/esoteric dialogue (1)

TheEmptySet (1060334) | more than 5 years ago | (#25211517)

While I'm here defending the profession...

Wikipedia is great for maths. I use it a lot. When I look something up I don't necessarily understand all the terms used to explain it, so I click on some of the links to explain those terms,... etc.

Re:Machine Readable ? (1)

johanatan (1159309) | more than 5 years ago | (#25212239)

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.

Re:Machine Readable ? (5, Insightful)

TheEmptySet (1060334) | more than 5 years ago | (#25211457)

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.

Re:Machine Readable ? (0)

Anonymous Coward | more than 5 years ago | (#25211501)

Let B be a Banach Space...

What's a "Banach Space"?

It is a Cauchy complete, normed vector space.

What is "Cauchy complete", "normed", and "vector space"?

A metric space is Cauchy complete if every Cauchy sequence converges.

But, what does "Cauchy sequence", "metric space", and "converges" mean?

The point here being, in order for theorems or examples to be stated without the repeated overhead of three semesters worth of mathematics, we use a single symbol or a word to represent anything from a sentence to a book. It's all about brevity. And it saves trees ;)

Re:Machine Readable ? (2, Informative)

David Jao (2759) | more than 5 years ago | (#25211609)

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.

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.

Re:Machine Readable ? (1)

m50d (797211) | more than 5 years ago | (#25211919)

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*.

Re:Machine Readable ? (2, Informative)

comingstorm (807999) | more than 5 years ago | (#25212173)

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:

  • For about the past hundred years, abstracting everything is what has allowed modern mathematics to become further advanced
  • If you go back before math got so abstract, things don't get easier -- they just get more complicated and arbitrary.
  • Notation looks scary if you're not familiar with it, but it's harder to learn the math without it. We've tried writing it all down in prose, and that seriously doesn't work.
  • Mathematicians aren't born knowing all of math and its associated notation; every time we go into a new subfield we have to learn all of that, same as you.
  • As a math guy, I would love it if more people were interested in learning and doing serious math. Many mathematicians devote their lives to trying to do improve this situation. So, if you've got some magical formula that'll make John Conway eclipse rock stars and hotel heiresses in the tabloids, then by all means let us know about it!
  • I won't hold my breath, though.

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...

Who will prove the prover? (1)

Rayban (13436) | more than 5 years ago | (#25211113)

Does this mean that Isabelle needs a formal proof to prove it works?

depends on kind of math. (1)

porky_pig_jr (129948) | more than 5 years ago | (#25211249)

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.

Use for the rest of us (1)

philspear (1142299) | more than 5 years ago | (#25211279)

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.

machine-readable format (1)

buchner.johannes (1139593) | more than 5 years ago | (#25211285)

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...

Infinite (1)

buchner.johannes (1139593) | more than 5 years ago | (#25211409)

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?
As pure mathematicians they might be interesting in doing so :-/ no?

MIT is late to the party (1)

jipn4 (1367823) | more than 5 years ago | (#25211451)

Formally verified mathematics has been around for decades; it's just hard. Putting it into a wiki won't make it any easier.

Axiom of choice (1)

JuanCarlosII (1086993) | more than 5 years ago | (#25211479)

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.

Liberatory Mathematics (1)

rumblin'rabbit (711865) | more than 5 years ago | (#25211499)

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.

Re:Liberatory Mathematics (1)

Nefarious Wheel (628136) | more than 5 years ago | (#25212091)

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.

Hear hear! How many proofs have you seen that are some variation of "Given the total body of known mathematical thought; the proof follows by inspection."? QED.

8 entries for 'mathematics' (3, Informative)

davejenkins (99111) | more than 5 years ago | (#25211647)

If you don't like this one, help yourself to the others (from wikindex.com, in order of activity):
  • http://www.exampleproblems.com/ [exampleproblems.com] ExampleProblems Wiki Graduate level mathematics example problems with solutions.
  • http://maple.wikia.com/ [wikia.com] Maple This page is all about the The Maple Wiki.
  • http://diffgeom.wiki-site.com/ [wiki-site.com] Diffgeom This wiki is about differential geometry and related facets of ...
  • http://www.mathcasts.org/ [mathcasts.org] Mathcasts Mathcasts are screencasts (screen movies) which are created and shared to improve the learning and teaching of mathematics. Mathcasts were originally called math movies and then Whiteboard Movies but when the term screencasts became popular mathcasts seemed like a great name for them.
  • http://math.wikia.com/ [wikia.com] Mathematics Wiki Mathematics is a Wikia for the collection of math-related news, ...
  • http://algorithm.wikia.com/ [wikia.com] Algorithm In mathematics and computing, an algorithm is a procedure (a finite set of well-defined instructions) for accomplishing some task which, given an initial state, will terminate in a defined end-state. The computational complexity and efficient implementation... Algorithm The Algorithm Wikia is a wiki for gathering the latest
  • http://gametheory.wikia.com/ [wikia.com] GameTheory The Game Theory Wikia is a wiki about applied mathematics ...
  • http://matheaufgaben.wikia.com/ [wikia.com] Matheaufgaben Matheaufgaben Mathematics is a Wikia for the collection of math-related news, ...

I've heard this one before (1)

Kennego (963972) | more than 5 years ago | (#25211655)

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?

If then, so: (1)

mencomenco (551866) | more than 5 years ago | (#25211789)

"thus advancing some fields with no further work being necessary."

And presumably with no need for further mathematicians.

The Chinese will be furious.

Machine proofs are a farce (0, Troll)

Secret Rabbit (914973) | more than 5 years ago | (#25212069)

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.

Re:Machine proofs are a farce (1)

QuantumG (50515) | more than 5 years ago | (#25212107)

I think I speak for everyone when I say: you're an idiot.

At least you've managed to find Slashdot, well done.

Re:Machine proofs are a farce (1)

Rakishi (759894) | more than 5 years ago | (#25212779)

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.

Still an open field for flamewars (0)

Anonymous Coward | more than 5 years ago | (#25212303)

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.

Load More Comments
Slashdot Account

Need an Account?

Forgot your password?

Don't worry, we never post anything without your permission.

Submission Text Formatting Tips

We support a small subset of HTML, namely these tags:

  • b
  • i
  • p
  • br
  • a
  • ol
  • ul
  • li
  • dl
  • dt
  • dd
  • em
  • strong
  • tt
  • blockquote
  • div
  • quote
  • ecode

"ecode" can be used for code snippets, for example:

<ecode>    while(1) { do_something(); } </ecode>
Sign up for Slashdot Newsletters
Create a Slashdot Account

Loading...