[FOM] Proof assistants and conjectures
Timothy Y. Chow
tchow at alum.mit.edu
Wed Jan 7 18:05:09 EST 2009
Steven Ericsson-Zenith wrote:
>I would be extremely cautious when attempting this sort of normalization
>for fear that we would put in place such constraints that pioneering
>would become impossible.
A fair point. However, pioneering would never be *impossible*. You could
always make up whatever new concepts you wanted. The requirement would
just be that you make contact with pre-existing concepts.
>If such translations were to be as difficult as you fear, then this would
>likely be good news, for then there is a greater chance that cases of
>merit really are pioneering.
Hmmm...it's hard to be sure in advance, but I very much doubt that
difficulty of translation would be a good sign. As others have pointed
out, there is already difficulty of translation between the various
existing proof assistants. Is this good news? Surely not.
Even within a fixed system, difficulties of translation are most likely to
arise not because of extreme originality and novelty of thought, but
because of the accumulation of seemingly trivial issues. Are graphs
special cases of multigraphs, or a different type altogether? Is the zero
ring a ring? Can I think of a curve as a variety or does it have to be a
scheme? I can imagine going for years thinking that a word means one
thing when it really means something else, because I rarely deal with the
cases where the difference matters---until it's kind of late in the game
and I've built lots of stuff around my misunderstanding.
These problems can't be eliminated entirely, but they can be reduced by
careful advance planning.
More information about the FOM