Science is a human activity (was: Python syntax in Lisp and Scheme)

[David Eppstein]

In article <1jclovopokeogrdajo6dfmhm090cdllfki at 4ax.com>,
 Michele Dondi <bik.mido at tiscalinet.it> wrote:

> >It's certainly true that mathematicians do not _write_
> >proofs in formal languages. But all the proofs that I'm
> >aware of _could_ be formalized quite easily. Are you
> >aware of any counterexamples to this? Things that
> >mathematicians accept as correct proofs which are
> >not clearly formalizable in, say, ZFC?
> 
> I am not claiming that it is a counterexample, but I've always met
> with some difficulties imagining how the usual proof of Euler's
> theorem about the number of corners, sides and faces of a polihedron
> (correct terminology, BTW?) could be formalized. Also, however that
> could be done, I feel an unsatisfactory feeling about how complex it
> would be if compared to the conceptual simplicity of the proof itself.

Which one do you think is the usual proof?
http://www.ics.uci.edu/~eppstein/junkyard/euler/

Anyway, this exact example was the basis for a whole book about what is 
involved in going from informal proof idea to formal proof: 
http://www.ics.uci.edu/~eppstein/junkyard/euler/refs.html#Lak

-- 
David Eppstein                      http://www.ics.uci.edu/~eppstein/
Univ. of California, Irvine, School of Information & Computer Science