#1: It goes against my intuitions too. I could do some empirical work, see how the location of the prime pairs changes, etc... and maybe I'd get some intuition that way.
Usually I think of a computer's reasoning as being intrinsically drawn up from axioms in such a way that its thought process would essentially be a proof.
This is indeed the mainstream way to work in automated reasoning. But it's too constraining. Working mathematicians need to work with heuristics, construct a few concrete examples, etc. When they come across proof failure or contradictions, they deal with it by redefining concepts, weakening or restricting their hypotheses, etc... none of which are in the scope of the traditional approach. There is also the aspect of multiple representations (e.g. simultaneously algebraic and geometrical), which most people in AR don't care to work with.
Alan Bundy and his followers are building AI that is closer to human mathematicians in these ways. Besides them, there are people who do model-based reasoning (i.e. draw conclusions by looking at some examples), and representations that can model e.g. geometrical reasoning.
Anyway, you can see I'm ranting. This is obviously one of my favourite ideas to evangelize.
![[personal profile]](https://www.dreamwidth.org/img/silk/identity/user.png){kind=small}
krja
Re: really?
Date: 2006-09-04 05:49 am (UTC)This is indeed the mainstream way to work in automated reasoning. But it's too constraining. Working mathematicians need to work with heuristics, construct a few concrete examples, etc. When they come across proof failure or contradictions, they deal with it by redefining concepts, weakening or restricting their hypotheses, etc... none of which are in the scope of the traditional approach. There is also the aspect of multiple representations (e.g. simultaneously algebraic and geometrical), which most people in AR don't care to work with.
Alan Bundy and his followers are building AI that is closer to human mathematicians in these ways. Besides them, there are people who do model-based reasoning (i.e. draw conclusions by looking at some examples), and representations that can model e.g. geometrical reasoning.
Anyway, you can see I'm ranting. This is obviously one of my favourite ideas to evangelize.