9 papers
AdCoEvo: A Co-Evolving Multi-Agent Advertising Delivery System
Tianzhu Hu, Hang Yu, Zeyuan Zhao +9
Digital advertising is an important means for platforms to reach potential users and drive business growth. Advertising delivery is the core link between marketing objectives and a…
Formalizing Carleson's Theorem in Lean
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +11
We present the formalization of Carleson's theorem in the proof assistant Lean. This paper describes the mathematical content, organization of the project, the blueprint, and the m…
On Some Problems from the Kourovka Notebook
Wouter van Doorn, Elias Judin, Pietro Monticone +1
The Kourovka Notebook is a long-running collection of open problems in group theory. In this paper we present solutions to eight of its problems. We construct a group with exactly…
Gaps in Multiplicative Sidon Sets
Wouter van Doorn, Pietro Monticone, Quanyu Tang
For a positive integer , let denote the infimum of all real numbers such that there exists a multiplicative Sidon set that intersects ever…
Global Product Intersection Sets in Semigroups
Wouter van Doorn, Pietro Monticone, Quanyu Tang
For a family of subsets of a semigroup, the product intersection set records those exponents for which the -fold product set of the intersect…
LeanArchitect: Automating Blueprint Generation for Humans and AI
Thomas Zhu, Pietro Monticone, Jeremy Avigad +1
Large-scale formalization projects in Lean rely on blueprints: structured dependency graphs linking informal mathematical exposition to formal declarations. While blueprints are ce…
A Blueprint for the Formalization of Seymour's Matroid Decomposition Theorem
Ivan Sergeev, Martin Dvorak, Cameron Rampell +2
This document is a blueprint for the formalization in Lean of the structural theory of regular matroids underlying Seymour's decomposition theorem. We present a modular account of…
The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale
Matthew Bolan, Joachim Breitner, Jose Brox +31
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 suc…
A blueprint for the formalization of Carleson's theorem on convergence of Fourier series
Lars Becker, María Inés de Frutos-Fernández, Leo Diedering +14
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 fu…