Proof and Computation
In general proof is something which is required during the development of a mathematical theory, e.g. complex analysis.
When it comes to application of the theory, proof is not generally called for.
In application computations or other problem solving methods are adopted which are justified by the theoretical results previously proven.
The standard of rigour adopted is perhaps slightly relaxed in applications.
Machines more easily cope with a mass of formal detail, but are not so good at informal methods.


The basic idea here is that by adapting merging compiler technology and proof technology we can effect a formal mechanisation of mathematics which combines the logical rigour of proof based techniques with the levels of automation and speed realised within their domains by numerical symbolic mathematical software.
This is a possible approach to the development of mathematical machine intelligence, but delivery of worthwhile functionality does not depend upon achieving artificial intelligence.


