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

[gustavolacerda.livejournal.com]

Btw, does the relevant concept of "high-level concepts" have any universality? Does it transcend our human-specific cognition?

I ask because I wonder whether our projects (the TUNES project as well as my project of bringing formal mathematics close to the level of human reasoning) are about human-computer interaction, or if they have a more fundamental nature as implementations of universal higher-level concepts (btw, I "believe" mathematics is universal, in spite of Lakoff).