Like I was saying, the tautologists have carved out a niche (as usual). Just don't confuse this claim with TV show renderings of computers and/or their controllers somehow proving all of the math you learned in high school, using some genetic algorithm. So far, proving theorems in most domains is strictly non-computable in the operational sense of computers so far not managing to hit the targets in questions. Kinda like Star Wars (SDI).
On Fri, Dec 23, 2011 at 10:08 AM, Joe Niederberger <email@example.com> wrote: >>Do your "garden variety mathematical theories" include >things like number theory, abstract algebra and geometry? > > I was being a bit tongue in cheek. To NOT be in the class of "effectively generated theory" the formal theory in question must have axioms that comprise a non-recursively enumerable set. Truly exotic, as I said. Actually, I'm not really aware of any theories of algebra or geometry that are not "effectively generated" (i.e., garden variety).