SCS Undergraduate Thesis Topics
|Brendan Meeder||Manuel Blum||Proof Triangles: Toward a Formal Theory of Mathematical Understanding|
Humans have developed great proficiency at creatively tackling mathematical problems. We seek to develop a computational model which encompasses many features of the human problem solving process. As a basic primitive for this model we have developed an object which we call a "proof triangle". A proof triangle for a theorem can be thought of as a triangle which has mathematical statements written on it. On its base the formal systems proof is written, and at the apex of the triangle are very short hints. The rest of the triangle is filled with more detailed hints which lead to a derivation of the formal proof. These objects encompass the knowledge required to guide an algorithm or human trying to solve the problem at hand, but not all information in a triangle may be required information.
In addition to providing a formal definition of a proof triangle system, we also develop formal definitions for concepts such as analogies and the extent to which an algorithm understands a theorem T and a proof P of the theorem. Our definitions approach these ideas from a complexity theoretic standpoint. We believe such methods will be useful in studying the broader problem of "understanding understanding."