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 ;-)
Best regards, Lukasz Stafiniak ----- 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
