Home

Here are notes and ideas for further chapters.

• We should have a Calculation chapter, which explains tactics like linear_combination, polyrith, positivity, gcongr. We can draw on Heather's lecture notes and here Algebraic computations in Lean.

• We need a chapter on discrete mathematics, explaining how to use finite sets and cardinality calculations, etc. See Kyle's lecture at MSRI. Jeremy also has notes, lectures, and exercises from his ITP class.

• We should have a chapter on Galois theory and polynomials. See Thomas Browning's lectures at MSRI.

• We should have a chapter on linear algebra.

• We should have a chapter on category theory.

• We should discuss Aesop somewhere.