**Meeting 12: December 6**

Euclidean diagrammatic reasoning, following the slides here.

**Meeting 11: November 20**

Modularity

- mathematics from a design standpoint
- modularity in complex systems
- modularity in computer science
- modularity in mathematics
- case studies

**Meeting 10: November 13**

Arana, "On the depth of Szemeredi's theorem"

- overview of Szemeredi's theorem
- views of depth: genetic, evidentialist, consequentialist, "cosmological"

Detlefsen, "Duality, epistemic efficiency, and consistency"

- examples: projective geometry, Boolean algebras, category theory
- different senses of dualization
- the epistemic calculus
- self-dual vs. non-self-dual axiomatizations

**Meeting 9: November 6**

Hamami, "Mathematical rigor, proof gap, and the validity of mathematical inference"

- the notion of a gapping
- Prawitz' account of grounds and operations
- Kitcher on a "mathematical practice"
- Intra vs. inter-practice gaps

Interactive theorem prover languages

- components of a proof language
- Wiedijk, "the mathematical vernacular"
- SSReflect

**Meeting 8: October 30**

Manders, "Expressive means and mathematical understanding"

- conceptual recasting
- merelification
- linguistic restriction, modes
- Euclidean devices to "suppress and retain responsiveness"
- Descartes

Hardalupas, "When is a proof not a proof?"

- traditional proofs vs. computer proofs, accounting for the differences
- why do mathematicians prove theorems?
- proof as narrative
- historical narrative vs. literary narrative

**Meeting 7: October 16**

**Meeting 6: October 9**

Simon, "Architecture of Complexity"

- recap from last week
- near decomposibility
- descriptions of complex systems, understandability
- state descriptions vs. process descriptions
- conclusions

Parnas, "On the criterion..."

- two modularizations
- differences
- conclusions

*Structure and Interpretation of Computer Programs*

- building abstractions with procedures (primitive combinations, means of combination, means of abstraction)
- local names
- higher-order procedures
- building abstractions with data
- abstraction barriers, multiple representations (type tags), generic operations, coercions
- modularity, objects, and state
- state vs. streams

**Meeting 5: October 2**

Birner and Ward

- open propositions
- preposing, inversion, gapping, etc.
- the methodology of linguistics

Mathematical texts

- excerpt from Hatcher,
*Algebraic Topology* - excerpt from Hardy and Wright,
*Introduction to the Theory of Numbers*

Modularity

- designed systems vs. natural systems
- hierarchy vs. modularity
- benefits

Simon, "Architecture of Complexity"

- Hora and Tempus
- examples

**Meeting 4: September 25**

Kaplan on "ouch" and "oops"

- recap of last week
- "ouch" vs. "oops," subjective vs. objective expressives
- "and" and "but," distinctions between descriptive content, expressive content, and pragmatics
- translation, and the distinction between linguistic conventions and social conventions
- conclusions

Birner and Ward

- information structure
- preposing, left-dislocation, postposing, and right-dislocation

**Meeting 3: September 18**

Interactive theorem proving

- formal sytems: expressive strength rather than logical strength
- varieties of proof languages
- proof languages and programming languages

Moving beyond the "standard" model of proof

- coarser steps, real-world justifications
- active language: apply, calculate, construct, ...
- non-inferential content: examples and special cases, motivation, key ideas
- subtleties of communication: word order, linguistic variation

Kaplan on "ouch" and "oops"

- the formalist tradition vs. meaning as use
- partial reconciliations: Grice (conventional meaning vs. pragmatics), Searle (logic of speech acts)
- semantic information (descriptive vs. expressive content)
- logical validity and entailment in this more general context

**Meeting 2: September 11**

Mathematical method and proof

- traditional views of mathematical knowledge
- more robust views: theorems, definitions, proofs, questions, concepts, methods, heuristics, ...
- products of sums of squares: evaluating proofs
- conclusions

Interactive theorem proving, following this survey: pdf.

**Meeting 1: September 4**

Course mechanics

Ideas, motivation, and background stories

- Formalizing the PNT; the structure of mathematical knowledge, and normative assessments in mathematcs
- The history of Dirichlet's theorem, modularity, and refactoring
- The design of an interactive theorem prover, and artificial languages

Goals / questions

- Consider informal mathematics as a
*designed language*. What are the design constraints? What are the mechanisms by which it attains its goals? - Consider formal proof languages. Can we develop a good design theory? Can we use insights from the design of programming languages? Can we use semantic approaches?
- What does this have to tell us about mathematical knowledge, ontology, and the history of mathematics?