[FOM] Proof assistants and conjectures

[Timothy Y. Chow]

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.

Tim