Contexte et objectifs
En 2018, Terry Tao a publié QED, un manuel interactif JavaScript destiné à enseigner la logique propositionnelle et du premier ordre sous forme de jeu de construction. Le projet proposait aux apprenants d’appliquer des règles logiques pour transformer un ensemble d’hypothèses en une conclusion cible. Après plusieurs mois d’interruption, l’auteur a repris le travail en 2026 en s’appuyant sur des agents de codage modernes afin de moderniser l’outil et d’y intégrer le système de preuve automatisé Lean.
Architecture technique et intégration de Lean
La refonte repose sur une pile JavaScript pure, conservant le moteur de jeu original tout en ajoutant une couche d’interfaçage avec Lean. Cette intégration nécessite la compilation du noyau Lean en WebAssembly, ce qui permet d’exécuter le vérificateur de preuves directement dans le navigateur sans serveur dédié. Le front‑end communique avec le module WebAssembly via l’API postMessage, transmettant l’état du jeu sous forme de termes Lean et récupérant la preuve partielle générée. Le choix d’une architecture client‑side garantit une latence minimale, indispensable pour un retour visuel instantané lors de la manipulation des règles logiques.
Nouvelles fonctionnalités et implications pédagogiques
Deux ajouts majeurs sont décrits dans le post : l’affichage d’une preuve Lean en cours d’élaboration et le « fantasy mode ». Le premier expose, ligne par ligne, le script Lean correspondant à chaque mouvement du joueur, offrant ainsi une trace formelle que l’étudiant peut comparer à la solution attendue. Cette transparence renforce la compréhension du lien entre la logique informelle du jeu et la syntaxe stricte de Lean. Le second mode remplace les termes mathématiques par des métaphores fantasy – les propositions deviennent des « potions », les expressions des « parchemins » – afin de réduire l’appréhension initiale et d’augmenter l’engagement ludique. Aucun chiffre de performance n’est fourni, mais la combinaison d’une UI JavaScript réactive et d’un moteur Lean WebAssembly montre que le rendu reste fluide sur les navigateurs modernes.
Limites et perspectives
Le projet reste en phase de test utilisateur ; aucune donnée quantitative sur l’efficacité pédagogique n’est présentée. L’utilisation de WebAssembly implique une taille de téléchargement supérieure à celle d’une application JavaScript classique, ce qui peut freiner l’accès sur des connexions limitées. De plus, la génération de preuves dépend de la capacité de l’agent de codage à traduire correctement les règles du jeu en code Lean, un processus qui peut introduire des bugs subtils non détectés sans validation exhaustive. Les prochains développements pourraient inclure un mode multijoueur, des métriques d’apprentissage et une intégration avec des plateformes d’enseignement en ligne.
