![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
guslThere 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.
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.
![[identity profile]](https://www.dreamwidth.org/img/silk/identity/openid.png){kind=small}
(no subject)
Date: 2004-11-19 02:54 pm (UTC)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.