why current formal mathematics is different from real human mathematics

[gusl]

There are many languages for formal mathematics, e.g. Coq, Mizar, HOL, Isabelle, but they often don't correspond to mathematicians' cognitive structures.

This is for the following reasons:

* these proofs are currently too low-level (proof plans, proof sketches are possible solutions to this)
* They don't model multiple representations, or semantics (humans integrate algebraic & geometrical reasoning)
* They work from absolute mathematical foundations. As we know, real mathematics existed way before it was given good foundations. Human mathematicians work with relative foundations.

Comments

[troyworks.livejournal.com]

I'd say that many computer languages in general are a poor overlap with cognitive structures.

I'm trying to tackle one aspect of that with semantic/fuzzy databases for a site I'm building.