Skip to content

Home

Jump to bottom
Jeremy Avigad edited this page May 2, 2020 · 14 revisions

Notes

  • We need to come up with a start on a table of contents. It can change, but this will let us get started with the writing.

  • We agree: lots of exercises.

  • We need Gabriel and Bryan to provide this functionality in VS Code:

    • try it! button: creates a folder in a hierarchy with a snippet, or open if it is already there
    • show more! button: opens a read-only file We need to come up with a general mechanism to specify where the files go.

  • The emphasis should be on mathematics rather than logic; we teach students the logic only insofar as they need to do mathematics. But is still not clear to Jeremy whether it is bad to have some general schematic identities, or to say words like "conjunction" and "quantifier". Patrick thinks we can use those words. In French math teaching we say quantifier everywhere, but don't have a word for conjunction. Here I don't see how to avoid needing words. Simply writing and and or doesn't blend with surrounding text, as illustrated by this sentence. And these words are not difficult to understand, the barrier is the lambda-calculus jargon.

  • Some sections should focus on basic skills: equational reasoning, proof by induction, etc. Others should be substantial mathematical examples, showing students how to use basic concepts in mathematics and how to write serious proofs.

  • The current site is here.

  • Patrick's tutorial is here.

  • Kevin's Lagrange gist is here, Jeremy's follow up is here.

  • Kevin's propositional exercises are here

  • There are also exercises in TPIL and Logic and Proof.

  • A glossary and a cheat sheet like this one will be helpful.

Ideas for a table of contents

Basic skills

  • equational reasoning
  • universal quantifiers and implication
  • conjunction and negation
  • disjunctions
  • existential quantifiers

(JA: I think I know how to do this now. I'll have a draft soon. I will use examples of proving ring identities and proving general facts from lattice axioms. These are a good way to introduce the basics, they are mathematically interesting, and the information will be useful later on. Also complete lattices: using lubs to define a glb is a good example of something that little more than pure logic.)

Fundamentals

  • sets (union, Union, sUnion, bUnion...)
  • relations (order relations and equivalence relations)
  • functions (injective / surjective, inverses, etc.)
  • finite sets and cardinality (a bit of combinatorics with finsets)
  • the finite (Cantor Bernstein)

Numbers

  • proof by induction
  • there exist infinitely many primes
  • integers, rationals, and reals
  • fighting coercion hell; test case: proving that 1/(n+1) tends to zero (with home brewed limit definition, no filters).

Algebra

  • some elementary group theory
  • Lagrange?
  • Sensitivity conjecture?
  • linear algebra?
  • lattices and Galois connections

This is crucial because it is a huge barrier to using mathlib. You cannot do subgroups, ideals, or any topology or analysis without lattices. Galois connections are less necessary to use those theories, but they are crucial for anyone who wants to get even a tiny bit of understanding of how things are set up.

Topology

  • filters
  • topological spaces and metric spaces (with a pinch of uniform spaces). The forgetful inheritance pattern
  • big example: IVT

Calculus

  • derivatives
  • integrals
  • find some nice example that brings everything together
Clone this wiki locally