Welcome to The Filter Game. Want to know the magic of filters in mathematics? Play it!

If you don't have Lean installed in your computer, don't worry! You can play online using Gitpod (wait a minute for set up). After everything is set up, open up the src/game directory on the left, and start with level_00_basic.lean.

If you have installed Lean, that's perfect!

You can open the terminal and insert:

leanproject get Biiiilly/filter

Then, you can open the folder where it's installed and start the game!

There are seven levels in this game:

• Level 0 : This level contains basic contents of filters. There is no puzzle in this level.

• Level 1 : We introduce the filter basis and discuss relevant properties of it in this level.

• Level 2 : Given two filters (or filter basis) F and G, we talk about how to define F ≤ G in this level.

• Level 3 : This level discusses the principal filters and relevant properties.

• Level 4 : This level discusses the ultrafilters which is the minimal (maximal in the set order) proper filterand relevant properties.

• Level 5 : One of the applications of filters is about topology, and we will go through some of them in this level.

• Level 6 : This level contains some challenging puzzles.

It's recommended to start with level 0, then go to level 1...

• Everyone in our group: Yichen Feng, Lily Frost, Archie Prime

• Our supervisor: Professor Kevin Buzzard