After reading Terence Tao’s article on how proof checkers can allow non-mathematicians to contribute to cutting-edge maths, I decided to give interactive LEAN games a spin.
I started with the Lean 4 version of Natural Number World and then moved to Lean intro to logic.
A few notes for fellow beginners:
The instructions are incomplete, likely because the materials were designed to accompany an Imperial College maths course. It is therefore useful to look at the answers within the source code, rather than struggle in.
It is not easy: bear in mind that Tao himself spent 3 hours on (the old version) of Natural Number World and didn’t finish in one go! Tao used GPT-4 to help with the puzzles.
Specifically for Lean intro to logic
Do Redux: ∧ World before Implication world
Check answers in advance, particularly for the Implication world.
The text does not give a full explanation of the tools available. Moreover, 3 to 4 alternative equivalent notations are introduced very quickly, and someone without background is bound to be confused.
For my part I simply stuck to the simplest formulation, i.e. for
Objects:
CDS: Prop
Assumptions:
h: C ∧ D → S
Goal:
C → D → S
I used
have x := fun (C D) => h (and_intro C D)
As opposed to the notations shown in the source code.