María Inés de Frutos-Fernández

I am María Inés, a researcher (chargée de recherche) at CNRS, attached to the Institut de Mathématiques de Jussieu-Paris Rive Gauche.

Previously, I have held postdoctoral positions at the University of Bonn, Universidad Autónoma de Madrid, and Imperial College London. Before joining Imperial College, I worked as an Assistant Professor (Profesor Ayudante Doctor) at Universidad Nebrija. I earned my PhD in Mathematics from Boston University in 2020, under the supervision of Jared Weinstein.

My main research interests are mathematical formalization and number theory.

Here is my CV.

Last updated: 2 November 2026.

Selected publications

Preprint

Formalizing Carleson’s Theorem in Lean

Lars Becker, María Inés de Frutos-Fernández, Leo Diedering, and 11 more authors

2026

Preprint

Abs Bib HTML PDF

We present the formalization of Carleson’s theorem in the proof assistant Lean. This paper describes the mathematical content, the organization of the project, the blue- print, and the main design decisions behind the formalization. It is the result of a large collaborative effort, written and developed in public.

@unpublished{CarlesonPaper,
  title = {Formalizing Carleson's Theorem in Lean},
  author = {{Becker}, Lars and {de Frutos-Fernández}, María Inés and {Diedering}, Leo and {van Doorn}, Floris and {Gouëzel}, Sébastien and {Karunus}, Evgenia and {van de Meent}, Edward and {Monticone}, Pietro and {Mulder-Sohn}, Jasper and {Portegies}, Jim and {Roos}, Joris and {Rothgang}, Michael and {Sundstrom}, James and {Tan}, Jeremy},
  note = {Preprint},
  year = {2026},
  url = {https://arxiv.org/abs/2609.31334},
}

CPP
Formalizing Polynomial Laws and the Universal Divided Power Algebra

Antoine Chambert-Loir and María Inés de Frutos-Fernández

In Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Rennes, France, 2026

Abs DOI Bib HTML PDF

The goal of this paper is to present an ongoing formalization, in the framework provided by the Lean/mathlib mathematical library, of the construction by Roby (1965) of the universal divided power algebra. This is an analogue, in the theory of divided powers, of the classical algebra of polynomials. It is a crucial tool in the development of crystalline cohomology; it is also used in p-adic Hodge theory to define the crystalline period ring. As an algebra, this universal divided power algebra has a fairly simple definition that shows that it is a graded algebra. The main difficulty in Roby’s theorem lies in constructing a divided power structure on its augmentation ideal. To that aim, Roby identified the graded pieces with another universal structure: homogeneous polynomial laws. We formalize the first steps of the theory of polynomial laws and show how future work will allow to complete the formalization of the above-mentioned divided power structure. We report on various difficulties that appeared in this formalization: taking care of universes, extending to semirings some aspects of the Mathlib library, and coping with several instances of "invisible mathematics".
@inproceedings{CLdFF26, title = {{Formalizing Polynomial Laws and the Universal Divided Power Algebra}}, author = {{Chambert-Loir}, Antoine and {de Frutos-Fernández}, María Inés}, year = {2026}, isbn = {9798400723414}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3779031.3779108}, doi = {10.1145/3779031.3779108}, booktitle = {Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs}, pages = {75–87}, numpages = {13}, keywords = {Lean, Mathlib, divided power algebra, formal mathematics, polynomial law}, location = {Rennes, France}, series = {CPP '26} }

ComposMath

The refined class number formula for Drinfeld modules

María Inés de Frutos-Fernández, Daniel Macías Castillo, and Daniel Martínez Marqués

Compositio Mathematica, 2026

Abs DOI Bib HTML PDF

Let K/k be a finite Galois extension of global function fields. Let E be a Drinfeld module over k. We state and prove an equivariant refinement of Taelman’s analogue of the analytic class number formula for (E, K/k), and derive explicit consequences for the Galois structure of the Taelman class group of E over K.

@article{RCNF,
  title = {The refined class number formula for Drinfeld modules},
  author = {{de Frutos-Fernández}, María Inés and {Macías Castillo}, Daniel and {Martínez Marqués}, Daniel},
  year = {2026},
  volume = {162},
  doi = {10.1017/S0010437X26103108},
  number = {4},
  pages = {852--903},
  journal = {Compositio Mathematica},
  url = {https://www.cambridge.org/core/journals/compositio-mathematica/article/refined-class-number-formula-for-drinfeld-modules/D22C391D65FB0B88ED9D30DA91237F62},
}

CPP
A Formalization of Complete Discrete Valuation Rings and Local Fields

María Inés de Frutos-Fernández and Filippo A. E. Nuccio Mortarino Majno di Capriglio

In Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, London, UK, 2024

Abs DOI Bib HTML PDF

Local fields, and fields complete with respect to a discrete valuation, are essential objects in commutative algebra, with applications to number theory and algebraic geometry. We formalize in Lean the basic theory of discretely valued fields. In particular, we prove that the unit ball with respect to a discrete valuation on a field is a discrete valuation ring and, conversely, that the adic valuation on the field of fractions of a discrete valuation ring is discrete. We define finite extensions of valuations and of discrete valuation rings, and prove some global-to-local results. Building on this general theory, we formalize the abstract definition and some fundamental properties of local fields. As an application, we show that finite extensions of the field Q_p of p-adic numbers and of the field F_p((X)) of Laurent series over F_p are local fields.
@inproceedings{dFN23, author = {{de Frutos-Fernández}, María Inés and {Nuccio Mortarino Majno di Capriglio}, Filippo A. E.}, title = {A Formalization of Complete Discrete Valuation Rings and Local Fields}, year = {2024}, isbn = {9798400704888}, publisher = {Association for Computing Machinery}, address = {New York, NY, USA}, url = {https://doi.org/10.1145/3636501.3636942}, doi = {10.1145/3636501.3636942}, booktitle = {Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs}, pages = {190--204}, numpages = {15}, keywords = {Lean, algebraic number theory, discrete valuation rings, formal mathematics, local fields, mathlib}, location = {London, UK}, series = {CPP 2024} }

ITP

Formalizing the Ring of Adèles of a Global Field

María Inés de Frutos-Fernández

In 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022

Abs DOI Bib HTML PDF

The ring of adèles of a global field and its group of units, the group of idèles, are fundamental objects in modern number theory. We discuss a formalization of their definitions in the Lean 3 theorem prover. As a prerequisite, we formalize adic valuations on Dedekind domains. We present some applications, including the statement of the main theorem of global class field theory and a proof that the ideal class group of a number field is isomorphic to an explicit quotient of its idèle class group.

@inproceedings{defrutosfernandez:LIPIcs.ITP.2022.14,
  author = {{de Frutos-Fernández}, María Inés},
  title = {{Formalizing the Ring of Ad\`{e}les of a Global Field}},
  booktitle = {13th International Conference on Interactive Theorem Proving (ITP 2022)},
  pages = {14:1--14:18},
  series = {Leibniz International Proceedings in Informatics (LIPIcs)},
  isbn = {978-3-95977-252-5},
  issn = {1868-8969},
  year = {2022},
  volume = {237},
  editor = {Andronick, June and de Moura, Leonardo},
  publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address = {Dagstuhl, Germany},
  url = {https://drops.dagstuhl.de/opus/volltexte/2022/16723},
  urn = {urn:nbn:de:0030-drops-167232},
  doi = {10.4230/LIPIcs.ITP.2022.14},
  annote = {Keywords: formal math, algebraic number theory, class field theory, Lean, mathlib}
}