On Thu, Oct 16, 2008 at 10:32 PM, Dr. Matthias Heger <[EMAIL PROTECTED]> wrote: > In theorem proving computers are weak too compared to performance of good > mathematicians.
I think Ben asserted this as well (maybe during an OpenCog tutorial?). Is this proven? My intuition is that a computer could easily beat a mathematician on randomly generated problems from theorem space, but could not generate mathematically interesting theorems the way a mathematician could. In other words, I would expect the hard AGI problem to be "figure out what other mathematicians will be excited about", not "prove theorems". So, I don't see how one would proceed in making math-based AGI... it seems like an effective natural language interface would be needed after all, to allow the AGI to read mathematical papers, and to write its own. Otherwise, it would just be creating theorems of interest to itself, and it would be impossible to judge these as "interesting" or "uninteresting" in an objective way. --Abram ------------------------------------------- agi Archives: https://www.listbox.com/member/archive/303/=now RSS Feed: https://www.listbox.com/member/archive/rss/303/ Modify Your Subscription: https://www.listbox.com/member/?member_id=8660244&id_secret=117534816-b15a34 Powered by Listbox: http://www.listbox.com
