> I wasn't thinking of any truly exotic. Look up > "effectively generated theory" - that covers most > garden variety mathematical theories. I'll guess your > proof checker doesn't handle anything that's not. >
Do your "garden variety mathematical theories" include things like number theory, abstract algebra and geometry? While designed as primarily a learning aid, I see no reason that DC Proof could not be used to generate most if not all of current mathematical theory -- that is, theories based on some underlying set, e.g. the set of natural numbers in number theory, or the set of points in a plane for geometry.