Digital computers far outstrip any previous tool which mathematicians have used.
The man/machine combination does mathematics which could never have been achieved without the computer. Computers are so flexible and powerful that many people believe that they ought to be able to do the maths without our help, that computers will ultimately be intelligent mathematicians in their own right. |
The range of mathematical techniques which have been coded up for computers is very wide.
Computers have also been programmed to find and check mathematical proofs, and have been able to find and prove new mathematical results.
Nevertheless, computers remain primitive by comparison with the most ordinary human mathematician, and few believe that they have any mathematical intelligence. Whats holding them back? |
It looks like the development of mathematical software and the development of proof technology have been going their own ways to their mutual detriment. Maybe they should get together. |
The development of mathematical software has been going on for several decades now.
Whenever a systematic mathematical technique is available and well understood it is a routine matter to code this up in a suitable programming language and get a computer to implement the method.
This applies not just to numerical methods (which computers can apply much better than people) but also to symbolic manipulations.
Once upon a time doing symbolic mathematics was thought of as a problem in machine intelligence, but now an extensive range of techniques for symbolic differentiation and integration and other symbolic transformations are available in commercial software packages such as Mathematica.
The progress of mathematical software has involved extensive coding up of specific techniques for solving many different kinds of mathematical problem.
Where general techniques are available, covering a broad range of problems then they may be used, but where generic methods are not available or not effective, specific techniques will be used.
|
The automation of proof has predominantly been directed at mathematical problems.
In principle the use of a proof tool should broaden the range of problems which can be solved and should increase the reliability of the answers obtained.
However, research in this domain has generally attempted to solve mathematical problems without coding up mathematical knowledge into the proof system.
The expectation is that provision of a set of axioms sufficient for the mathematical domain in which the problem is posed will suffice to enable the machine to solve the problem.
Consequently the mathematical capabilities of proof tools are greatly inferior to those of non proof based mathematical software.
There are proof tool architectures (the LCF paradigm is one) which permit any amount of coding of domain specific techniques, but these have not yet been exploited on the scale necessary to make proof tools good at mathematics.
|
I don't know any reason why proof tools should not be made as good at mathematics as less rigorous mathematical software. Anyone care to offer me one? |