Assignments
December 4
Read:
- Ken Manders, "The Euclidean diagram," pdf
- Jeremy Avigad, Edward Dean, and John Mumma, "A formal system for Euclid's Elements," pdf.
- Jeremy Avigad, review of Marcus Giaquinto, Visual Thinking in Mathematics: An Epistemological Study, pdf.
November 20
There is no reading assignment for this week; I will give a presentation of modularity in mathematics.
November 13
Read:
- Michael Detlefsen, "Duality, epistemic efficiency and consistency," pdf
- Andrew Arana, "On the depth of Szemeredi's theorem," pdf.
November 6
We will start with the Hamami paper from last week. After that, we will look at specific proof languages used by interactive theorem provers. You can read about any that interest you (see the bibliography page), but I will focus on these:
- Freek Wiedijk, "The mathematical vernacular," pdf.
- Georges Gonthier, Assia Mahboubi, and Enrico Tassi, "A Small Scale Reflection Extension for the Coq System," pdf.
- Tobias Nipkow, Programming and Proving in Isabelle/HOL, pdf.
- Jeremy Avigad, Leonardo de Moura, and Soonho Kong, Theorem Proving in Lean, pdf.
October 30
Note that the seminar will not meet on Friday, October 23.
For October 30, read the following:
- Kenneth Manders, "Expressive means and mathematical understanding," pdf
- Yacin Hamami, "Mathematical rigor, proof gap, and the validity of mathematical inference," pdf
- Mahi Hardalupas, "When is a proof not a proof?: A computer-aided evaluation of the mathematical notion of proof," pdf
October 16
- Read Avigad and Morris on Dirichlet's theorem: either pdf, which focuses more on the philosophical issues, or doi, arXiv, which focuses more on the mathematics and history
- On deck: Hamami, Hardalupas, and Manders
October 9
- This week, we'll continue to discuss Simon, then move on to Parnas and SICP.
October 2
- Read Simon, "The architecture of complexity," pdf.
- Read Parnas, "On the Criteria to Be Used in Decomposing systems into Modules," pdf.
- Skim over the chapters of Abelson, Sussman, and Sussman, Structure and Interpretation of Computer Programs, pdf. Read especially the introductions to chapters 2, 3, and 4, and section 3.5.5.
September 25
- This week, we will continue to work through the Kaplan paper, and then move on to the paper by Ward and Birner. We will also look at some sample mathematical texts to see if we can discern any interesting phenomena. Please send me examples we can look at together.
September 18
- Read Kaplan, "The meaning of ouch and oops," either the manuscript, pdf, or the transcript of the talk, pdf.
- Read Ward and Birner, "Discourse effects of word order variation," pdf.
- Look through your favorite mathematical text (or any mathematical text) for interesting examples of not-strictly-inferential content, and interesting choices of word order. Bring some examples to the next meeting.
September 11
- Read Avigad, "Mathematical method and proof," pdf.
- To get a sense of interactive theorem proving, try any of these:
- Avigad and Harrison, "Formally verified mathematics," pdf.
- Gonthier et al., "A Machine-checked proof of the odd order theorem," pdf.
- Hales et al., "A formal proof of the Kepler Conjecture," pdf.
Alternatively, read any of the surveys and papers on interactive theorem proving on the bibliography.
September 4
- Take a look at Avigad, "Mathematics and language," pdf, and the associated talk, pdf.
- Let me know if you would like to be on the seminar e-mail list.