The classification below is somewhat arbitrary, since some of these papers could possibly fit more than one topic.
Mathematics:
Algebraic structures:
The Interpretation Lifting Theorem for C-systems, Theory and Applications of Categories, Vol. 38, 2022, No. 7, article.
Homotopical structures:
On a Model Invariance Problem in Homotopy Type Theory, Applied Categorical Structures, 2019, article.
On the Inadequacy of the Projective Structure with Respect to the Univalence Axiom, 23 pages. arXiv:1712.0265
Books:
Homotopy Type Theory : Univalent Foundations of mathematics, as part of The Univalent Foundations Program, Institute for Advanced Study, Princeton, 2013. book freely available online
Expository writing:
What is a Scheme in Algebraic Geometry? A Problem-Oriented Approach, draft
Computer science:
Artificial Intelligence/Machine Learning/Natural Language Processing:
Bourbaki: Self-Generated and Goal-Conditioned MDPs for Theorem Proving, 2025, preprint v1 (as of July 4th 2025, SOTA on PutnamBench at the 7B scale)
Three Conjectures on Upscaling and Downscaling LLMs, LMCRC, 7th Nov. 2024, slides
with Yiannos Stathopoulos and Lawrence Paulson, A Parallel Corpus of Natural Language and Isabelle Artefacts, AITP 2022, abstract
Quantum:
with Hanna Lachnitt and Yijun He, Certified Quantum Computation in Isabelle/HOL, Journal of Automated Reasoning, 65(5), 691-709, 2020 (arXiv version)
with Yijun He, Comment on "Quantum Games and Quantum Strategies", 2019, arXiv:1911.09354
Other Journal articles:
with Lawrence Paulson and Wenda Li, Simple Type Theory is not too Simple: Grothendieck's schemes without dependent types, Experimental Mathematics, 2022, article
Workshop and conference refereed articles:
with Manuel Eberl, Lawrence Paulson and Wenda Li, Formalising Half of a Graduate Textbook in Number Theory, ITP 2024, article.
with Adrian Dona Mateo, Encoding Dependently-Typed Constructions into Simple Type Theory, CPP 2023, article.
with Yiannos Stathopoulos and Lawrence Paulson, A Parallel Corpus for Natural Language Machine Translation to Isabelle, CICM 2022, article available in the following proceedings.
with Nicolo Cavalleri, Elements of Differential Geometry in Lean, CEUR Workshop Proceedings of FMM 2021, the Fifth Workshop on Formal Mathematics for Mathematicians (part of CICM 2021), article.
Refereed book chapters:
Univalent Foundations and the UniMath Library : The Architecture of Mathematics, in Reflections on the Foundations of Mathematics, Synthese Library, 407, 2019, Springer. arXiv:1710.02723
Some computer code:
The Galois connection induced by an arbitrary relation, 2024.
Strict Omega Categories , Archive of Formal Proofs, 2023.
Grothendieck's Schemes in Algebraic Geometry , Archive of Formal Proofs, 2021.
Isabelle Marries Dirac: a Library for Quantum Computation and Quantum Information, Archive of Formal Proofs, 2020.
The Localization of a Commutative Ring, Archive of Formal Proofs, 2018.
Projective Geometry, Archive of Formal Proofs, 2018.
Things with ideas:
A Tale of Duality, Letter to the Editor, Notices of the American Mathematical Society, 69(1), January 2022, pdf
Hypercriticality, Hypocriticality and Hyperempathy, Letter to the Editor, Communications of the ACM, 64(12), December 2021, online version
A Replication Crisis in Mathematics? The Mathematical Intelligencer (2021)
Some Slides:
A Parallel Corpus for Autoformalisation, IRIF, November 21th 2022, slides
Machine Learning and Autoformalisation, LMF, November 16th 2022, slides
How to Do Maths without Dependent Types, IHES, June 15th 2022, slides
Textbooks:
with Alice Erlinger and Vincent Nolot, L'épreuve de mathématiques à Sciences Po, Ellipses, 2016, 304 pages (math textbook in French).
Translations:
with Julien Cantegreil et al, L'Ecole de New Haven de droit international, Editions A.Pedone, 2010. (International Law)