Recently I had a question assigned to me in “The Theory of Sets” class I am taking. I responded to this task by generating a computer-verified formal proof. Though I got full marks for the informal proof section, other exercises that consisted of only formal proof were given a 0 by this TA.
This event raises some interesting questions. What is the purpose of assigning proofs as exercises in math courses? Does submitting a computer-verified formal proof satisfy these purposes? The TA in this case gave many comments on the subject, which I will address here. In this document I take formal proof to mean a computer-verified formal proof of some kind.
In this document I am not arguing that students should be required to submit formal proofs. It seems clear that proof editing environments are not yet well enough developed to make such a requirement reasonable. I do argue that, in general, submitting a formal proof for an assigned question should be acceptable.
One common complain about computer-verified proofs is that the system is would contain bugs, so the results are not trustworthy. The TA wrote the following.
You mean we should convert the clear statements [...] into an enormous jumble of nonsense and plug that into a device of gargantuan complexity that we have no hope of ever understanding in complete detail?
The first thing I note is that to the rest of the world what mathematicians do all day is work with an enormous jumble of nonsense. The TA of all people should appreciate the meaning that such a jumble can contain.
The point about the device of gargantuan complexity is just plain false. Though an entire proof system might of gargantuan complexity, the output is simple. The proof object (usually some form of lambda expression) is type checked. There are three components being relied on.
This is what most people think needs to be trusted. It is a fairly simple program. The algorithm is simple enough that asking for an implementation would be a reasonable assignment in an undergraduate computer science course. Smart people write and inspect popular implementations and test them throughly. I think the scrutiny given to the code is at least as much as to any given informal English proof, and certainly more than a single TA gives to a given assignment.
The complier turns the type-checker into machine code. Every day thousands of people trust their compiler. If one is paranoid, one can turn off all optimizations. Even in this sorry state, the type-checker can run quickly (because it is such a simple algorithm). Different compilers can be used and different programs run for added security.
Big companies put in lots of effort to ensure the hardware runs correctly. Far more than is put into hand checking informal English proofs. Millions of people use the same hardware all the time without problems.
So in reality verification of formal proofs is a simple process. Although lots of structure is in place to make generating proofs easier, none of this extra structure is relevant to believing a computer when it verifies a proof. The gargantuan complexity of a proof editing environment may be buggy. It is possible that the environment will produce erroneous proofs; however, these erroneous proofs will be caught by the proof-verification process, and the bug in the program revealed. It is impossible to have a computer claim that a unprovable theorem is provable given a correct implementation of the type-checking algorithm.
The above aside, the main concern is that I did not fulfill the purpose of the assignment. Upon reflection it is unclear to me what the purpose of assignments are. I am sure this can be hotly debated. The TA expressed four purposes that should be met. I address these now.
To develop your intuition regarding the universe of sets
I feel that this is the most important reason for doing assignments. Writing a formal proof definitely fulfills this purpose.
Even when a student understands a subject, writing a formal proof is a difficult process. If the student does not understand a subject, writing a formal proof would be all but impossible. One cannot try to bullshit one’s way through the formal verification.
In my case, one might object if I were using a library of proofs in set theory. In this case I am not. I did employ the Tauto tactic which infers propositional tautologies. Since this is a course on set theory not propositional logic, I feel using such automation is reasonable.
Also I did not automatically search to find a proof. Such a procedure is extremely intractable (undecidable), and in general any assignment calling for a proof that could be found this way would be an insult to the student.
To convince the relevant people that you are working on this class and studying etc…
The TA concedes that writing a formal proof fulfills this purpose as he states it. Whether a student submitting a formal proof convinces the relevant people that the student understand the subject requires some commentary.
One thing that formal proofs are bad at is explaining the subject. However presumably the professor and TA already know the subject. The goal of the assignment is to determine if the student knows the subject. Submitting a formal proof that a student writes theirself provides evidence to the university that the student understands the subject. If the student did not understand the material, then they could not have made such a submission without cheating.
Detecting cheating with formal proofs is about as hard as detecting cheating with programming assignments in computer science. Since submitting programs is acceptable in computer science courses, fears of cheating should not make submitting formal proofs in mathematics unacceptable.
To give you practice in ‘formal’ proofs in set theory
I am not sure what the TA meant by ‘formal’ proofs. I would guess a ‘formal’ proof is a proof written is sufficient detail to enable a peer mathematician to construct a fully detailed formal proof if wanted. Clearly given an actual formal proof satisfies this. The hypothetical peer mathematician need not do any work.
To develop the skills in you to enable you to read research-level papers and to do independent research on you own, proving novel theorems, etc.
I do not see how assignments requiring proofs helps a student read research-level papers and to do independent research on their own. Reading research papers can help the student understand the material better, enabling them to write formal proofs, but this is not guaranteed to happen by such an assignment.
The ability to prove novel theorems comes from gaining an understanding of the subject. As I have remarked already, understanding of the subject is required to create formal proofs, so the ability to write formal proofs will help a student prove novel theorems.
I am certain that creating formal proofs will someday be common place in the world of the working mathematician, and we will realise far more is gained than lost by such a practice.