[FOM] Proof assistants and conjectures

[Steven Ericsson-Zenith]

On Jan 4, 2009, at 8:37 PM, Timothy Y. Chow wrote:

> ... However, from the point of view of knowledge management, it  
> would seem
> desirable to put down some stakes in the sand even in uncharted  
> territory,
> to prevent different pioneers from developing overly idiosyncratic
> dialects that later turn out to be extremely difficult to translate
> between.

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. 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.

This is not to say that your proposal has no merit, just that we must  
allow for thinking about the problem differently (whatever that may  
mean).

Sincerely,
Steven

--
	Dr. Steven Ericsson-Zenith
	Institute for Advanced Science & Engineering
	http://iase.info
	http://senses.info