Skip to content

Home

Jump to bottom
Patrick Massot edited this page Apr 29, 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

Maybe follow Patrick's strategy?

  • equational reasoning
  • inequalities (basically using lemmas, forall, and implication)
  • disjunctions
  • negations
  • existential quantifiers

In Patrick's strategy, negations come after everything else. They are really tricky.

Sets, relations, and functions

Any objection to just doing the usual things? Set identities, order and equivalence relations, injective functions.

We can do something on finite sets and cardinalities (though this may mean fighting with the current mathlib).

Numbers

What goes here? Proof by induction? Primes and gcd?

Patrick thinks the main thing here is fighting coercion hell. Test case: proving that 1/(n+1) tends to zero (with home brewed limit definition, no filters).

Algebra

  • Elementary group theory?
  • rings
  • linear algebra

Lattices and Galois Connections

  • definition of lattices
  • complete lattices
  • Galois connections

Patrick thinks 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 and analysis

  • filters
  • topological spaces and metric spaces (with a pinch of uniform spaces). The forgetful inheritance pattern
  • derivatives
  • integrals
Clone this wiki locally