Théo STOSKOPF
Postdoctoral Researcher
LIP, CASH team, École Normale Supérieure de Lyon, Inria
I am a postdoctoral researcher in the CASH team at ENS Lyon (Inria), under the supervision of Nicolas Tabareau and Cyril Cohen. My research focuses on AI-assisted formal reasoning and software verification with the Rocq and Lean proof assistants. I work on model–prover interaction, proof translation, tactic recommendation, and scalable infrastructure for training and evaluation.
My current research includes:
- Pile-of-Rocq and rocq-ml-toolbox (dataset, toolbox): a data and infrastructure stack for machine learning with Rocq. Pile-of-Rocq contains more than 47 million structured records extracted from 48 Rocq environments, while the companion tooling supports parallel prover interaction, evaluation, trajectory generation, and reinforcement-learning workflows.
- Tacq (repository, JFLA 2026 paper): a context-aware tactic recommender that enriches Rocq proof states with dependency, notation, and natural-language information.
- Babel-formal: Translation of Proofs between Lean and Rocq (MATH-AI@NeurIPS 2025 paper, repository): translation between Rocq and Lean using proof terms as a pivot language, including experiments in transferring proof styles such as vanilla Rocq to MathComp's SSReflect tactics.
- LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback (Rocqshop@ITP 2025 paper, repository): expert-reviewed natural-language documentation, retrieval, and autoformalisation resources for MathComp.
- Crrrocq (repository): an interactive theorem-proving system combining retrieval, reasoning, and feedback from Rocq to construct proofs incrementally.
During my PhD (2019–2024), I spent one year in industry as a Research Scientist in generative AI at Jumbo Mana. I designed and deployed AI pipelines for cultural and interactive applications, including speech recognition, speech synthesis, and large language models. I co-led Bonjour Vincent at the Musée d'Orsay and co-developed the Felon-E video game, presented at Gamescom and Paris Games Week 2023.
I studied mathematics at ENS Paris-Saclay, am an agrégé de mathématiques (national rank 24), and completed my PhD in mathematics under the supervision of Christian Gérard at the Laboratoire de Mathématiques d'Orsay.
Personal GitHub · Team GitHub · ORCID · LinkedIn · Email · Detailed CV
Recent Publications
-
Tacq – Context Aware Tactic Recommendation for Rocq
JFLA 2026 -
Babel-formal: Translation of Proofs between Lean and Rocq
MATH-AI@NeurIPS 2025 -
LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback
Rocqshop@ITP 2025
Recent Talks and Teaching
-
Introduction to transformers and their application to proof assistants
Invited lecturer, Proof Assistants and Applications Summer School, University of Strasbourg, 2026 -
AI-assisted formal reasoning — hands-on session
AI, Proof and Formalization Days, ENS Lyon, 2026 -
LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback
Rocqshop@ITP, 2025 -
Hands-on session
AI and Mathematics Conference, PSL, 2025