- The entire work of the understanding must be begun afresh and the mind, from the start, not left to take its own course but guided step by step and the business done as if by machinery.

I examine and explain some of my beliefs about formal logic systems. First here is how and some of what I learned about them. I highly recommend this book which is largely about why and how others care.

In summary however, I have become convinced that:

- Formal systems commonly in use today in the math community are faithful enough to my own modes of reasoning that I believe what they formally prove.
- Proofs in such systems are suitable for being checked by fast simple programs.
- Some of the proofs are so long that I may overlook errors and fool myself. The computer can verify that such a proof indeed follows the rules and I have learned that computers find things like errors in programs and proofs far better than I.
- Formal proof systems in the computer science community may ultimately be simple but little work has been done to make them appear simple. I looked in vain for the semantics of the formal system used by Mizar. Maybe this is good.

I suspect that I do not need a system that has a name for the set of integers, but perhaps I am wrong here.

I think that any proof that I need to verify is a sequence of fairly short propositions, but perhaps a very long sequence.

Of course I agree with the widely quoted caveat that the problem with formal proofs is understanding what you have proven.