**From:** Herb Martin (*HerbM@LearnQuick.Com*)

**Date:** Sun Oct 23 2005 - 23:05:05 MDT

**Next message:**Herb Martin: "RE: Mizar conversion project..."**Previous message:**Olie Lamb: "Re: AI debate at San Jose State U."**In reply to:**Ben Goertzel: "Mizar conversion project..."**Next in thread:**Herb Martin: "RE: Mizar conversion project..."**Messages sorted by:**[ date ] [ thread ] [ subject ] [ author ] [ attachment ]

Ben Goertzel

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

<snip about proofs important -- yes they are>

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

Yes.

*> The problem is, their notation is complex, and their proof
*

*> checker is proprietary, even though their corpus of
*

*> mathematical theorems is publicly available.
*

It's didn't seem complicated at first glance since

it was declared to be formally rigorous.

What complications did I overlook? (I only took a

quick glance and downloaded the system out of curiousity,

which includes the same subject, and also intereste in

Novamente.

It appears to be well-defined in Backus-Naur form.

*> What is needed is for someone to write some scripts that
*

*> translate Mizar definitions, theorems and proofs into some
*

*> standard set-theoretic notation.
*

I am entering an intensive phase of work at least until

after Thanksgiving (into Dec probably) so may not have

much time for even considering the task, but it does look

interesting.

*> This will make the proofs much longer and less
*

*> human-readable, but will enable the loading of Mizar data
*

*> into AI programs.
*

Not necessarily -- depends on the format/syntax you

wish to use.

What is the native language of Novamente? What mathamatical

notations will/does Novamente use?

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

According to one source it contains:

"As of 2005, it contained about 8000 definitions and

40,000 theorems..."

< http://www.absoluteastronomy.com/encyclopedia/m/mi/mizar_system.htm >

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

"Straightforward" should remove the "major" from this.

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

*> and mathematics community, IMO.
*

That alone would interest me in looking into it,

when time permits.

What sort of real use would you get from this in

the near term?

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

Supposedly it is written in Pascal.

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

Although I am interested you might do better/faster to ask

of one of the Mizar groups/sites. The links on the page

I referenced above, include:

Main Mizar site, contains links to the MML, to

the Journal of Formalized Mathematics, and a

bibliography section linking to several

introductions to the system

MML Query, is a search engine for MML.

Freek Wiedijk's Mizar site, contains slides of a

conference talk about the system, as well as a

40 page introductory article

Association of Mizar Users

A paper about Mizar history

There are people much more skilled that I in parser

writing but it doesn't look THAT hard as such things

go.

Maybe I missed some serious problem in my rapid

survey....

-- Herb Martin

**Next message:**Herb Martin: "RE: Mizar conversion project..."**Previous message:**Olie Lamb: "Re: AI debate at San Jose State U."**In reply to:**Ben Goertzel: "Mizar conversion project..."**Next in thread:**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
*