The aim of such an encylopedia would be twofold. First it would be a quick and easy reference to any mathematical concepts which come up (saving lots of time for anyone who's learning or using mathematics which is new to them), and as a base upon which to build complete computer-verifiable (and also human-readable) proofs, run automated proof-checkers, proof generators and conjecture generators.
Sound useful?
By 'encyclopedia of maths' I mean a large system of objects, each representing a mathematical idea such as a definition, theorem, proof, or even an explaination or article. Each of these is linked to the objects representing the ideas upon which it relies (either explicitly or implicitly). An object might be an axiom, a defintion, a theory, a theorem, a conjecture or a proof.
For example, a theorem object would probably contain
- a natural-language statement, with a reference to another object in the encylopedia for each technical term used.
- references to any proofs which are in the encyclopedia
- a machine-understandable statement of the result, again with references to every mathematical object involved.
- parhaps a natural-language comment, including information such as the source of the theorem, papers it appears in, the subject(s) that it forms a part of (with references as always).
Another useful feature of such a system would be a thesaurus. Mathematical notation varies wildly across the sciences (try comparing notation for groups used by physicists and mathematictians), so a quick and painless way to translate from one language/notation to another and back would allow people to actually read material written by people from a different discipline.
There's actually been quite a lot of work done on most of the components which would be required for such a system. To try and encourage more people to take an interest in this sort of project I'm putting up a little website about it (with lots of juicy links): An Encyclopedia of Mathematics