"Your intuition is dead wrong based on the last decades of work in automated theorem proving!!"
Ben, Thanks... though I do find that rather strange... can you cite any particular references? The reason I find it surprising, is that it suggests the existence of actual shortcuts, rather than only heuristics that work in the domains we're interested in but which become useless on random problems. If these shortcuts exist, I wonder, could they be enumerated by some brute-force method? --Abram On Thu, Oct 16, 2008 at 11:26 PM, Ben Goertzel <[EMAIL PROTECTED]> wrote: > > > On Thu, Oct 16, 2008 at 11:21 PM, Abram Demski <[EMAIL PROTECTED]> > wrote: >> >> 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". > > Your intuition is dead wrong based on the last decades of work in automated > theorem proving!! > > Combinatorial explosion is the problem. The lack of effective inference > control, as we discussed in last night's OpenCog chat/tutorial session. > > All the most interesting achievements of automated theorem proving have been > **semi-automated**, with humans helping the AI to prune the > backward-chaining inference tree at the difficult places. > >> >> 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. > > The way to proceed would be to feed the AGI on proofs from Mizar.org ... > > But, this is certainly very hard if the AGI doesn't have any way to accept > tutoring > > Still, I imagine that via a combination of Lojban and Mizar, one could teach > an AGI theorem-proving, without needing to mess with the horrible syntax or > excessive semantic ambiguity of natural languages... > > -- Ben > > ________________________________ > agi | Archives | Modify Your Subscription ------------------------------------------- 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
