RE: Mizar conversion project...

From: Herb Martin (HerbM@LearnQuick.Com)
Date: Sun Oct 23 2005 - 23:05:05 MDT

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

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

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

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

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

Maybe I missed some serious problem in my rapid

Herb Martin

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