From: Ben Goertzel (ben@goertzel.org)
Date: Wed Nov 10 2004 - 22:37:10 MST
Christian,
Do you know the book "Where Mathematics Comes From?" by Lakoff and Nunez.
It explores the foundations of mathematical concepts in cognitive psychology
and embodied experience. I think it well summarizes the essence of what's
missing in contemporary theorem-proving technology. Mathematical proofs, as
created by humans, are guided by mathematical intuition, which is mostly
grounded in physical and linguistic intuition suitably abstracted. This
metaphorical grounding constrains our search through proof space, making
some valid proofs opaque to us but compensating but cutting through the
otherwise unmanageable combinatorial explosion. Without this sort of
grounding, mathematical theorem-provers have nothing to guide them but
generic search heuristics, which are far far far too inefficient to produce
nontrivial proofs without human guidance.
Thus I argue that, although theorem-proving may indeed be part of an AGI
system, getting advanced theorem-proving to work based on human-based
mathematics as an initial knowledge base requires a system that has a system
of internal schemata representing basic physical and linguistic phenomena
(measuring, grouping, building, continuous paths, etc. etc.). These
experientially grounded schemata are what will allow future
advanced-theorem-proving AGI's to create inductive and abductive hypotheses
that guide their deductive inference.
So advanced theorem-proving will emerge from embodied, experientially-savvey
AGI.
-- Ben G
> -----Original Message-----
> From: owner-sl4@sl4.org [mailto:owner-sl4@sl4.org]On Behalf Of Christian
> Szegedy
> Sent: Wednesday, November 10, 2004 6:41 PM
> To: sl4@sl4.org
> Subject: Re: Calculemus
>
>
> > This is interesting indeed, but I don't know of any work that makes this
> > practically useful, do you? If so I'd love to hear about it.
>
> I don't see its immediate relevance for AI. Note that the PCP is about
> checking of the correctness of proofs, not of conjectures.
>
> The constants in the PCP theorem are not astonomical and the degrees
> of the polynomials are small, so it could be practically feasible.
>
> The significance of the PCP theorem is mainly theoretical today: it
> is the base of almost all inapproximability results.
>
>
> > Yeah, but control theory totally falls apart when you start dealing with
> > situations of significant complexity.
>
> This sounds like an ad-hoc statement. Of course, as someone working on
> CAD systems for several years, I experience the gap between mathematically
> provable and practically efficient every day. Still, I also see that
> mathematically justified methods and mathematical insights lead to
> much better performance after additional tricking around than
> pure heuristics.
>
> > Is there more online information about Bless somewhere?
>
> BLess is in the implementation phase. The ideas are very
> stable, but there is no documenation yet. As soon as I release
> BLess 0.1, there will be a documenation.
> The only currently available resource is a short discussion
> on comp.lang.functional:
>
> http://www.talkaboutprogramming.com/group/comp.lang.functional/mes
sages/49357.html
This archive was generated by hypermail 2.1.5 : Tue Feb 21 2006 - 04:22:48 MST