Introduction to Proofs

The syllabus can be found here.

REFERENCES

The main text with be Clive Newstead's An Infinite Descent into Pure Mathematics, version 0.4, which is available for free in a variety of formats (PDF, tablet, smartphone).

An optional supplemental reference is How To Prove It: A Structured Approach by Daniel J Velleman.

You might also enjoy How to write proofs: a quick guide by Eugenia Cheng.

PROBLEM SETS

Problem sets will be posted on the Blackboard site and are due before class on Wednesdays. An extra optional problem set, related to the computer proof assistant unit, appears below.

• Optional Problem Set 8; Coq version

Here are some resources, originally developed by tslil clingman:

• JsCoq, an online theorem prover
• lecture notes
• source code

• Script 1
• Script 2
• Script 3
• Script 4
• Script 5
• Script 6
• Script 7

Here are some questions for discussion (feel free to add others):

• What is a proof? (see On proof and progress in mathematics, Mathematicians know how to admit they're wrong, What is a proof?)
• If an expert mathematician writes up an argument that few others understand, does this constitute a proof? Did Mochizuki resolve the ABC conjecture? (see The ABC conjecture has not been proved, The ABC conjecture has still not been proved, A crisis of identification)
• If mathematicians reduce a problem to 730 cases and a computer verifies the claimed result in each case, does this constitute a proof? Did Appel and Haken prove the four-color theorem and did Ferguson and Hales prove the Kepler conjecture? (see The colorful life of the four-color theorem, Proof confirmed of 400-year-old fruit-stacking problem)
• Does an argument constitute a proof if it hasn’t been formally verified? (see The Origins and Motivations of Univalent Foundations)

If you have any questions about the course, please get in touch. My contact info can be found on my personal website.