Exercises in Formalizing Mathematics with Lean 4

This repository contains solutions to the exercises of the course Formalising Mathematics by Kevin Buzzard at Imperial College London.

• 1: Logic

  • 1: The implication
  • 2: True and False
  • 3: The negation
  • 4: The conjunction
  • 5: The bi-implication
  • 6: The disjunction

• 2: Reals numbers

  • 1: Equalities and inequalities between numerical expressions
  • 2: Algebra in the real numbers
  • 3: Limits of sequences
  • 4: The linarith tactic
  • 5: Limits of sequences (2)
  • 6: Limits of sequences (3)

• 3: Functions

  • 1: Functions in Lean