Re: if vs. when vs. and: style question

["Pascal J. Bourguignon" <pjb@informatimago.com>]

Óscar Fuentes <ofv@wanadoo.es> writes:

> Marcin Borkowski <mbork@wmi.amu.edu.pl> writes:
>
>>> Along the same lines, I don't know many programmers whose code is never
>>> passed to a compiler/interpreter but is instead only read by other
>>> human beings.
>>
>> BTW: I think you nailed a serious problem with contemporary mathematics:
>> that machine checking proofs isn't a routine part of the publishing
>> process.  The number of erroneous papers in math journals is
>> horrifying.  Substantial portion of my depatment's seminar is devoted to
>> discussing errors in papers.  Once a colleague found a relatively simple
>> /counterexample/ to a theorem which was a cornerstone of a whole theory
>> (and a basis for several dozen other papers).

Perhaps it's not pertinent in a specific case, but I'd see it as much as
a question of what axioms or inference rules would be needed to prevent
those counter examples, and thus validate the theory developed so far,
as the need to revise the validity of that theorem and its supposed
consequences.



> Yeah, that remembers me of Vladimir Voevodsky's story about why he
> always has a Coq session running nearby.
>
> OTOH I'm afraid that proof assistants can be a hindrance for creative
> work.


Perhaps they should work both way:  

- deduce consequences from axioms (or check deductions), and

- find axioms and deduction rules that would allow a given "chain of
  reasoning" to be a theorem.


If you only knew Euclidian geometry and imagined a triangle whose sum of
angles was 200 degree, you'd want a formal tool to help you infer
spherical geometry's axioms.


-- 
__Pascal Bourguignon__                 http://www.informatimago.com/
“The factory of the future will have only two employees, a man and a
dog. The man will be there to feed the dog. The dog will be there to
keep the man from touching the equipment.” -- Carl Bass CEO Autodesk