Nach zweijähriger Entwicklungszeit ist das Lernspiel Robo bereit für den Praxistest. Das Spiel vermittelt den Umgang mit dem interaktiven Beweisassistenten Lean anhand verschiedener Themen aus der Eingangsphase des Mathematikstudiums. Es gilt beispielsweise per Induktion diverse Summenformeln zu beweisen, nachzuweisen, dass eine Abbildung genau dann surjektiv ist, wenn sie ein Rechtsinverses besitzt, zu zeigen, dass es überabzählbar viele Folgen natürlicher Zahlen gibt, oder die Spur als Abbildung auf dem Raum der quadratischen Matrizen zu charakterisieren. Das Spiel kommt beispielsweise im Seminar „Game over oder QED?“ (Bachelor-Studiengang Mathematik) im Sommersemester 2025 zum Einsatz. Es eignet sich aber auch hervorragend zum Selbststudium.

Die Entwicklung des Spiels wurde im Rahmen des Programms Freiraum 2022 von der Stiftung Innovation in der Hochschullehre finanziert.