arXiv subjects

Floris van Doorn

Publications and source records attributed to Floris van Doorn.

16 recordsLinked to original sources

arXiv2026

A blueprint for the formalization of norm-variation of multiple ergodic averages for commuting transformations

This blueprint serves as a companion to a forthcoming, shorter traditional mathematical paper. The purpose of this blueprint is two-fold: first, it has served as the foundation for a formalization in Lean 4 of these results. This formalization has been completed largely automatically, making essential use of current frontier large language models. Second, it will serve as a resource to readers of the main paper who are interested in further technical details of the proofs. The main result concerns norm-variation estimates for multiple ergodic averages associated with $n\ge 2$ commuting measure preserving transformations, providing a quantitative strengthening of Tao's norm-convergence theorem and answering an open question of Avigad and Rute. At the core of the analysis lies an explicit real-variable estimate for twisted multilinear averages that is closely related to certain singular Brascamp--Lieb inequalities.

math.DS↗

arXiv2025

The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale

We report on the Equational Theories Project (ETP), an online collaborative pilot project to explore new ways to collaborate in mathematics with machine assistance. The project successfully determined all 22 028 942 edges of the implication graph between the 4694 simplest equational laws on magmas, by a combination of human-generated and automated proofs, all validated by the formal proof assistant language Lean. As a result of this project, several new constructions of magmas satisfying specific laws were discovered, and several auxiliary questions were also addressed, such as the effect of restricting attention to finite magmas.

math.RA↗

arXiv2025

Carleson operators on doubling metric measure spaces

Doubling metric measure spaces provide a natural framework for singular integral operators. In contrast, the study of maximally modulated singular integral operators, the so-called Carleson operators, has largely been limited to Euclidean space with modulation functions such as polynomials defined by algebraic means. We present a general axiomatic approach to modulation functions on doubling metric measure spaces and prove $L^p$ bounds for the corresponding Carleson operators in Theorem 1.1 and Theorem 1.2. This generalizes classical and modern results on Carleson operators. In addition to the proofs presented here, our main results have been computer verified using the language Lean and the library mathlib, as documented in the sibling communication arXiv:2405.06423.

math.CA↗

arXiv2024

A blueprint for the formalization of Carleson's theorem on convergence of Fourier series

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.

math.CA↗

arXiv2022

Designing a general library for convolutions

We will discuss our experiences and design decisions obtained from building a formal library for the convolution of two functions. Convolution is a fundamental concept with applications throughout mathematics. We will focus on the design decisions we made to make the convolution general and easy to use, and the incorporation of this development in Lean's mathematical library mathlib.

cs.LO↗

arXiv2022

Formalising the $h$-principle and sphere eversion

In differential topology and geometry, the h-principle is a property enjoyed by certain construction problems. Roughly speaking, it states that the only obstructions to the existence of a solution come from algebraic topology. We describe a formalisation in Lean of the local h-principle for first-order, open, ample partial differential relations. This is a significant result in differential topology, originally proven by Gromov in 1973 as part of his sweeping effort which greatly generalised many previous flexibility results in topology and geometry. In particular it reproves Smale's celebrated sphere eversion theorem, a visually striking and counter-intuitive construction. Our formalisation uses Theillière's implementation of convex integration from 2018. This paper is the first part of the sphere eversion project, aiming to formalise the global version of the h-principle for open and ample first order differential relations, for maps between smooth manifolds. Our current local version for vector spaces is the main ingredient of this proof, and is sufficient to prove the titular corollary of the project. From a broader perspective, the goal of this project is to show that one can formalise advanced mathematics with a strongly geometric flavour and not only algebraically-flavoured

cs.LO↗

arXiv2021

Progress on a perimeter surveillance problem

We consider a perimeter surveillance problem introduced by Kingston, Beard, and Holt in 2008 and studied by Davis, Humphrey, and Kingston in 2019. In this problem, $n$ drones surveil a finite interval, moving at uniform speed and exchanging information only when they meet another drone. Kingston et al. described a particular online algorithm for coordinating their behavior and asked for an upper bound on how long it can take before the drones are fully synchronized. They divided the algorithm's behavior into two phases, and presented upper bounds on the length of each phase based on conjectured worst-case configurations. Davis et al. presented counterexamples to the conjecture for phase 1. We present sharp upper bounds on phase 2 which show that in this case the conjectured worst case is correct. We also present new lower bounds on phase 1 and the total time to synchronization, and report partial progress towards obtaining an upper bound.

eess.SP↗

arXiv2021

Formalized Haar Measure

We describe the formalization of the existence and uniqueness of Haar measure in the Lean theorem prover. The Haar measure is an invariant regular measure on locally compact groups, and it has not been formalized in a proof assistant before. We will also discuss the measure theory library in Lean's mathematical library \textsf{mathlib}, and discuss the construction of product measures and the proof of Fubini's theorem for the Bochner integral.

cs.LO↗

arXiv2021

A Formal Proof of the Independence of the Continuum Hypothesis

We describe a formal proof of the independence of the continuum hypothesis ($\mathsf{CH}$) in the Lean theorem prover. We use Boolean-valued models to give forcing arguments for both directions, using Cohen forcing for the consistency of $\neg \mathsf{CH}$ and a $σ$-closed forcing for the consistency of $\mathsf{CH}$.

math.LO↗

arXiv2020

Maintaining a Library of Formal Mathematics

The Lean mathematical library mathlib is developed by a community of users with very different backgrounds and levels of experience. To lower the barrier of entry for contributors and to lessen the burden of reviewing contributions, we have developed a number of tools for the library which check proof developments for subtle mistakes in the code and generate documentation suited for our varied audience.

cs.PL↗

arXiv2019

A formalization of forcing and the unprovability of the continuum hypothesis

We describe a formalization of forcing using Boolean-valued models in the Lean 3 theorem prover, including the fundamental theorem of forcing and a deep embedding of first-order logic with a Boolean-valued soundness theorem. As an application of our framework, we specialize our construction to the Boolean algebra of regular opens of the Cantor space $2^{ω_2 \times ω}$ and formally verify the failure of the continuum hypothesis in the resulting model.

cs.LO↗

arXiv2018

On the Formalization of Higher Inductive Types and Synthetic Homotopy Theory

The goal of this dissertation is to present synthetic homotopy theory in the setting of homotopy type theory. We will present various results in this framework, most notably the construction of the Atiyah-Hirzebruch and Serre spectral sequences for cohomology, which have been fully formalized in the Lean proof assistant.

math.AT↗

arXiv2018

Higher Groups in Homotopy Type Theory

We present a development of the theory of higher groups, including infinity groups and connective spectra, in homotopy type theory. An infinity group is simply the loops in a pointed, connected type, where the group structure comes from the structure inherent in the identity types of Martin-Löf type theory. We investigate ordinary groups from this viewpoint, as well as higher dimensional groups and groups that can be delooped more than once. A major result is the stabilization theorem, which states that if an $n$-type can be delooped $n+2$ times, then it is an infinite loop type. Most of the results have been formalized in the Lean proof assistant.

cs.LO↗

arXiv2017

Homotopy Type Theory in Lean

We discuss the homotopy type theory library in the Lean proof assistant. The library is especially geared toward synthetic homotopy theory. Of particular interest is the use of just a few primitive notions of higher inductive types, namely quotients and truncations, and the use of cubical methods.

cs.LO↗

arXiv2015

Constructing the Propositional Truncation using Non-recursive HITs

In homotopy type theory, we construct the propositional truncation as a colimit, using only non-recursive higher inductive types (HITs). This is a first step towards reducing recursive HITs to non-recursive HITs. This construction gives a characterization of functions from the propositional truncation to an arbitrary type, extending the universal property of the propositional truncation. We have fully formalized all the results in a new proof assistant, Lean.

math.LO↗

arXiv2015

Propositional Calculus in Coq

I formalize important theorems about classical propositional logic in the proof assistant Coq. The main theorems I prove are (1) the soundness and completeness of natural deduction calculus, (2) the equivalence between natural deduction calculus, Hilbert systems and sequent calculus and (3) cut elimination for sequent calculus.

math.LO↗