7 papers
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…