Overview:

A short story about the mechanisation of mathematics. Its primary purpose is speculation about what could be done, and how, but there's a bit of background material about what has been done.

paradigms The discussion hangs around three paradigms for mathematical software, numeric, symbolic and logical. The first two are already mature, the third is speculative. Each of these paradigms more or less subsumes the previous one, in terms of its capabilities, with a couple of exceptional aspects which we will mention, both connected with rigour.

logical power When it comes to the logical paradigm, I want to distinguish two levels of capability. I associate these with the terms engineering logic and intelligent logic. The second is what you get if you manage (in this restricted logical domain) to crack the machine intelligence problem. I consider how to do engineering logic in a way which is sympathetic to, but independent of, intelligent logic.

numeric:

The predominant area of application of computers to mathematics is in brute numeric computation.

Alongside sorting punched cards this is what computers were invented for, and what they have been used for from the very beginning. Computerised numerical computation is used not only where a mathematician would otherwise have computed by hand or by calculator, but also for problems that would without computers have been inconceivable, and also to solve by brute force problems which a mathematician would solve with more intelligence and less computation (e.g. numerical integration).

Numerical Analysis Numerical analysis is concerned with the computational application of mathematical theories built on the real number system, mainly to problems in science and engineering. For example, numerical integration involves computing the value of some mathematical function at many points and adding these together to obtain a value for the area under the curve of the function, which may correspond to some useful physical quantity such as a distance travelled by a projectile.

Discrete Mathematics Involves integers rather than real numbers and is most conspicuous these days for its cryptographic applications.

Software Paradigm Mainly non-interactive programs taking numeric data input and yielding numeric results. Problems in this area are often solved by custom programs written in languages such as Fortran or C by applied mathematicians scientists or engineers who understand the problem domain.

Computing with Real Numbers Numerical analysis should strictly involve computations with real numbers, but since real numbers are hard to represent in computers its usual to settle for floating point numbers. The practical implications of this seem modest, but it becomes a more significant problem if numeric computation is to be integrated into a more rigorous mathematical environment.

symbolic:

The most versatile modern mathematical software is symbolic. Packages like Mathematica not only crunch numbers but also transform mathematical formulae.

Symbolic Mathematics Much of the work of mathematicians involves symbolic transformation of mathematical expressions. When confronted with an integral, a mathematicians first thought would be to obtain a symbolic expression for the value of the integral rather than to undertake numerical integration. This has the advantage of better efficiency, accuracy and re-usability.

Software Paradigm Symbolic mathematics tools such as Mathematica provide an interactive environment with a special programming language oriented towards manipulation of symbolic expressions. A rich library of numerical and symbolic functions is provided, which are used to evaluate or simplify expressions entered. The user can extend the environment by defining new mathematical functions or new ways of transforming mathematical expressions.

Rigour Deficit Symbolic mathematics tools provide good support for the application of mathematics, but the don't know about proof, and don't really know about truth either. So they will blindly accept new transformation rules without regard to the soundness of the transformation. As mathematical assistants, they are agile. and smarter than numeric software, but still, basically, dumb. To get smart you need rigour, and to get rigour you need logic.

logical:

The final stage is to build mathematical tools on a proof technology base so that they are in a position to reason about the problems they are given, can comprehend and check mathematical proofs, and maybe eventually come up with intelligent solutions to non-routine problems.

If you throw large amounts of computing power at the solution of mathematical problems its not going to be practical (in general) to check that the machine hasn't made an error. You have to be able to write mathematical software which is reliable. Software which "understands" the formal foundations of mathematics and is able to enforce rigour on itself is one approach to solving this problem.

One of the basic motivations behind the Formalised Mathematics is to make practical the kind of rigour in the development of mathematics which was demonstrated by Principia Mathematica but has ever since seemed too much work for too little benefit. The idea is that formal proofs could become the accepted standard of rigour in the development of new mathematics if computers were able to do the donkey work in constructing and checking the detailed formal proof.

"Engineering Logic" is the name I have adopted for the enterprise of using the technology of formalised mathematics as a basis for the development of rigorous symbolic mathematical tools which are capable of delivering similar functionality to that provided by today's symbolic tools + rigour. I conjecture that by a substantial engineering effort this sort of capability could be realised without dependence on research advances in artificial intelligence.

"Intelligent Logic" is the name I have adopted for the pie-in-the sky project of realising an intelligent mathematical assistant by gradual evolutionary extension of the mathematical capabilities of "Engineering Logic" based tools. This would be a distributed open-source project, delivering a distributed intelligence and is a subtheme of:

created 1995/10/29 modified 1998/8/28