The Filter Game

The Filter Game is a Year 2 maths student group project at Imperial College London, authored by Jiale Miao (@Biiiilly), Yichen Feng, Lily Frost, Archie Prime and supervised by Prof. Kevin Buzzard (@kbuzzard).

This is an adaptation of the filter game to Lean 4.

Note: compared to the Natural Number Game, this game requires more advanced Lean knowledge, including lemma-like tactics (have or suffices) and the understanding of definitions of new types and functions (structure, def). If you are a beginner, you can try this game after completing NNG!


First install Git, Lean 4, Visual Studio Code and the Lean 4 extension by following the instructions here.

Then, open a terminal somewhere and type in the following commands one by one:

git clone
cd filter-game
lake exe cache get

The last step will download the Mathlib cache, and can take several minutes to complete. Upon completion, open the filter-game folder in VSCode and double-click the FilterGame/Filter.lean file on the left pane; VSCode should start downloading the required version of Lean automatically. After this completes, the yellow bars should soon disappear, and you are ready!


There are seven worlds in this game:

  • Filter.lean: this world contains the basic definition of filters.
  • Basis.lean: this world introduces filter bases, and discusses some of its properties.
  • Order.lean: given two filters (or filter bases) f and g, this world talks about the definition of f ≤ g.
  • Principal.lean: this world discusses "principal filters", or filters that can be generated from a single set.
  • Semilattice.lean: this world shows that the f ≤ g relation can be made into a "semilattice", by introducing a notion of "greatest lower bound".
  • Ultrafilter.lean: this world discusses "ultrafilters", or minimal proper filters.
  • Topology.lean: one of the application areas of filters is topology, and we will go through some of the results in this world.

General Tips

  • In Lean 4, you can now hover your mouse cursor over a tactic to see how it can be used. Or hover over the name of a lemma to see its statement. If you are playing in a real Lean environment, hovering over lemma names in the infoview (the panel on the right displaying your goals) also works.
  • To use what you already have:
    • If you have a function, or anything like p → ... or ∀ x, ..., you simply supply arguments to it, or use specialize.
    • If you have an equality, use rw.
    • In all other cases, use pattern-matching have (simple), cases (medium) or induction (powerful) on what you have.
  • To make something required by the goal:
    • If the goal is in the form p → ... or ∀ x, ..., use intros.
    • If you need to prove an equality, use rw.
    • In all other cases, use either exact (simple), apply (medium) or refine (powerful). If you don't know which lemma to use, try constructor.
  • To progress step-by-step, use have or suffices.
  • To temporarily save an expression, use let.
  • Special-purpose tactics:
    • Use conv if you want to have more control over rw.
    • Use simp_rw to rewrite inside function bodies or . (Plain rw does not work in this case.)
    • Use simp to carry out chains of rws. (Or when some horribly-complicated thing pops up in the infoview.)
    • Use apply? to search the Mathlib.
    • Use ac_rfl, ring, linarith, tauto (or, finally, aesop?) on their respective expertise areas.