[FOM] Formal verification

[WILLIAM TAIT]

On Oct 21, 2014, at 4:31 PM, Rempe-Gillen, Lasse <L.Rempe at liverpool.ac.uk> wrote:

> I for one would also be quite happy to make every beginning postgraduate student of mine - and perhaps also project undergraduate students - formalize some part of existing mathematics, assuming that there is a system that is easy enough to learn and use to make this feasible. In my view there is a real benefit to really having to understand a proof on this detailed level.

Without in the least questioning the value of having a foundation in terms of which one can formalize proofs, I think that maybe you are overstating its value in terms of the creation of new mathematics. Euler, for example, would likely have dropped out of your program (unless he just saw formalization of a particular proof or class of proofs, as just another challenging mathematical problem). Someone who looked to solve problems about the integers by introducing complex integers was not overly engaged with or bounded by foundational issues.

In particular, I worry about "there is a real benefit to really having to understand a proof on this detailed level." Benefit to whom? Again, our tidy souls (and mine) want foundations; but if you should ever be fortunate enough to have an Euler in your program, I bet you wont drive him/her away.

Bill