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

**Date:** Sun Oct 23 2005 - 21:49:56 MDT

**Next message:**Olie Lamb: "Re: AI debate at San Jose State U."**Previous message:**Michael Vassar: "Re: AGI motivations"**Next in thread:**Herb Martin: "RE: Mizar conversion project..."**Reply:**Herb Martin: "RE: Mizar conversion project..."**Reply:**Herb Martin: "RE: Mizar conversion project..."**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

Hi all,

I'm writing this message just to see if there's anyone out there who's

interested in taking up a somewhat difficult but very important

math/software project, which would be very helpful for AGI in general (and

for my Novamente project, as it happens ;) ...

I am not alone in believing that mathematical theorem-proving is going to be

very important to AGI in the long run. If an AGI is going to learn to

modify its own codebase intelligently, it had better understand mathematics

pretty well.

But how will this hypothetical AGI learn to prove theorems?

Of course, it could learn from human teachers, just as we humans do.... I

suspect this kind of teaching WILL play a role.

But, it's not the only way... because AI programs will have the capability

to automatically ingest mathematical proofs in digital form....

And the good news is: there is a large corpus of mathematical proofs already

in mathematical form, check out

www.mizar.org

Beautiful idea, huh?

The problem is, their notation is complex, and their proof checker is

proprietary, even though their corpus of mathematical theorems is publicly

available.

What is needed is for someone to write some scripts that translate Mizar

definitions, theorems and proofs into some standard set-theoretic notation.

This will make the proofs much longer and less human-readable, but will

enable the loading of Mizar data into AI programs.

Although it hasn't been our focus, Novamente has already been used for some

simple set-theoretic theorem-proving. We could load Mizar into Novamente

right now and play with inductive learning of "how to prove theorems" based

on the Mizar corpus of thousands of proofs --- but we can't because

translating Mizar into some more tractable notation is a major though

straightforward task, and we don't have the resources to undertake it.

This would be a project of tremendous general value to the AI and

mathematics community, IMO.

It might be that this could be done by hacking the Mizar proof-checker

itself ---- if one could get access to the source-code of this, which would

require asking the owners realllly nicely, I suppose. Not having seen that

code I don't know if that would be the best approach or not.

Anyway, if anyone out there is interested in taking on this project please

let me know. It is obviously a bit of tedious work, but the end result

would be very very useful to a lot of people and would help science advance.

-- Ben

**Next message:**Olie Lamb: "Re: AI debate at San Jose State U."**Previous message:**Michael Vassar: "Re: AGI motivations"**Next in thread:**Herb Martin: "RE: Mizar conversion project..."**Reply:**Herb Martin: "RE: Mizar conversion project..."**Reply:**Herb Martin: "RE: Mizar conversion project..."**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

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