**From:** Ben Goertzel (*ben@goertzel.org*)

**Date:** Thu Nov 11 2004 - 08:32:47 MST

**Next message:**Christian Szegedy: "Re: Calculemus"**Previous message:**Keith Henson: "Re: META: Memes and War [was: Tomorrow is a new day]"**In reply to:**Christian Szegedy: "Re: Calculemus"**Next in thread:**Christian Szegedy: "Re: Calculemus"**Reply:**Christian Szegedy: "Re: Calculemus"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

Christian,

One key point is that, while embodiment and physical experience are

certainly not necessary guidance for theorem-provers *in general*, it

happens that our existent mathematics is HUMAN mathematics which is mostly

metaphorically grounded in human experience (spatial geometry, language,

etc.). Thus a system sharing some human commonsense intuitions will have an

advantage at dealing with human-created mathematics, although it wouldn't

necessary have an advantage in the greater space of all mathematical

theorems and proofs...

-- Ben

*> -----Original Message-----
*

*> From: owner-sl4@sl4.org [mailto:owner-sl4@sl4.org]On Behalf Of Christian
*

*> Szegedy
*

*> Sent: Thursday, November 11, 2004 6:59 AM
*

*> To: sl4@sl4.org
*

*> Subject: Re: Calculemus
*

*>
*

*>
*

*> Ben Goertzel wrote:
*

*>
*

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

*> >
*

*> I agree to some extent, but I am unsure whether mimicking human
*

*> thinking is
*

*> the best approach. Of course, as long as there is not anything better,
*

*> it is a good idea. The nature developed methods which can be
*

*> inferior under
*

*> slightly different cicrcumstances: if we build roads, cars are superior to
*

*> quadrupeds. Evolutionary methods are slow. Neural networks are inefficient
*

*> on current hardware. We can choose different, more efficient ways than
*

*> nature uses. The human thinking is the result of a long
*

*> cumbersome emergent
*

*> process. Some parts work efficiently, some are simply workarounds for
*

*> problems that could be eliminated by better overall design.
*

*>
*

*> I think that the correct approach is to cut the whole deducton
*

*> problem into
*

*> smaller subproblems, specify clear goals, meeasurable objective
*

*> functions for the parts and try to find mathematical optimization methods
*

*> to solve the subproblems efficiently. Whether these methods resemble
*

*> human thinking seems to be irrelevant.
*

*>
*

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

*> >
*

*> >
*

*> >
*

*> Experimental guiding is a natural and good idea, However, I am
*

*> not sure that
*

*> it is necessary to have "real-life" or simulated phyiscal experience
*

*> for pure
*

*> mathematical problem solving.
*

*>
*

*> My intuition is that an AI that could perform experiments on
*

*> mathematical objects
*

*> developed by itself, could perform very well. Of course, pure symbolic
*

*> reasoning like in todays theorem provers is not enough: a theorem prover
*

*> system
*

*> must be able to test the semantics of the mathematical statement by
*

*> performing
*

*> mathematical experiments, hence the necessity of the integration of
*

*> theorem-provers
*

*> and computer-algebra (and optimization) systems. I think that this type
*

*> of experience
*

*> (plus experience about the performance of internal algorithms) could be
*

*> enough
*

*> for a good AI.
*

*>
*

*> This is like a primal-dual optimization approach: the primal world is
*

*> the world of
*

*> formal statement, the dual is the semantics of those statements. When
*

*> looking for
*

*> a proof (a path in the primal world), you can eliminate false paths by
*

*> looking at
*

*> the dual function, just like in mathematical optimization.
*

*>
*

*> > So advanced theorem-proving will emerge from embodied,
*

*> experientially-savvey
*

*> > AGI.
*

*>
*

*> I think that a good AGI would emerge from a synthesis of different
*

*> concepts including formal deduction.
*

*>
*

*>
*

*>
*

**Next message:**Christian Szegedy: "Re: Calculemus"**Previous message:**Keith Henson: "Re: META: Memes and War [was: Tomorrow is a new day]"**In reply to:**Christian Szegedy: "Re: Calculemus"**Next in thread:**Christian Szegedy: "Re: Calculemus"**Reply:**Christian Szegedy: "Re: Calculemus"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

*
This archive was generated by hypermail 2.1.5
: Wed Jul 17 2013 - 04:00:50 MDT
*