From: Ben Goertzel (email@example.com)
Date: Sun Apr 04 2004 - 09:11:49 MDT
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.
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
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.
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
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
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.
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.
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!
> -----Original Message-----
> From: firstname.lastname@example.org [mailto:email@example.com] On Behalf
> Of Marc Geddes
> Sent: Sunday, April 04, 2004 4:15 AM
> To: firstname.lastname@example.org
> Subject: I'm making my move! A new AGI Project is born
> I'm posting a brief outline: this is a sketch of what
> I'm thinking of putting on the web-site when I get one
> up. Hopefully I can get this thing off the ground.
> I'm the new player on the block in the race for AGI
> and I'm making a big power play! ;) Watch the sl4
> list for further news. Meantime comments or private
> e-mails are welcome.
> The Riemann Artificial Intelligence Institute
> Mission Statement:
> The Riemann Artificial Intelligence Institute aims to
> research artificial general intelligence, with an
> emphasis on developing software capable of reasoning
> about mathematics. The long-term goal is to create
> true artificial general intelligence in a computer
> True AGI would be AI with a general capacity for
> learning exceeding that of a human. Smarter than
> human intelligence could help solve problems and make
> breakthroughs which would enormously improve the quality of
> life for humanity. Such a thing is regarded as possible by
> experts because our best current scientific theories indicate
> that it is a sensible proposition.
> The shorter-term goals are to develop software which
> can assist in solving problems in mathematics of
> significance and propriety value. The purpose of the
> shorter-term goals is to try to ensure results of definite
> value to society and to secure sufficient on-going interest
> and funding to achieve the long term goal. Since mathematics
> is the language of science, there is also the possibility
> that software capable of reasoning about mathematics will be
> useful for artificial general intelligence research.
> The specific mathematical problem initially selected
> to be attempted was 'The Riemann Hypothesis' (Named
> after the great German mathematician Berhard Riemann).
> Not only is this the most famous unsolved problem in
> mathematics, a cash prize of $US 1 million is currently being
> offered by the Clay Mathematics Institute for its solution.
> A solution to the Riemann Hypothesis could solve the deepest
> mystery of pure mathematics - the secret to the distribution
> of prime numbers - and provide insights of great value to the
> mathematics community. It would also generate enormous
> interest and result in immediate financial reward to assist
> with further research. The reason for thinking that success
> is a fair possibility is that some experts feel that
> knowledge has progressed to the point where a solution may
> not be far off, and the computer-assisted approach is one
> which has been neglected.
> Plan and estimates:
> Staff and budget:
> The Institute aims for 5 full-time paid team members,
> each of which would have a salary of $US 20 000 per
> year (Total annual cost of team salary: $US 100 000).
> This is obviously fairly low pay, but it's
> sufficient. One of the team members would double as
> the director. There could also be any number of
> additional part-time team members, but these would
> have to be volunteers.
> The Institute aims for a budget of an additional $US
> 100 000 annually, in order to rent living space and
> buy equipment.
> Total annual budget: $US 200 000
> This is probably the minimum budget required for a
> full-time AGI project capable of getting anywhere.
> Time frames:
> The shorter-term goals of creating software capable of
> deep mathematical reasoning would be expected to begin
> yielding results within 2 years. A solution to the
> specific 'hard problem' selected (the Riemann
> hypothesis) could be to hand within 2-5 years.
> Initial software design related to the problem could
> take around a year of full-time research by the team,
> and another 1-4 years of coding and refinements. Note
> that on a budget of $US 200 00 per year, 5 years work
> to solve the Riemann hypothesis would cost $US 1
> million, which would be fully reimbursed upon payment
> of the prize offered by the Clay Mathematics Institute
> for the solution.
> The longer term goal of true general artificial
> intelligence in a computer system could take anywhere
> from 2-50 years of full-time work. There are too many
> unknowns to be able to estimate a more precise time
> frame with any confidence. All one can really say is
> that AGI will probably be achieved some time within
> the next 50 years. A 'consensus' guesstimate by
> experts is for AGI circa 2030. The task is thus
> likely monumental, speculative and truly long-term.
> More modest (slight irony!) goals such as software
> capable of assisting in finding solutions to hard
> mathematical problems such as the Riemann Hypothesis
> are needed for a realistic chance of shorter term
> usefulness. The Institute will have achieved
> something if it can contribute but a little towards
> the grand goal of AGI.
> Institute Background
> The Institute was born on 4th April, 2004. Its
> founder was Marc Geddes, Free-Lance Writer,
> Transhumanist and paid member of the WTA (World
> Transhumanist Organization) since 2002. Transhumanism
> is a rationalistic philosophy of the world advocating
> the responsible use of science, technology and
> critical thinking to improve the human condition.
> Institute Status as of: 4th April, 2004
> News of the Institute's founding was posted to the Sl4
> (Shock Level 4) Mailing List. A dedicated web-site
> has not yet been created on the World-Wide-Web. One
> is being planned.
> The Institute has no legal status.
> The only person working for the Institute is Marc
> Geddes. He has begun research pertinent to Artificial
> General Intelligence, Pure Mathematics, and the
> Riemann Hypothesis. This work is currently only
> part-time and unpaid.
> The Institute currently has no funding or physical
> location. Businessmen and philanthropists in New
> Zealand and Australia are being approached. A
> physical location in Australia is preferred.
> Other AGI Projects
> Although 'Artificial intelligence' is a field which
> now attracts large interest and a great deal of
> funding around the world, circa 2004 there are few
> projects which have the aim of achieving true
> artificial general intelligence in a computer system.
> True AGI would be AI with a general capacity for
> learning comparable to humans or better. There are 3
> main dedicated players (the names of the founders are
> in brackets):
> Singularity Institute (Eliezer Yudkowsky)
> Artificial General Intelligence Institute (Ben
> Adaptive AI Inc. (Peter Voss)
> The Riemann A.I Institute strongly supports the work
> of the three named organizations. A wealth of
> information about the long-term promises and perils of
> AGI is available on the Singularity Institute web-site
> and it is recommended that those interested in AGI
> read the materials available there. Where possible,
> the Riemann A.I Institute is prepared to donate funds
> and other support to these projects.
> "Live Free or Die, Death is not the Worst of Evils."
> - Gen. John Stark
> "The Universe...or nothing!"
> Please visit my web-site: http://www.prometheuscrack.com
> Find local movie times and trailers on Yahoo! Movies.
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:46 MDT