## Abstract

Progress in the foundations of mathematics has made it possible to formulate all thinkable mathematical concepts, algorithms and proofs in one language and in an impeccable way. This is not in spite of, but partially based on the famous results of Gödel and Turing. In this way statements are about mathematical objects *and* algorithms, proofs show the correctness of statements *and* computations, and computations are dealing with objects *and* proofs. Interactive computer systems for a full integration of defining, computing and proving are based on this. The human defines concepts, constructs algorithms and provides proofs, while the machine checks that the definitions are well formed and the proofs and computations are correct. Results formalized so far demonstrate the feasibility of this ‘computer mathematics’. Also there are very good applications. The challenge is to make the systems more mathematician-friendly, by building libraries and tools. The eventual goal is to help humans to learn, develop, communicate, referee and apply mathematics.

## Footnotes

One contribution of 13 to a Discussion Meeting Issue ‘The nature of mathematical proof’.

↵One of these referees told us the following. ‘If an ordinary non-trivial mathematical paper contains an interesting idea and its consequences and obtains ‘measure 1’, then Wiles' proof can be rated as having measure 156.’

↵In predicative sytems a subset of an infinite set

*X*can only be defined if one does not refer to the class of all subsets of*X*. For example is allowed, but not↵By ‘rational integers’ Hilbert just meant the set of integers . This problem is equivalent to the problem over . The solvability of Diophantine equations over is still open.

↵This definition scheme was generalized by Scott (1970) to inductive types. For example over the binary trees introduced above one can define a primitive recursive function mirror as follows.It mirrors the tree displayed above.

↵Previously called (

*total*)*recursive functions*.↵For substantial computations one needs to introduce decimal (or binary) notation for numbers and prove that the operations on them are correctly defined. In the history of mathematics it was al-Khowàrizmì (780–850) who did not introduce algorithms as the name suggests, but proved that the well-known basic operations on the decimal numbers are correct.

↵Here ‘!’ stands for ‘∀’ and ‘\’ stands for ‘λ’.

↵Structurally this last version is what one would like to write, but typographically it still is not ideal. Perhaps one day it will be possible to use in a proof assistant a mathematical style like in † above or, at least, the LaTeX source for it.

↵In this proof ‘

`limit_in1 f D l x0`’ is the Coq notation for where*x*ranges over the set .↵Actually, this is a mixture of Mizar and Coq. The proof language is Mizar, but the statements are written in Coq syntax. We do this to be able to follow the Coq script very closely.

↵Another difference was that in Nijmegen we formalized an intuitionistic proof, while Harrison formalized a classical proof. But when analysing the formalizations, it turned out that this was not the main reason for the difference in work needed.

↵Indeed if every theorem of length

*n*would have a proof of length , then theorem-hood would be decidable by checking all the possible candidate proofs.- © 2005 The Royal Society

Sign in for Fellows of the Royal Society

Fellows: please access the online journals via the Fellows’ Room

Not a subscriber? Request a free trial

### Log in using your username and password

### Log in through your institution

Pay Per Article - You may access this article or this issue (from the computer you are currently using) for 30 days.

Regain Access - You can regain access to a recent Pay per Article or Pay per Issue purchase if your access period has not yet expired.