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
>
> 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
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:52 MDT