>> But if you spend 20 years and millions of dollars to verify something
>> that is already known to be true, in what sense are you "demonstrating
>> the enormous usefulness of such a system"?
It seems to me that the long-range goal is not to verify one
specific theorem, but rather to construct a tool which
mathematicians in the future can use as a referee. This tool
should be 100% reliable (unlike human referees), and
easy and painless to use (unlike current verification systems).
I think that verifications (even if not painless) of individual hard
theorems are of interest primarily because they tend to indicate that this
long-range goal is attainable, eventually.
Ken Kunen