"Maths is Scruffy but Computable"

[gusl]

Edmund Furse's "Maths is Scruffy but Computable" is interesting, but not very rigorous

Some keywords:
* mathematics understanding
* experience-based learning
* learning heuristics


Here is his Why did AM run out of steam?

Comments

really?

[metaeducat10n.livejournal.com]

Goldbach's conjecture that every even number can be expressed as a sum of two primes.

Holy cow. Really?!

Oh. Wait, not proven.

So the AI came up with an idea it couldn't prove? That's odd.

Re: really?

[gustavolacerda.livejournal.com]

hm... I can't tell if you're being sarcastic.

I don't see anything odd about it.

Re: really?

[metaeducat10n.livejournal.com]

Surprise #1: Conjecture itself. I'd not suspect it to be true.

Surprise #2: Computer coming up with something that *might* be true but that it can't prove. 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. I suppose if you give it, in its list of axioms, other things that *might* be true then you could get this result, so perhaps not so strange.

Re: really?

[gustavolacerda.livejournal.com]

#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.