[AmishDude]

Trying to put this in terms of formal math: proofs really only demonstrate that mathematical systems are self-consistent, and the derived theorems agree with the axioms, and each other.

Oh, I don't think so, but your area might be in that of algebra/logic. I focus on combinatorics/number theory. Computers are used to find certain structures and whether they exist but they can't be used in any way when there are an infinite number of postulates (Fermat's last, for example).

[grey_whiskers]

Computers are used to find certain structures and whether they exist but they can't be used in any way when there are an infinite number of postulates (Fermat's last, for example).

Oh, come OFF it already.

People write infinite loops all the time. (Some Cray supercomputers were able to complete an infinite loop in Fortran in under 2 seconds :-P )

Cheers!