**December 4**

- 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**

**November 13**

- Michael Detlefsen, "Duality, epistemic efficiency and consistency," pdf
- Andrew Arana, "On the depth of Szemeredi's theorem," pdf.

**November 6**

- 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**

- 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: Alternatively, read any of the surveys and papers on interactive theorem proving on the bibliography.

**September 4**