Théo STOSKOPF

Postdoctoral Researcher

LIP, CASH team, École Normale Supérieure de Lyon, Inria

I am a postdoctoral researcher at ENS Lyon in the CASH team (Inria), under the supervision of Nicolas Tabareau and Cyril Cohen. I work on the integration of large language models with proof assistants (Rocq and Lean 4).

My current research focuses on automatic theorem proving and translation between proof assistants. I am exploring several aspects of this direction:

• Crrrocq (repository): a model trained to use retrieval, reasoning, and feedback from Rocq to generate proofs step by step.
• Babel-formal: Translation of Proofs between Lean and Rocq (MATH-AI@NeurIPS 2025, repository): a model trained to translate proofs between Rocq and Lean by using proof terms as a pivotal language, and also experiments with transferring proof styles (e.g., vanilla Rocq to MathComp's SSReflect tactics).
• LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback (Rocqshop@ITP 2025, repository): a project focused on creating a dataset of docstrings for MathComp with expert feedback, and training models for auto-formalization (translation of informal statements into formal ones) and annotation (formal statement into informal statement).

During my PhD (2019–2024), I spent one year in industry (2023–2024) as a Research Scientist in generative AI at Jumbo Mana, where I trained and deployed AI pipelines for interactive applications (cultural mediation, entertainment), including speech recognition (ASR), speech synthesis (TTS), and large language models. This experience gave me practical insights into building AI systems that work in real-world contexts. I co-led Bonjour Vincent project @Orsay Museum, Felon-E video game, presented @Gamescom 2023, and @PGW 2023.

Normalien, studied mathematics at ENS Paris-Saclay, agrégé de mathématiques (national rank 24), completed my PhD under the supervision of Christian Gérard in mathematics (LMO).

Personal GitHub · Team GitHub · LinkedIn · Email · Detailed CV

---

Recent Works

• Crrrocq, [link].
  

• Babel-formal: Translation of Proofs between Lean and Rocq, [link].
  

• LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback, [link].
  

Recent Talks

• LLM4Docq: Bootstrapping Documentation for MathComp with LLMs and Expert Feedback
  rocqshop@ITP, 2025

• Hands-on session
  AI and maths conference, PSL, 2025

• Robustness in Deep Learning: From Data to Inference
  LCIS Scientific Day, 2025

• MathAData
  AI Action Summit, Mines Paris-PSL