**From:** Marc Geddes (*marc_geddes@yahoo.co.nz*)

**Date:** Sun Apr 04 2004 - 23:44:10 MDT

**Next message:**Tyler Emerson: "Need remarkable sayings for new SIAI site buttons"**Previous message:**Thomas Buckner: "Re: On the subjective experience of consciousness"**In reply to:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Next in thread:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Reply:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Reply:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

--- Ben Goertzel <ben@goertzel.org> wrote: >

*> Hi Marc,
*

*>
*

*> I have some comments about AGI and mathematical
*

*> reasoning, and also
*

*> about fundraising strategy for your project.
*

*>
*

*> About AGI and mathematical reasoning...
*

*>
*

*> I have long been interested in using the Mizar
*

*> corpus (www.mizar.org) as
*

*> a resource for helping teach AGI's mathematics.
*

Fascinating, fascinating. I'll check it out.

*>
*

*> Mizar is a knowledge base that consists of a large
*

*> amount of
*

*> mathematical knowledge, encoded in a purely formal
*

*> language. (Comparing
*

*> Mizar articles with typical mathematics research
*

*> papers is very
*

*> instructive in terms of how *informal* typical
*

*> mathematical discourse
*

*> is.)
*

*>
*

*> However, the formal language of Mizar is large and
*

*> complicated; a first
*

*> step would be merely to translate Mizar into a
*

*> simpler formal language,
*

*> such as some kind of variant of predicate calculus.
*

*> (Note: My own AI
*

*> system, Novamente, does not use predicate calculus
*

*> or anything terribly
*

*> similar, but, predicate calculus is commonly
*

*> understood, and it's simple
*

*> enough that converting predicate calculus into
*

*> Novamente node-and-link
*

*> structures or pretty much anything else isn't a big
*

*> trick.)
*

*>
*

*> The purpose of translating Mizar into a simpler
*

*> formalism is that one
*

*> can then feed Mizar -- this vast corpus of
*

*> mathematical reasoning --
*

*> into one's AI system, and allow one's AI system to
*

*> learn how
*

*> mathematical reasoning has been done in many past
*

*> cases. The main
*

*> point isn't the *theorems* per se, it's the *proof
*

*> patterns*, both
*

*> low-level and abstract.
*

*> At any rate, this is my best bet regarding how to
*

*> get an AI system to do
*

*> mathematics really well.
*

Excellent ideas.

*>
*

*> The alternative to a Mizar-based approach, in my
*

*> opinion, is to begin
*

*> not with mathematics but with *natural language
*

*> processing*, so that the
*

*> AI system can be taught mathematics by humans.
*

*>
*

*> Without Mizar (or something similar) or NLP, you're
*

*> asking an AI system
*

*> to learn mathematics by all by itself, and that's
*

*> very very hard. By
*

*> "learn mathematics" here, I mean "learn the subtle
*

*> patterns of
*

*> demonstration and hypothesis that characterize
*

*> creative mathematical
*

*> thinking".
*

I'm thinking (or hoping) that it's a somewhat simpler

task than full-blown AGI. What I also like is that

mathematical problems are well-defined and results are

clear-cut.

*>
*

*> Now, about fundraising.
*

*>
*

*> My guess is that you'll have a better chance at
*

*> raising the funds you
*

*> want if you can first demonstrate some notable
*

*> success at a simpler
*

*> mathematical theorem-proving task. The Riemann
*

*> Hypothesis is a big
*

*> goal, obviously.
*

Well, needless to say, if I ever pull off a proof of

the Riemann Hypothesis all the funding problems would

be over for good. I'd be world famous - ;)

The reason I mentioned the Riemann Hypothesis is

precisely because of the huge interest it generates.

I'm thinking people would 'sit up and take notice' if

I'm actually shooting for some big goal of great

interest, but at the same thing something which is

more understandable and modest than AGI.

But in practise the solution is not the important

thing. It's the proccess of trying to get there that

I'm thinking would generate some results.

*>
*

*> The current state of mathematical theorem-provers is
*

*> not very
*

*> impressive, so if you have a genuinely innovative
*

*> and high-quality AGI
*

*> design with a theorem-proving orientation, it
*

*> shouldn't be sooooo hard
*

*> to beat the state of the art. Current
*

*> theorem-provers really only
*

*> perform adequately when given continual human
*

*> guidance regarding the
*

*> choice of which "proof path" to take.
*

Hmm.

*>
*

*> In the Mizar-based approach, mentioned above, it
*

*> would probably be
*

*> fairly simple to make unprecedented progress in
*

*> mathematical
*

*> theorem-proving just by loading Mizar into a
*

*> reasonably robust
*

*> AGI-oriented architecture and letting it lern some
*

*> proof-patterns, and
*

*> setting it loose to prove theorems in a relatively
*

*> compactly
*

*> formalizable domain like set theory or topology.
*

Good. The reason for the emphasis on mathematics is

that I want something with well defined results and

good prospects for business applications or results of

monetary value (for funding).

Certainly, theorem provers would have a good demand in

many different scientific appplications.

*>
*

*> Without demonstrable preliminary results, my guess
*

*> is that in order to
*

*> raise funding you'll need to get someone with some
*

*> record of success in
*

*> automated theorem-proving involved. Unfortunately,
*

*> everyone I know in
*

*> that community is rather conservative in orientation
*

*> and would be
*

*> unlikely to get involved in a project they viewed as
*

*> highly speculative.
*

*> But perhaps my constacts are not representative of
*

*> that community!
*

*>
*

*> Best of luck!
*

*> Ben Goertzel
*

*>
*

I must say, I like the way you've been 'playing it'

for your own projects. Far smarter than 'Sing Inst'

in my opinion. I think the business-oriented model is

the way to go. For any AGI Project to get on-going

funding, I think what is needed is an emphasis on a

series of more modest, shorter-term applications -

which have clearly defined results and some potential

monetary value. That's why I'm looking the 'theorem

prover' angle.

I'll see what I can do before the end of the year to

raise some interst in N.Z and Australia. At the very

least there will be a new Institute with a team of one

working away part-time ;)

Cheers

=====

"Live Free or Die, Death is not the Worst of Evils."

- Gen. John Stark

"The Universe...or nothing!"

-H.G.Wells

Please visit my web-site: http://www.prometheuscrack.com

Find local movie times and trailers on Yahoo! Movies.

http://au.movies.yahoo.com

**Next message:**Tyler Emerson: "Need remarkable sayings for new SIAI site buttons"**Previous message:**Thomas Buckner: "Re: On the subjective experience of consciousness"**In reply to:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Next in thread:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Reply:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Reply:**Ben Goertzel: "RE: I'm making my move! A new AGI Project is born"**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

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