Re: A mathematical assistant that you'd like?

On 31 Jan, 14:50, Arnold Neumaier <Arnold.Neuma...@xxxxxxxxxxxx>
wrote:
Ian Parker schrieb:





On 30 Jan, 10:18, Arnold Neumaier <Arnold.Neuma...@xxxxxxxxxxxx>
wrote:
What would be the kind of computer system that could take the role
of a general-purpose mathematical assistant to practicing
mathematicians? Which features should it have in order that you
would like to use it? What is necessary or desirable to make such
a mathematical assistant a routine tool?

How should it improve upon tools such as LaTeX (type-setting, no
contents checking), Mathematica (symbolic math, no proofs), or
Matlab (computations, no rigor) that are much used by mathematicians
today? How must it differ from the current generation of proof
assistants (rigorous but difficult to use) that are hardly used
by mathematicians, and not at all used by them for their daily work?

How much (and which) mathematics should such a system know and/or
make accessible to the user, and at which level of formality?

A - Make ALL levels available. Nothing else is sound. I will explain
my reasoning which is based on current AI trends.

Thanks for your view.

I feel that the question of proof and QED should be viewed in the
context of AI in more general terms. Here is a posting I have made in
"creatingAI".

http://groups.google.co.uk/group/creatingAI/browse_frm/thread/76177ac...

Mathematics has been described as a "language". This leads me onto the
type of assistant I would want. My assistant would have the whole of
mathematics encoded onto it. Isn't that a lot? Yes and no. In fact
proofs of virtually everything are available somewhere on the Web.
This effectively transforms our "proof" problem into a linguistics
problem. What we need is a spider that goes round looking at proofs,
and builds up a set of theorums.

This can be stated far more simple than it really is.
Otherwise it would have been done already.
There is lots on mathematical knowledge management,
   http://www.mkm-ig.org/
but people are only able to scratch the surface.

A theorem is, of course, simply a
sentence in our mathematical language.

How would you propose to cope with the problem that the same
mathematical result may exist in many variants differing slightly in
notation, phrasing, exact asssumptions?

I also have an idea about how such a language might me written. If you
have an online Arabic-English dictionary you look up words using a
hashing algorithm. Hashing algorithms, as we all know look up in a
constant time independently of the amount of information in them.
Could theorems be placed in a hashing algorithm?

How would you find the theorem that ''every number not leaving 7 as
remainder when divided by 8 is the sum of three primes'' in such a
dictionary?

I would write it
X>5;X%8!=7;X=P(1)+P(2)+P(3);

I am here using C++/Java rather than mathematical notation. In fact X
%8!=7 is irrelevant

X>5;X=P(1)+P(2)+P(3);

In fact X>3;X%2=0;X=P(1)+P(2)

is equivalent for

X%2=0 -> X-2 = P(1)+P(2)
X%2=1 -> X-3 = P(1)+P(2)

How would this be found using a hashing algorithm? Well, you would
modify an expression according to rules. The system would not find
X>5;X%8!=7;X=P(1)+P(2)+P(3); so it would try (say) X>5;X=P(1)+P(2)+P
(3); Bingo it would see that this was a form of Goldbach, although not
the most general form. Basically in QED we would have concepts. We
need to define a prime number. X%n!=0;n>1; is the obvious definition.
Any definition is assigned an integer code and (possibly) a class
where the rules are defined.

class Prime{
int n;
true(int);
};

ebool true(int i){
if(n<2)return possible;
if(n%i)==0)return false;else return possible;
}

These rules can be extended. We could use the more powerful x^
(p-1)%p=1, this would however not be a definition, but a theorem. A
vector to the proof would need to be given.

The fact that a lot of theorems appear in different forms and in
differing degrees of generality need not deter us too much. What you
would have to do is to include ALL manifestations of any theorem. The
most general manifestation would be the named theorem and all other
manifestations would simply have pointers to that theorem X=P(1)+P(2)+P
(3) would point to Goldbach.

http://en.wikipedia.org/wiki/Goldbach's_conjecture

http://projecteuclid.org/DPubS?service=UI&version=1.0&verb=Display&handle=euclid.facm/1229618748

and perhaps Goldbach would point to the Extended Riemann hypothesis.
The proof given in the reference above being made available. BTW - You
work at an academic institution, you will probable have access to the
body of the paper which I don't. Is it right? I can't say at this
stage.

http://en.wikipedia.org/wiki/Generalized_Riemann_hypothesis

The search routines employed by Google show that such a search
technique is possible. QED will need to use Sawzall.

http://en.wikipedia.org/wiki/Sawzall_(programming_language)
http://research.google.com/archive/sawzall.html

Each theorem, proof etc will be given a 64 bit address. I think we are
reasonably safe with 64 bits even with the whole of mathematics. The
assignment will be made by QED. The user just enters a theorem and (if
known) a proof. Just as you simply construct your website, you don't
worry about spiders and retrieval. In QED (ideally) you would have a
website, you would then enter something into your website. The spider
in addition to the task it performs at present of looking at words
would look for words that had meaning in QED. In QED a user would have
first to define what the quantities meant. For example :-

REAL x;
ROOT -> ax^2 +bx +c

would not have a solution if b^2 - 4ac was negative.

COMPLEX x; would however ALWAYS have roots. It might be possible to
use context to infer things about the quantities. Rigorously every
variable used has to have its properties defined strictly. A
statistical interpreter (or translator) could make this for you.

bsm Allh means "in the name of God" not "by poison God" although a
grammatical interpretation yields both. In the same way one might be
able to deduce what variables mean even if not stated. One should not
and QED should ask "Is this correct?"

If I said :- QED{

}

All the words would be interpreted in their mathematical sense. If I
said that Gaza was "compact" in the ordinary sense it would mean that
the area was small. In the mathematical sense it means a finite
covering which refers to the tunnels (holes in a 3 dimensional solid).
As you can see all this runs very much along the lines that Google has
already gone with its search engine. The thing that immediately struck
me about the Arabic Translation in

http://sites.google.com/site/aitranslationproject/deepknowled

Is that Google gets the Stephan Boltzmann law correct. Now concepts in
Physics will come under QED too. Google will look for QED words in a
text. Stephan Boltzmann Law is a unique QED expression. As I think I
have already said Web 3.0 will force Google to look for wrappers. A
QED word is in effect a wrapper. All that is required therefore for
radically improved translation is for the matching of wrappers.

Stephan Bolzmann{
DIMENSION MT^-3K^-4
}

Wikipaedia in fact gives Js^1m^-2K^-4 which is in fact the same
bearing in mind that J=MLT^-2L or ML^2T^-2. Quite clearly it cannot
translate K^-1! This is what has led me to think in terms of a
translation from QED to a natural language.

I think, and hope, mathematicians will be using QED to verify proofs.
Will they be the main users? Not necessarily. The "killer app" may be
something much more in the language translation and general AI area.
One should not bee too disappointed in this. After all QED is going to
have both pure and applied uses.

I mentioned Gaza for the following reason. Kurtzweil in a talk on AI
boasted that no Arabist had been involved in producing the world's
best machine translator. This may well have been born of necessity.
Google has an army of mathematicians and IT specialists to hand.
University departments of Middle Eastern studies have the job of
teaching people Arabic, notably journalists in the Middle East. This
presents considerable difficulties. No journalist ever says to himself
that the colours needed in Gaza are (7+√(1+48T))/2 where T is the
number of tunnels.

I would therefore regard the jury as being very much out on whether
knowledge of Arabic would improve the translation. What is absolutely
clear however is that swarm translation will dominate. QED needs a
swarm to make it effective. I think that earlier work has failed
because the technology was not there. It is today. It seems probable
that automatic checking of a translation using QED.

We can see that the whole theory of QED is inextricably linked with
concepts of search and machine translation. Google is in fact
providing an API for researchers and perhaps they could be induced to
sponsor some research. Success would certainly improve their
technology so there is no reason why they should not cooperate.

I have put concepts in C++. Clearly QED must be written in MANIFOLD
http://www.ercim.org/publication/Ercim_News/enw35/arbab.html which can
coordinate tasks in C++ and Java. There is one othee role for our
assistant, and that is to write programs. We need to specify
something, perhaps in words and a program written. If every module has
a QED definition this should be possible.




Trying the words in google or scholar.google turned up nothing of
direct interest.

(Trivial for things like Calculus
and Matrix theory)

Not even elementary number theory is trivial. See, e.g.,
    C. Zinn,
    Understanding Mathematical Discourse
   http://citeseerx.ist.psu.edu/viewdoc/summary?doi=10.1.1.44.8407

I think this is because the right keywords are not there (Yet)

I have given you a lot to think about. I will probably publish this
all in a blog some time.


- Ian Parker
.