Anyone taking this course for a credit will need to complete a (group) project.

Deadline for choosing projects is on the 11th of March.

What is a project?

  • A project can be a theorem you want to formalise:
    • This can be some theorem from a lecture/book you like.
    • This can be a theorem that already exists in mathlib. You can reinvent the wheel!
    • This can be something new you want to add to mathlib.
    • It can also be some result from your research.

      Note. In some cases, formalising the statement of the theorem can be enough.

  • A project can also be a game that explains a topic in mathematics using Lean
    • This can be a topic in Analysis, Topology, Algebra, Graph theory, etc…
    • Check out the template.

Logistics

  • You are expected to join the GitHub Organisation glams-lean-2024 by sending us your GitHub usernames
  • Expected deadline is at the end of April
  • You are expected to give a presentation afterwards