Terence Tao baut sein Logik-Lehrbuch zum Spiel um – mit einem Coding-Agent
Lean Grimoire
Terence Tao hat sein interaktives JavaScript-Lehrbuch „QED“ von 2018 mit einem Coding-Agent neu aufgelegt: Statt Propositional- und Prädikatenlogik trocken zu üben, sammelt man in einem „Crafting Game“ Regeln, um aus Hypothesen Schlüsse zu ziehen. Neu ist unter anderem die Option, den aktuellen Spielstand als laufenden Lean-Beweis anzuzeigen. Ein „Fantasy-Modus“ verwandelt Aussagen in Tränke und Ausdrücke in Schriftrollen. Tao sucht nun Playtester, die das Werkzeug als Lehrmittel für Beweise und Lean erproben.
Für den Spaß habe ich außerdem einen „Fantasy-Modus“ hinzugefügt, in dem verschiedene Spielelemente mit fantasyhaften Flavor-Texten dargestellt werden – mathematische Aussagen werden etwa zu „Tränken“, mathematische Ausdrücke zu „Schriftrollen“ und so weiter.
- torben-friis
Was für ein Durcheinander von einem Lernspiel.
Sorry, dass ich so negativ bin, aber man kann diese LLM-artige Einleitung kaum parsen, und diese Steuerelemente wirken wie ein halbfertiges persönliches Obsidian-Dokument.
Irgendwie seltsam für Tao, ich erinnere mich, dass seine Mathenotizen ziemlich zugänglich und gut geschrieben waren.