Robo

A game for learning Lean 4 in which a cute little smart-elf named Robo joins you on your exploration of a universe inhabited by formalosophers.

The game is currently available only in German. It can be played at the Lean Game Server.

Game content

Planetkey mathematical contentLean tactics introducedBoss level
Logopropositional logic: ∧, ∨, ¬rfl, left, right,tauto, …
Implispropositional logic: ⇒, ⇔apply, intro, revert, rw, …A ⇒ B equivalent to ¬ A ∨ B
Saturnelementary arithmetic, polynomialsring, rw for equationsa well-known polynomial sums-of-squares formula
Quantuspredicate logic, even/odd numbersuse, obtain, decide, push_negDrinker's paradox
Lunainequalitieslinarith, omega
Spinozaproof structuringsuffices, by_contra, contrapose
Babylon∑ notation, inductioninduction'sum of cubes
Piazzabasic set theoryext, simp
Pradoprime numbersexactly one even prime
Euklid∏ notationinfinitely many primes
Vietamaps (between types)funextanother induction exercise
Eposurjective maps, axiom of choicechoosemap surjective ⇔ has right inverse
Monoinjective mapsmap injective ⇔ has left inverse
Isobijective mapsmap bijective ⇔ has inverse
Samarkand(pre)images of subsetsmap surjective ⇔ induced contravariant map on powersets injective
Cantorfixed points of mapsℕ-valued sequences uncountable
Robotswanamatrices, tracecharacterization of trace map
Ciao(good-bye planet)

Contribution

Bugs

For small content fixes like spelling mistakes, missing hints, missing documentation, or other things that were unclear or you've struggled with, please open an Issue or PR here!

Issues concerning the underlying software are better placed in the lean4game repo.

New Content

Contributions of new planets are welcome! Each planet in the game talks about a new topic in a standard Mathematics undergrad (bachelor) curriculum at university.

Please follow our Contribution Guide, which helps you create new content step-by-step.

Technical

Building

You can build the game just like a regular Lean project. In particular, inside Robo/ you should call

lake update -R
lake build

Note: the repo is set up in a way that lake update is NOT destructive and can be called liberally anytime. (This is not true for other Lean projects)

Note: lake update will call the two commands lake exe cache get (retrieve the latest mathlib cache) and lake build gameserver (build the gameserver executable); so if you're not calling lake update, you should call these two commands manually.

Updating Lean/mathlib

In order to update the Lean version used by the game, you should follow these steps:

  • See what versions are available of lean4game: Releases
  • Modify the file lean-toolchain to contain the string leanprover/lean4:v4.7.0 where v4.7.0 is replaced by the newest version available.
  • Call lake update -R and lake build. Your game now uses the specified Lean version and the corresponding mathlib release.

Refactoring existing worlds

The bash script sofi.sh (sort out filnames and imports), contained in the root folder, can help restructure existing worlds, see the documentation.