# Towards a Wiki For Formally Verified Mathematics

#### kdawson posted about 6 years ago | from the preparing-the-ground-for-our-robot-overlords dept.

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

## Uh ... (2, Insightful)

## David Gerard (12369) | about 6 years ago | (#25210921)

1. Bertrand Russell's

Principia Mathematicagot there first.2. Godel proved the endeavour was impossible.

I'm amazed a mathematician proposed this.

## Re:Uh ... (4, Funny)

## johannesg (664142) | about 6 years ago | (#25210961)

So Godel proved that Russell was wrong, then?

## Re:Uh ... (2, Interesting)

## mckinnsb (984522) | about 6 years ago | (#25211075)

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) | about 6 years ago | (#25211155)

## Re:Uh ... (5, Informative)

## zacronos (937891) | about 6 years ago | (#25211841)

eitherbe 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) | about 6 years ago | (#25211997)

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) | about 6 years ago | (#25212115)

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) | about 6 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) | about 6 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) | about 6 years ago | (#25211913)

## Re:Uh ... (2, Informative)

## Free the Cowards (1280296) | about 6 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 | about 6 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) | about 6 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 proofsfor submitted theorems. For some reason people see machine verification and fly off into nonsense la-la land. Butverifyinga 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) | about 6 years ago | (#25212525)

## Re:Uh ... (0)

## Anonymous Coward | about 6 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) | about 6 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

allmathematical truths. But working through what isknownand 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) | about 6 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) | about 6 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 | about 6 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) | about 6 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) | about 6 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

knownmathematics and use automated theorem proving to do some advances.## Re:Uh ... (0)

## Anonymous Coward | about 6 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) | about 6 years ago | (#25212139)

knownmathematics 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) | about 6 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) | about 6 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) | about 6 years ago | (#25211015)

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

## Re:Uh ... (1)

## DriedClexler (814907) | about 6 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) | about 6 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) | about 6 years ago | (#25212189)

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 | about 6 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 | about 6 years ago | (#25212287)

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 trueabout 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) | about 6 years ago | (#25211061)

## Re:Uh ... (0)

## Anonymous Coward | about 6 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) | about 6 years ago | (#25211811)

Any given mathematical fact falls into one of three categories:

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

provingfacts, it is merelyverifyingthe 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) | about 6 years ago | (#25210931)

## Re:Godel (1)

## mathmathrevolution (813581) | about 6 years ago | (#25211027)

## Re:Godel (4, Funny)

## Free the Cowards (1280296) | about 6 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 | about 6 years ago | (#25211735)

Next case: Gordon Bennet vs English language

## Re:Godel (0, Flamebait)

## Silicon Jedi (878120) | about 6 years ago | (#25211885)

## Re:Godel (1, Funny)

## Anonymous Coward | about 6 years ago | (#25211219)

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

## How much translation is needed? (1)

## caramelcarrot (778148) | about 6 years ago | (#25210943)

## Re:How much translation is needed? (1)

## ceoyoyo (59147) | about 6 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) | about 6 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) | about 6 years ago | (#25211259)

## Re:How much translation is needed? (1)

## Chris Burke (6130) | about 6 years ago | (#25211743)

Maybe if I added the "Miracle Axiom"?

## Re:How much translation is needed? (1)

## ijakings (982830) | about 6 years ago | (#25211751)

Ah but all checkers recognise that

1) Math

2) ???

3) Profit

Must be true

## Re:How much translation is needed? (0)

## Anonymous Coward | about 6 years ago | (#25212165)

You could rename the variables to spell "penis".

## Re:How much translation is needed? (1)

## Repton (60818) | about 6 years ago | (#25212159)

Nah, you just have to sneak :-)

1=2into one of the axioms... Everything else will follow## Re:How much translation is needed? (1)

## badboy_tw2002 (524611) | about 6 years ago | (#25212559)

You'll probably want a machine readable code for your statement. I suggest "???".

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

## Cyberax (705495) | about 6 years ago | (#25211283)

It's a pretty much work. A lot of 'obvious' English sentences translate to bulky code for proof verifier.

Just look at the definition of Peano arithmetic, for example: http://pauillac.inria.fr/coq/V8.1/stdlib/Coq.Arith.Plus.html [inria.fr]

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

## exp(pi*sqrt(163)) (613870) | about 6 years ago | (#25211723)

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

## ceoyoyo (59147) | about 6 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) | about 6 years ago | (#25212659)

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) | about 6 years ago | (#25212503)

I'm not entirely familiar with machine verifiable proofsThen 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) | about 6 years ago | (#25210951)

## Re:Skynet (4, Interesting)

## Relic of the Future (118669) | about 6 years ago | (#25211137)

## Re:Skynet (4, Funny)

## Chris Burke (6130) | about 6 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) | about 6 years ago | (#25212077)

George Dyson? Is he related to Miles Bennett Dyson?

## Re:Skynet (0)

## Anonymous Coward | about 6 years ago | (#25212629)

Wait for it.

Wait for it.

Whooooossssshhh!

## Re:Skynet (1)

## Onaga (1369777) | about 6 years ago | (#25211679)

Skynet approves of this machine readable knowledge store.

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

## Machine Readable ? (0)

## daveime (1253762) | about 6 years ago | (#25210977)

the wiki will state all of known mathematics in a machine-readable languageI'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) | about 6 years ago | (#25211101)

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

## Re:Machine Readable ? (2, Insightful)

## ceoyoyo (59147) | about 6 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) | about 6 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) | about 6 years ago | (#25211193)

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) | about 6 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) | about 6 years ago | (#25211517)

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) | about 6 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) | about 6 years ago | (#25211457)

## Re:Machine Readable ? (0)

## Anonymous Coward | about 6 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) | about 6 years ago | (#25211609)

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) | about 6 years ago | (#25211919)

## Re:Machine Readable ? (2, Informative)

## comingstorm (807999) | about 6 years ago | (#25212173)

instead of abstracting everything and assuming everyone knew as much as them [...] resent the way mathematicians try to maintain their elitist cliqueUmm... parent article is so many flavors of wrong I don't know where to start, so I'll just tick off some things:

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

## What? (1)

## moniker127 (1290002) | about 6 years ago | (#25210981)

## Yay! Truth Mines! (2, Informative)

## seanellis (302682) | about 6 years ago | (#25210987)

What? You haven't read

Diasporaby Greg Egan? Shame on you!## Re:Yay! Truth Mines! (1)

## treeves (963993) | about 6 years ago | (#25212769)

BJ and the Bear, with Greg Evigan. Does that count?## Who will prove the prover? (1)

## Rayban (13436) | about 6 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) | about 6 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.

## Zombie David Hilbert... (1)

## weston (16146) | about 6 years ago | (#25211449)

... laughs at your difficulties.

(but is afraid of zombie Kurt Gödel.)

## Use for the rest of us (1)

## philspear (1142299) | about 6 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) | about 6 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...

## Does this mean I can use Isabelle.. (1)

## QuantumG (50515) | about 6 years ago | (#25211315)

without EMACS? Now

thatis progress.## Infinite (1)

## buchner.johannes (1139593) | about 6 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? :-/ no?

As pure mathematicians they might be interesting in doing so

## MIT is late to the party (1)

## jipn4 (1367823) | about 6 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) | about 6 years ago | (#25211479)

## Liberatory Mathematics (1)

## rumblin'rabbit (711865) | about 6 years ago | (#25211499)

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) | about 6 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.

## vapourware (1)

## QuantumG (50515) | about 6 years ago | (#25211565)

I sounds like a great idea. So, umm, do it.

## 8 entries for 'mathematics' (3, Informative)

## davejenkins (99111) | about 6 years ago | (#25211647)

## I've heard this one before (1)

## Kennego (963972) | about 6 years ago | (#25211655)

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) | about 6 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.

## Been doing this since 2001, someone plz vote me up (1)

## adougher9 (1092141) | about 6 years ago | (#25211889)

## Re:Been doing this since 2001, someone plz vote me (1)

## adougher9 (1092141) | about 6 years ago | (#25212029)

## Machine proofs are a farce (0, Troll)

## Secret Rabbit (914973) | about 6 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) | about 6 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)

## Secret Rabbit (914973) | about 6 years ago | (#25212499)

And for not saying why, that makes you what again?

## Re:Machine proofs are a farce (2, Funny)

## QuantumG (50515) | about 6 years ago | (#25212683)

A smug bastard who would rather point and laugh at you than educate?

## Re:Machine proofs are a farce (1)

## Rakishi (759894) | about 6 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 | about 6 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.

## But is it reliable? (1)

## yafujifide (716502) | about 6 years ago | (#25212601)