computer-formalized math needs multiple representations, just like human mathematicians

[gusl]

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.

Comments

[williamallthing.livejournal.com]

yo gus, any chance of you going being in the states any time soon? was driving past beacon hill yesterday and thinking of our adventures (murray has long since moved). i miss your unique brand of wacky hijinks! come visit ca! -w

[gustavolacerda.livejournal.com]

hey William, I can hardly believe it's already been 3 years since I left Boston! I definitely intend to visit CA when I get my life in order financially... or maybe move to CA to get my life in order financially.
wacky hijinks?! you'll have to remind me.

[rdore.livejournal.com]

Historically, it seems people were tying to formalize mathematical reasoning so that they could prove things about what could and could not be reasoned. From this point of view it is ideal to have as smiple of a system as possible - A simple system is generally more easy to argue about.

This is one of the nice things about doing math - you can easily tack together many layers of abstraction that to do out computationally or even totally formally would be a huge mess. Of course this also makes automating math harder.

[gustavolacerda.livejournal.com]

This is one of the nice things about doing math - you can easily tack together many layers of abstraction that to do out computationally or even totally formally would be a huge mess. Of course this also makes automating math harder.

Yes. But if a human mind can quickly verify that a mathematical step follows, then there should be a way of formalizing that computationally that is *not* a huge mess.

My assumption is that the cognitive processes used in mathematical reasoning correspond to relatively simple computations. The hard part is creating the logical framework and the software to do integrate the different meta-levels of reasoning. And I'm not even sure if it's that difficult.

[rdore.livejournal.com]

But if a human mind can quickly verify that a mathematical step follows, then there should be a way of formalizing that computationally that is *not* a huge mess.

Sure, but if I say something like "by a straightforward compactness argument" (in the context of model theory), this means you need to automate which constants and formulas to add, and how to pick witnesses for each finite set and so forth. Now maybe for this concept you can do it, perhaps even in a nice and elegant way. But there are thousands of concepts like this. If you're asking for a meta-framework to handle these many concepts, well that sounds like a hard problem. (But also one which sounds quite useful to solve.)