**From:** Christian Szegedy (*szegedy@or.uni-bonn.de*)

**Date:** Thu Nov 11 2004 - 04:59:29 MST

**Next message:**Keith Henson: "Re: META: Memes and War [was: Tomorrow is a new day]"**Previous message:**Mikko Särelä: "Re: META: Memes and War [was: Tomorrow is a new day]"**In reply to:**Ben Goertzel: "RE: Calculemus"**Next in thread:**Ben Goertzel: "RE: Calculemus"**Reply:**Ben Goertzel: "RE: Calculemus"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

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:**Keith Henson: "Re: META: Memes and War [was: Tomorrow is a new day]"**Previous message:**Mikko Särelä: "Re: META: Memes and War [was: Tomorrow is a new day]"**In reply to:**Ben Goertzel: "RE: Calculemus"**Next in thread:**Ben Goertzel: "RE: Calculemus"**Reply:**Ben Goertzel: "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
*