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 ------- To unsubscribe, change your address, or temporarily deactivate your subscription, please go to http://v2.listbox.com/member/[EMAIL PROTECTED]
