Mizar Conversion Project
From AGIRI.org
The purpose of this post is to solicit volunteers for a somewhat difficult but very important math/software project, which I believe would be very helpful for AGI in general.
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 an 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:
"The Mizar project is a long-term effort aimed at developing software to support a working mathematician in preparing papers. A. Trybulec, the leader of the project, has designed a language for writing formal mathematics. The logical structure of the language is based on a natural deduction system developed by Jaskowski. The texts written in the language are called Mizar articles and are organized into a data base. The Tarski-Grothendieck set theory forms the basis of doing mathematics in Mizar. The implemented processor of the language checks the articles for logical consistency and correctness of references to other articles."
The problem is, the Mizar 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.
Pretty much any simple, standard notation similar to predicate logic would do, but as a concrete suggestion I'd advocate KIF (Knowledge Interchange Format), see:
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.
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 AI advance.
To contribute to this project, contact Ben Goertzel ben -at- goertzel.org
