Here is the direct quote:

"In the calculational case, one’s typically dealing with an operation to be performed. In the Wolfram|Alpha-like pure mathematical case, one’s typically just giving a description of something. In some cases that description will be explicit. A specific number. A particular equation. A specific graph. But more often it will be implicit. It will be a set of constraints. One will say (to use the example from above), “Let F be a field,” and then one will give constraints that the field must satisfy.

But to really be useful in pure mathematics, there’s something else that’s needed. In addition to being able to deal with concrete mathematical objects, one also has to be able to deal with abstract mathematical structures. Countless pure mathematical papers start with things like, “Let F be a field with such-and-such properties.” We need to be able to enter something like this—then have our system automatically give us interesting facts and theorems about F, in effect creating a whole automatically generated paper that tells the story of F.

So what would be involved in creating a system to do this? Is it even possible? There are several different components, all quite difficult and time consuming to build. But based on my experiences with Mathematica, Wolfram|Alpha, and A New Kind of Science, I am quite certain that with the right leadership and enough effort, all of them can in fact be built."

Consider the exact example he gives of something Mathematica cannot represent - "Let F be a field with such-and-such properties". Consider the first axiom I have in my original post - "M3 is a metric space with a metric tensor g". From the point of view of level of abstraction, they seem to be similar.

Your example shows that theorem proving in possible using simple propositional calculus and first-order logic constructs. This is well known to me. However, my question is whether Mathematica can provide a True/False answer (which is a strictly weaker requirement than actually proving that answer. I would love to have a proof, but at this point I don't expect it) to statements involving abstract mathematical structures like fields. A first order logic statement does not involve abstract mathematical structures. From the above quotation, Wolfram's answer appears to be that this is not possible at present.

It seems that True/False answers involving arithmetic are possible. I was able to ask Mathematica if the square root of 2 is rational, and it replied with False, although I don't believe a proof can be generated at present. Theorema (an add-on package for Mathematica) should eventually be able to provide proofs of things like this, but cannot at present.

I would LOVE to be proved wrong. In fact, I posted this question hoping that I'll be proved wrong. But that would involve someone providing a Wolfram Language translation of say, the first axiom I provide. If someone knows of an add-on or different algebra system (Magma?) that makes this possible, I'd be delighted as well.

Take a look at the The Theorema System package.

Did anyone hear of Coq?

I do not know how it is possible, from my question, to conclude that I expect Mathematica to know all of mathematics, and prove the necessary theorems for every question that might be asked. It seems to me that I have presented 4 axioms, only 3 of which I have presented completely, and am asking if Mathematica can represent those 3, or even just one, of the axioms, in the Wolfram Language.

The obvious way to answer in the affirmative would be to provide a translation of one of those axioms. This would be very helpful to me, and I'd really appreciate it if someone could spare a few mins to do it (it probably wouldn't take more than a few mins for an expert).

Yes, I am asking if the Wolfram Language can represent the axioms of specific field (which is different from saying that I expect the axioms to be built into Mathematica - I am merely asking for the tools to program them in myself). The axioms I provided are 3 from about 20 axioms of the Newton-Poisson theory of gravitation, as formulated by Mario Bunge in his book "Philosophy of Physics" (1973).

I find it very interesting that the axiom system of Grassmann algebra can be represented in Mathematica, although that does necessarily mean that my axioms can. You also seem to suggest that you can deduce Euclidean theorems from the axioms. I like this idea a lot - could you please point me a publication where I can learn about it? Also, could you show me an axiom or two represented in the Wolfram Language, as illustrative examples?

Thanks!

This is an interesting question and discussion. If Atriya is asking if Mathematica can or could know all of mathematics and find, or prove on the fly, the necessary theorems for every question that might be asked, then I'm certain the answer is no.

But if something more modest is asked for, say representation of the structures and axioms of a specific field, then I think Mathematica can do a fairly good job. I've been working with John Browne on his Grassmann algebra and Grassmann calculus application. This is built up on an axiom system and the axioms are represented either in definitions or often in rules that are available and can be applied to symbolic expressions. Its applications are certainly limited to a specific area but that area is extremely broad, extending from simple exterior algebra to the generation of hyper-complex algebras including symbolic quaternions and octonions. Going back to the simple end, it's easy to use the algebra to prove Euclidean theorems. And, of course, it's useful in practical calculations.

So yes, the symbolic capabilities of Mathematica are very good - but you can't expect to start from zero, or encompass all possible mathematics.

Yes, it certainly seems to be. I was aware of it, but just wanted to confirm (by asking this question) that the kind of things I'm trying to do are indeed the ones Wolfram states (in the blog entry) that Mathematica cannot presently do.

In that case, my question is: is there any add-on to Mathematica, or an entirely different system (Magma, maybe?) which CAN do things like this? Theorema (mentioned above) might aspire to this end, but is in a very early stage of development, and not helpful to me as of now.