From: Ben Goertzel (ben@goertzel.org)
Date: Sun Oct 23 2005 - 21:49:56 MDT
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
This archive was generated by hypermail 2.1.5 : Wed Jul 17 2013 - 04:00:52 MDT