CANUM 2026 : mini-symposium "IA pour les mathématiques"

Programme

jeudi 04/06

17:00 17:40

Formalizing at Scale

Ahmad Rammal

We present AutoformBot, a multi-agent system for building an Autoformalized Textbook Library. At Scale (ATLAS) in Lean 4. AutoformBot orchestrates thousands of LLM agents, equipped with formal verification tools, dependency-aware task scheduling, and collaborative version control, to translate informal textbook prose into machine-checked definitions and proofs. We apply our methods to a corpus of over 20 open-access textbooks spanning analysis, algebra, topology, combinatorics, and probability, producing ATLAS : a verified library of over 50,000 Lean 4 declarations and 500 thousand lines of code. We release two artifacts : (i) AutoformBot, the open-source multi-agent framework ; and (ii) ATLAS, the resulting formal library. Our results suggest that autoformalizing the core content of graduate-level mathematics at scale is now economically and technically feasible. This opens the door to the automated verification of both human- and machine-generated mathematics at a research level.

17:40 18:20

Axplorer - Construction d'exemples utilisant des méthodes d'IA générative

François Charton

Un modéle d’IA générative peut être entrainé pour produire des objets mathématiques particuliers, par exemple de bonnes solutions à des problèmes d’optimisation discrète, ou des contre-exemples falsifiant des conjectures. Je présente la méthode générale, et son application à un problème difficile, le nombre de graphes sans cycle d’ordre 4.

18:20 19:00

Agentic approach for neural theorem proving in Rocq

Jules Viennot

Dans cet exposé, nous allons parler de preuve assistée par Large Language Models (LLM). En effet, leurs raisonnements sont de plus en plus performants, et la preuve mathématique formelle est devenue un cadre de choix pour évaluer ces capacités : elle offre une garantie objective de correction et de validité, là où d’autres méthodes nécessitent une relecture humaine. Dans cet exposé, nous commençons par faire le point sur l’actualité, quand de plus en plus de modèles généralistes, comme ceux d’OpenAI, de Google ou d’Anthropic, repoussent les limites du possible. Ces découvertes sont propulsées grâce à un nouveau paradigme dans l’utilisation des LLMs : les agents. Un agent est un modèle ayant accès à des outils et qui choisit ses actions en fonction des observations qu’il fait de son environnement, décuplant les capacités d’un LLM classique. Mais au-delà de ces avancées, nous nous intéressons à comprendre ce qui aide vraiment ces modèles à prouver. Nous présentons donc une série d’explorations menées par notre équipe autour de cette question. Nous commencerons par rocq-mcp, un serveur MCP qui permet à un agent de dialoguer directement avec l’assistant de preuve Rocq. Nous parlerons ensuite de Tacq, qui explore dans quelle mesure donner du contexte mathématique pertinent à un LLM améliore ses capacités de preuve. Nous présenterons également une étude sur la résolution des problèmes du concours Putnam avec Claude, et comment un modèle peut lui-même choisir les outils dont il a besoin. Enfin, nous terminerons par Proof Agent, un travail en cours qui tire parti des erreurs d’un gros modèle privé pour guider un modèle open source plus petit vers de meilleurs résultats.