[FOM] formal proofs

[Hendrik Boom]

On Wed, Oct 22, 2014 at 10:31:34AM +1030, David Roberts wrote:
> Hi Tim,
> 
> If the Mizar community, or any other formal proof community, could
> prove this theorem formally in two years, I for one would tip my hat
> to them, and reconsider my position, which is the same as Urs', that
> traditional membership-based formal systems make for impractical
> formalised proofs.

Could it be that, against all expectations, type theory is closer than 
set theory to the way that mathematicians think?  The main things that 
Coq provides are sophisticated forms of abstraction.  And, oh yes, a 
few data structures.

Or maybe it's just close to the way homotopy theorists think?

Are different formal systems appropriate to different kinds of 
mathamatics?

-- hendrik