Delamano

This is a web platform built to support second-semester CS students at Universidad de los Andes with their Discrete Math course.

The platform gives them exercises related to the class, allows them to input the steps they believe would solve each problem, and checks whether those steps are valid. Given that Universidad de los Andes is based in Bogotá, a significant part of the site is written in Spanish.

It was inspired by ADAM’s Lean Game Server and uses the same license.

The platform

On the landing page, students can choose a topic they want to work on (based on the actual syllabus at Universidad de los Andes).

After selecting a topic, they’ll see “worlds” (the big circles) and “levels” (the smaller ones). Each level is a discrete math exercise, like the ones they face in class.

Inside each level, the UI is split into three main parts: the middle block shows the exercise, the left block gives hints, and the right block lists the theorems they can use.

For instance, if a student types definicion_implicacion, the proof advances. Once they enter a full sequence of steps that leads the statement to a tautology, the platform confirms that their proof is correct. This way, students can practice and learn even when no one’s around to help.

Running the project

To run the project, you’ll need to install a couple of less-common dependencies:

• Lean4: a proof-oriented programming language that’s super useful for working with theorems. You can install it through VSCode.
• Elan: if you don’t want to use VSCode, Elan helps you manage Lean4 installations.

You’ll also need to build the platform’s levels before using it. You can run npm build_games to do that, but this currently installs the same library in all game subfolders (which will be fixed in a future release). Alternatively, you can choose to build a specific game—check the build_games command definition to see how.

Once everything is built, run npm start to launch the development version and start playing around.