Gradually the patterns of proofs began to come to your attention. Perhaps a high school geometry course explicitly discussed the form of proofs that Euclid closely followed. College logic courses first used precise definitions of logical propositions and also what it takes to be a proof. They may also provide metatheorems about proofs. A common pattern is proofs that proofs for certain propositions exist when those latter proofs are too big to write down. Another pattern is a proof that every proposition of some particular form has a proof.

I saw the study of this subject matter as a way to improve mathematics by making it more reliable. I was thus disoriented when I sat in on some graduate logic courses where the thrust was to use informal mathematical methods to discover what sorts of things a given formal system could prove, rather than exploitation of metatheory to become more certain of conventional mathematics.

The contrast was between:

- Applying logic to math—(Applying formal logic to do better mathematics);
- Applying math to logic—(Using conventional mathematical reasoning to elucidate various axiomatizations of mathematics).