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

[fare.livejournal.com]

Actually, this is precisely what initially motivated my works on reflection: change in representation and relative foundations as a way to enable machines to interface to the concepts that mathematicians use, at as high-level as possible!

[troyworks.livejournal.com]

how is that going? sounds like interesting work.

TUNES

[fare.livejournal.com]

Not going much, these days. But things will start anew this november. See the TUNES project.

[gustavolacerda.livejournal.com]

yes! Again the analogy between programs and proofs. It feels good to clear up the old vision.

change in representation and relative foundations as a way to enable machines to interface to the concepts that mathematicians use, at as high-level as possible
Do you mean specifically mathematicians, or just programmers and users in general?

[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).

[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.

[darius.livejournal.com]

Have you looked at Ontic? I haven't, but the overview article claimed its proofs were higher level.

Re absoluteness, Raph Levien's been working on a proof system meant to accommodate different foundations so we could have a kind of WWW of formalized math.