reckless intuitions of an epistemic hygienist (![[info]](http://l-stat.livejournal.com/img/userinfo.gif){kind=small} gustavolacerda) wrote,@ 2005-07-25 14:23:00 |
|
| Entry tags: | formal_math |
computer-formalized math needs multiple representations, just like human mathematicians
I wish I had written this:
Manfred Kerber, Martin Polleti - On the Design of Mathematical Concepts
That foundational systems like first-order logic or set theory can be used to construct large parts of existing mathematics and formal reasoning is one of the deep mathematical insights. Unfortunately it has been used in the field of automated theorem proving as an argument to disregard the need for a diverse variety of representations. While design issues play a major rôle in the formation of mathematical concepts, the theorem proving community has largely neglected them. In this paper we argue that this leads not only to problems at the human computer interaction end, but that it causes severe problems at the core of the systems, namely at their representation and reasoning capabilities.
This is the main reason I don't like the mainstream approach to formalizing mathematics. On a previous post, I compared it to doing everything in assembly-language (even though people at Nijmegen don't mainly use lambda-terms, but more powerful tactics instead).
Kerber has also made slides, where he had made a point about representation with the clever problem of domino-tiling an NxN square missing 2 tiles at opposite corners.
