Hi, Adding some thoughts on AGI math - If the AGI or a sub processor of the AGI is allotted time to "sleep" or idle process it could lazily postulate and construct theorems with spare CPU cycles (cores are cheap nowadays), put things together and use those theorems to further test the processing of data structures and representations in new ways. When the AGI is first started it could have the proof engine Mizar or Coq built in with a base set of proofs. It could use existing theorems to operate over its data and it can monitor the success and efficiency of the algorithms that it is using but implicitly understand that more efficient methods are possible. The close mapping of mathematical structures and language to its existing operational framework begets efficiency - if the internal language is closely related to a mathematical language it is better IMHO. This is probably not the case of existing AGI's perhaps there is a close mapping to NL for NLP sake and for efficiency in "rolling it out" existing AGI's are probably more hardcoded /hardwired. Reading about Coq and CIC the concept of the "Curry - Howard isomorphism" of typed lambda calculi is interesting. I have never heard of CIC. Mizar is a different approach to proofing? Mizar source code seems to be less available that Coq...
John -----Original Message----- From: Lukasz Stafiniak [mailto:[EMAIL PROTECTED] > Hi, > How should an AGI think about formal mathematical ideas? What > formalization of a logical argument would be the most digestible? Many > mathematicians don't like formalized approaches, because they think on > the level of patterns (which correspond to understanding the reality), > not on the "assembly" level of formalizations. But AGI could take > advantage of perceiving and manipulating the formalization itself. > Although I live not far from Bialystok, I don't think Mizar is the > right formalization to use. Mizar is a sophisticated artificial > language. What I would like to see used is a powerful, intelligible > system with frugal formulation, a logic whose assertions combine > theorems and proofs, and whose proofs are algorithms: the Calculus of > Inductive Constructions (CIC). The system that implements CIC is Coq > (http://coq.inria.fr/). The AGI would still need to think on the > patterns level (sometimes called heuristics), and it would still be > very useful to translate Mizar to CIC (perhaps the AGI could do the > translation...) but to have a being embodied at once in the physical > world and in the CIC world, wow! That would certainly prove something > ;-) ----- This list is sponsored by AGIRI: http://www.agiri.org/email To unsubscribe or change your options, please go to: http://v2.listbox.com/member/?member_id=231415&user_secret=fabd7936
