![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
Y Combinator
Mar. 7th, 2007 03:29 pmI'm surprised I haven't heard any CMU undergrads talking about http://www.ycombinator.com/ . Business plans are due April 2.
Mar. 7th, 2007
I just had a half-hour chat with Hannes Leitgeb.
At noon, he gave a very interesting talk on formalizing the notion of informal provability (in which he expressed the Penroseish view that human intelligence may mean that may some steps in mathematical proofs may be unformalizable, or at least that the AI required for proof-checking this a single step would be very hard to implement). If that happens, this would create an interesting application for human computation.
A cognitive science of math must be about cognitive representations: what data structures do people have in their heads? (It should also address questions like "Why are definitions useful?") He suggests using these data structures as a way of modeling intuition (a belief is intuitive if it's a frequently-observed pattern). He used Steve's face as an example of a cognitive representation. The way we draw and talk about diagrams illustrates what features are relevant (i.e. essential to our cognitive representations), and which ones are irrelevant (e.g. the size of the drawing).
Our private conversation was mostly about his other work. I learned that Carnap's "The Logical Structure of the World" is about translating all statements into statements about sense experience. This reminded me of Hartry Field's "Science without Numbers", which is about doing science without abstracta. They are both analogous to cut-elimination (i.e. translating your proofs so that they don't use definitions). Apparently, for Carnap, the focus is not as much on ontology as for Field.
He also referenced some interesting work about proof transformations directed at changing the genus of the natural deduction proof graph, although I don't remember how this fits with the rest of the talk.
--
I told him about my ideas regarding formalized math.
Given a corpus of computer-formalized proofs, can we learn to automatically make them more readable, either by summarizing them, or by adding higher-level structure (as desired by people in MKM)? (in both cases, an interesting machine learning project)
Can we teach computers to read math papers? (i.e. either into a formal system, or into informal human-like representation... although we would ideally like to integrate these two)
In both of the above questions, I think the most important factor is: how much background knowledge do we need to give the computer? This is the same question that we face with the SimStudent project.
It seems no-one is working on automatic reading of math texts. This work would involve reconstructing human-like cognitive representations of mathematics. Undergraduate-level number-theory is probably a good place to start with. Introductory group theory would probably be boring, because most proofs are almost formal already.
It seems to me that making math-reading AI is hard because formalization of math is hard.
Generally speaking, formalization is hard because of:
* the ubiquity of mathlore: retrieving the needed facts is time-consuming.
Maybe what I need is to do task analysis on formalization work. But that may be too hopeful.
At noon, he gave a very interesting talk on formalizing the notion of informal provability (in which he expressed the Penroseish view that human intelligence may mean that may some steps in mathematical proofs may be unformalizable, or at least that the AI required for proof-checking this a single step would be very hard to implement). If that happens, this would create an interesting application for human computation.
A cognitive science of math must be about cognitive representations: what data structures do people have in their heads? (It should also address questions like "Why are definitions useful?") He suggests using these data structures as a way of modeling intuition (a belief is intuitive if it's a frequently-observed pattern). He used Steve's face as an example of a cognitive representation. The way we draw and talk about diagrams illustrates what features are relevant (i.e. essential to our cognitive representations), and which ones are irrelevant (e.g. the size of the drawing).
Our private conversation was mostly about his other work. I learned that Carnap's "The Logical Structure of the World" is about translating all statements into statements about sense experience. This reminded me of Hartry Field's "Science without Numbers", which is about doing science without abstracta. They are both analogous to cut-elimination (i.e. translating your proofs so that they don't use definitions). Apparently, for Carnap, the focus is not as much on ontology as for Field.
He also referenced some interesting work about proof transformations directed at changing the genus of the natural deduction proof graph, although I don't remember how this fits with the rest of the talk.
--
I told him about my ideas regarding formalized math.
Given a corpus of computer-formalized proofs, can we learn to automatically make them more readable, either by summarizing them, or by adding higher-level structure (as desired by people in MKM)? (in both cases, an interesting machine learning project)
Can we teach computers to read math papers? (i.e. either into a formal system, or into informal human-like representation... although we would ideally like to integrate these two)
In both of the above questions, I think the most important factor is: how much background knowledge do we need to give the computer? This is the same question that we face with the SimStudent project.
It seems no-one is working on automatic reading of math texts. This work would involve reconstructing human-like cognitive representations of mathematics. Undergraduate-level number-theory is probably a good place to start with. Introductory group theory would probably be boring, because most proofs are almost formal already.
It seems to me that making math-reading AI is hard because formalization of math is hard.
Generally speaking, formalization is hard because of:
* the ubiquity of mathlore: retrieving the needed facts is time-consuming.
Maybe what I need is to do task analysis on formalization work. But that may be too hopeful.