Publications
2026
- PreprintFormalizing Carleson’s Theorem in LeanLars Becker, María Inés de Frutos-Fernández, Leo Diedering, and 11 more authors2026Preprint
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}, } - CPPFormalizing Polynomial Laws and the Universal Divided Power AlgebraAntoine Chambert-Loir and María Inés de Frutos-FernándezIn Proceedings of the 15th ACM SIGPLAN International Conference on Certified Programs and Proofs, Rennes, France, 2026
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} } - ComposMathThe refined class number formula for Drinfeld modulesMaría Inés de Frutos-Fernández, Daniel Macías Castillo, and Daniel Martínez MarquésCompositio Mathematica, 2026
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}, }
2025
- PreprintA blueprint for the formalization of Carleson’s theorem on convergence of Fourier seriesLars Becker, María Inés de Frutos-Fernández, Leo Diedering, and 14 more authors2025Preprint
This paper is the blueprint underlying the Lean formalization of the proof of Carleson’s classical result asserting almost everywhere convergence of Fourier series of continuous functions. We break up the proof into two steps, a reduction of the classical result to a new theorem that appears in a sibling communication and a proof of this new theorem, which is also detailed as blueprint in this paper. An early version of this blueprint was used to initiate the Lean formalization. During the formalization, many contributors elaborated the blueprint with minor corrections, modifications and extensions. The final version is presented here as a guide through the accompanying Lean code.
@unpublished{CarlesonBlueprint, title = {A blueprint for the formalization of Carleson's theorem on convergence of Fourier series}, 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 {Jamneshan}, Asgar 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 {Srivastava}, Rajula and {Sundstrom}, James and {Tan}, Jeremy and {Thiele}, Christoph}, note = {Preprint}, year = {2025}, url = {https://arxiv.org/abs/2405.06423}, } - ITPA Formalization of Divided Powers in LeanAntoine Chambert-Loir and Marı́a Inés Frutos-FernándezIn 16th International Conference on Interactive Theorem Proving (ITP 2025), 2025
Given an ideal I in a commutative ring A, a divided power structure on I is a collection of maps {\gamma_n \colon I \to A}_n ∈\mathbbN, subject to axioms that imply that it behaves like the family {x \mapsto \fracx^nn!}_n ∈\mathbbN, but which can be defined even when division by factorials is not possible in A. Divided power structures have important applications in diverse areas of mathematics, including algebraic topology, number theory and algebraic geometry. In this article we describe a formalization in Lean 4 of the basic theory of divided power structures, including divided power morphisms and sub-divided power ideals, and we provide several fundamental constructions, in particular quotients and sums. This constitutes the first formalization of this theory in any theorem prover. As a prerequisite of general interest, we expand the formalized theory of multivariate power series rings, endowing them with a topology and defining evaluation and substitution of power series.
@inproceedings{CLdFF25, author = {Chambert-Loir, Antoine and de Frutos-Fern\'{a}ndez, Mar{\'\i}a In\'{e}s}, title = {{A Formalization of Divided Powers in Lean}}, booktitle = {16th International Conference on Interactive Theorem Proving (ITP 2025)}, pages = {4:1--4:17}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, isbn = {978-3-95977-396-6}, issn = {1868-8969}, year = {2025}, volume = {352}, editor = {Forster, Yannick and Keller, Chantal}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, url = {https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.ITP.2025.4}, urn = {urn:nbn:de:0030-drops-246038}, doi = {10.4230/LIPIcs.ITP.2025.4}, annote = {Keywords: Formal mathematics, algebraic number theory, commutative algebra, divided powers, Lean, Mathlib} }
2024
- CPPA Formalization of Complete Discrete Valuation Rings and Local FieldsMaría Inés de Frutos-Fernández and Filippo A. E. Nuccio Mortarino Majno di CapriglioIn Proceedings of the 13th ACM SIGPLAN International Conference on Certified Programs and Proofs, London, UK, 2024
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} }
2023
- ITPFormalizing Norm Extensions and Applications to Number TheoryMaría Inés de Frutos-FernándezIn 14th International Conference on Interactive Theorem Proving (ITP 2023), 2023
The field R of real numbers is obtained from the rational numbers Q by taking the completion with respect to the usual absolute value. We then define the complex numbers C as an algebraic closure of R. The p-adic analogue of the real numbers is the field Q_p of p-adic numbers, obtained by completing Q with respect to the p-adic norm. In this paper, we formalize in Lean 3 the definition of the p-adic analogue of the complex numbers, which is the field C_p of p-adic complex numbers, a field extension of Q_p which is both algebraically closed and complete with respect to the extension of the p-adic norm. More generally, given a field K complete with respect to a nonarchimedean real-valued norm, and an algebraic field extension L/K, we show that there is a unique norm on L extending the given norm on K, with an explicit description. Building on the definition of C_p, we formalize the definition of the Fontaine period ring B_HT and discuss some applications to the theory of Galois representations and to p-adic Hodge theory. The results formalized in this paper are a prerequisite to formalize Local Class Field Theory, which is a fundamental ingredient of the proof of Fermat’s Last Theorem.
@inproceedings{defrutosfernandez:LIPIcs.ITP.2023.13, author = {{de Frutos-Fernández}, María Inés}, title = {{Formalizing Norm Extensions and Applications to Number Theory}}, booktitle = {14th International Conference on Interactive Theorem Proving (ITP 2023)}, pages = {13:1--13:18}, series = {Leibniz International Proceedings in Informatics (LIPIcs)}, isbn = {978-3-95977-284-6}, issn = {1868-8969}, year = {2023}, volume = {268}, editor = {Naumowicz, Adam and Thiemann, Ren\'{e}}, publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik}, address = {Dagstuhl, Germany}, url = {https://drops.dagstuhl.de/opus/volltexte/2023/18388}, urn = {urn:nbn:de:0030-drops-183880}, doi = {10.4230/LIPIcs.ITP.2023.13}, annote = {Keywords: formal mathematics, Lean, mathlib, algebraic number theory, p-adic analysis, Galois representations, p-adic Hodge theory} }
2022
- JTNBModuli Spaces of Shtukas over the Projective LineMaría Inés de Frutos-FernándezJournal de théorie des nombres de Bordeaux, 2022
We provide explicit equations for moduli spaces of Drinfeld shtukas over the projective line P^1 with Γ(N), Γ_1(N) and Γ_0(N) level structures, where N is an effective divisor on P^1. If the degree of N is high enough, these moduli spaces are relative surfaces. We study some invariants of the moduli space of shtukas with Γ_0(N) level structure for several degree 4 divisors on P^1.
@article{JTNB22, title = {Moduli Spaces of Shtukas over the Projective Line}, author = {{de Frutos-Fernández}, María Inés}, journal = {Journal de théorie des nombres de Bordeaux}, volume = {34}, number = {2}, pages = {393--418}, year = {2022}, doi = {10.5802/jtnb.1207}, url = {https://jtnb.centre-mersenne.org/articles/10.5802/jtnb.1207/}, } - ITPFormalizing the Ring of Adèles of a Global FieldMaría Inés de Frutos-FernándezIn 13th International Conference on Interactive Theorem Proving (ITP 2022), 2022
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} }
2021
- SISYComputing Rational Points on Rank 0 Genus 3 Hyperelliptic CurvesMaría Inés de Frutos-Fernández and Sachi HashimotoIn Arithmetic Geometry, Number Theory, and Computation, 2021
We compute rational points on genus 3 odd degree hyperelliptic curves C over ℚ that have Jacobians of Mordell–Weil rank 0. The computation applies the Chabauty–Coleman method to find the zero set of a certain system of p-adic integrals, which is known to be finite and include the set of rational points C(ℚ). We implemented an algorithm in Sage to carry out the Chabauty–Coleman method on a database of 5870 curves.
@inproceedings{10.1007/978-3-030-80914-0_14, author = {{de Frutos-Fernández}, María Inés and Hashimoto, Sachi}, editor = {Balakrishnan, Jennifer S. and Elkies, Noam and Hassett, Brendan and Poonen, Bjorn and Sutherland, Andrew V. and Voight, John}, title = {Computing Rational Points on Rank 0 Genus 3 Hyperelliptic Curves}, booktitle = {Arithmetic Geometry, Number Theory, and Computation}, year = {2021}, publisher = {Springer International Publishing}, address = {Cham}, pages = {449--460}, isbn = {978-3-030-80914-0}, } - PreprintRational linear subspaces of hypersurfaces over finite fieldsMaría Inés de Frutos-Fernández, Sumita Garai, Kelly Isham, and 2 more authors2021Preprint
Fix positive integers n,r,d. We show that if n,r,d satisfy a suitable inequality, then any smooth hypersurface X⊂P^n defined over a finite field of characteristic p sufficiently large contains a rational r-plane. Under more restrictive hypotheses on n,r,d we show the same result without the assumption that X is smooth or that p is sufficiently large.
@unpublished{arXiv21, title = {Rational linear subspaces of hypersurfaces over finite fields}, author = {{de Frutos-Fernández}, María Inés and Garai, Sumita and Isham, Kelly and Murayama, Takumi and Smith, Geoffrey}, note = {Preprint}, year = {2021}, url = {https://arxiv.org/abs/2111.10976/}, }
2020
- ThesisModularity of Elliptic Curves Defined over Function Fields (PhD Thesis)María Inés de Frutos-FernándezProQuest Dissertations and Theses, 2020
We provide explicit equations for moduli spaces of Drinfeld shtukas over the projective line with Γ(N), Γ_1(N) and Γ_0(N) level structures, where N is an effective divisor on P^1. If the degree of N is big enough, these moduli spaces are relative surfaces. We study how the moduli space of shtukas over P1 with Γ_0(N) level structure, Sht^{2,tr}(Γ_0(N)), can be used to provide a notion of motivic modularity for elliptic curves defined over function fields. Elliptic curves over function fields are known to be modular in the sense of admitting a parametrization from a Drinfeld modular curve, provided that they have split multiplicative reduction at one place. We conjecture a different notion of modularity that should cover the curves excluded by the reduction hypothesis. We use our explicit equations for Sht^{2,tr}(Γ_0(N)) to verify our modularity conjecture in the cases where N = 2(0) + (1) + (∞) and N = 3(0) + (∞).
@article{PhD_thesis, author = {{de Frutos-Fernández}, María Inés}, year = {2020}, title = {Modularity of Elliptic Curves Defined over Function Fields (PhD Thesis)}, journal = {ProQuest Dissertations and Theses}, pages = {108}, keywords = {Drinfeld shtukas; Elliptic curves; Function fields; Modularity; Moduli spaces; Number theory; Mathematics; 0405:Mathematics}, isbn = {9798678170910}, language = {English}, url = {https://open.bu.edu/handle/2144/41489}, }
Other Writing
2014
- ThesisEl problema del logaritmo discreto para curvas elípticas y sus aplicaciones criptográficasMaría Inés de Frutos-Fernández2014Trabajo de Fin de Grado/Senior Thesis
We present some cryptographical applications of the discrete logarithm problem over elliptic curves, including Diffie-Hellman key exchange, Massey-Omura encryption and ECDSA digital signatures. We analyze some general attacks on the DLP: Baby-Step Giant-Step, Pollard’s rho algorithm and Silver-Pohlig-Hellman attack. We also describe two specifics attacks: the subexponential algorithm Index Calculus, which works over F_q^*, and Xedni Calculus, which is an attack on the DLP over elliptic curves. Finally, we compare the performances of several attacks over F_q^* and E(F_q): Baby-Step Giant-Step, four variants of Pollard’s rho method and Index Calculus (the last one, only over F_q^*). We conclude that, on groups of the sizes we consider, Pollard’s rho attack works best for computing isolated logarithms, while Index Calculus is the fastest method when several attacks need to be made.
@unpublished{senior_thesis, title = {El problema del logaritmo discreto para curvas elípticas y sus aplicaciones criptográficas}, author = {{de Frutos-Fernández}, María Inés}, note = {Trabajo de Fin de Grado/Senior Thesis}, year = {2014}, }