close

You are currently browsing the monthly archive for January 2026.

Thomas Bloom’s Erdös problem site has become a real hotbed of activity in recent months, particularly as some of the easiest of the outstanding open problems have turned out to be amenable to various AI-assisted approaches; there is now a lively community in which human contributions, AI contributions, and hybrid contributions are presented, discussed, and in some cases approved as updates to the site.

One of the lessons I draw from this is that once a well curated database of precise mathematical problems is maintained, it becomes possible for other parties to build upon it in many ways (including both AI-based and human-based approaches), to systematically make progress on some fraction of the problems.

This makes me wonder what other mathematical databases could be created to stimulate similar activity. One candidate that came to mind are “optimization constants” – constants {C} that arise from some mathematical optimization problem of interest, for instance finding the best constant {C} for which a certain functional inequality is satisfied.

I am therefore proposing to create a crowdsourced repository for such constants, to record the best upper and lower bounds known for any given such constant, in order to help encourage efforts (whether they be by professional mathematicians, amateur mathematicians, or research groups at a tech company) to try to improve upon the state of the art.

There are of course thousands of such constants one could consider, but just to set the discussion going, I set up a very minimal, proof of concept Github repository holding over 20 constants including:

  1. {C_{1a}}, the constant in a certain autocorrelation quantity relating to Sidon sets. (This constant seems to have a surprisingly nasty optimizer; see this tweet thread of Damek Davis.)
  2. {C_{1b}}, the constant in Erdös’ minimum overlap problem.

Here, I am taking inspiration from the Erdös problem web site and arbitrarily assigning a number to each constant, for ease of reference.

Even in this minimal state I think the repository is ready to start accepting more contributions, in the form of pull requests that add new constants, or improve the known bounds on existing constants. (I am particularly interested in constants that have an extensive literature of incremental improvements in the lower and upper bounds, and which look at least somewhat amenable to computational or AI-assisted approaches.) But I would be interested to hear feedback on how to improve the repository in other ways.

Update: Paata Ivanisvili and Damek Davis have kindly agreed to help run and expand this repository.

A basic problem in sieve theory is to understand what happens when we start with the integers {{\bf Z}} (or some subinterval of the integers) and remove some congruence classes {a_i \pmod{q_i}} for various moduli {q_i}. Here we shall concern ourselves with the simple setting where we are sieving the entire integers rather than an interval, and are only removing a finite number of congruence classes {a_1 \pmod{q_1}, \ldots, a_k \pmod{q_k}}. In this case, the set of integers that remain after the sieving is periodic with period {Q = \mathrm{lcm}(q_1,\dots,q_k)}, so one work without loss of generality in the cyclic group {{\bf Z}/Q{\bf Z}}. One can then ask: what is the density of the sieved set

\displaystyle  \{ n \in {\bf Z}/Q{\bf Z}: n \neq a_i \hbox{ mod } q_i \hbox{ for all } i=1,\ldots,k \}? \ \ \ \ \ (1)

If the {q_i} were all coprime, then it is easy to see from the Chinese remainder theorem that the density is given by the product

\displaystyle  \prod_{i=1}^k \left(1 - \frac{1}{q_i}\right).

However, when the {q_i} are not coprime, the situation is more complicated. One can use the inclusion-exclusion formula to get a complicated expression for the density, but it is not easy to work with. Sieve theory also supplies one with various useful upper and lower bounds (starting with the classical Bonferroni inequalities), but do not give exact formulae.

In this blog post I would like to note one simple fact, due to Rogers, that one can say about this problem:

Theorem 1 (Rogers’ theorem) For fixed {q_1,\dots,q_k}, the density of the sieved set is maximized when all the {a_i} vanish. Thus,

\displaystyle  |\{ n \in {\bf Z}/Q{\bf Z}: n \neq a_i \hbox{ mod } q_i \hbox{ for all } i=1,\ldots,k \}|

\displaystyle \leq |\{ n \in {\bf Z}/Q{\bf Z}: n \neq 0 \hbox{ mod } q_i \hbox{ for all } i=1,\ldots,k \}|.

Example 2 If one sieves out {1 \pmod{2}}, {1 \pmod{3}}, and {2 \pmod{6}}, then only {0 \pmod{6}} remains, giving a density of {1/6}. On the other hand, if one sieves out {0 \pmod{2}}, {0 \pmod{3}}, and {0 \pmod{6}}, then the remaining elements are {1} and {5 \pmod{6}}, giving the larger density of {2/6}.

This theorem is somewhat obscure: its only appearance in print is in pages 242-244 of this 1966 text of Halberstam and Roth, where the authors write in a footnote that the result is “unpublished; communicated to the authors by Professor Rogers”. I have only been able to find it cited in three places in the literature: in this 1996 paper of Lewis, in this 2007 paper of Filaseta, Ford, Konyagin, Pomerance, and Yu (where they credit Tenenbaum for bringing the reference to their attention), and is also briefly mentioned in this 2008 paper of Ford. As far as I can tell, the result is not available online, which could explain why it is rarely cited (and also not known to AI tools). This became relevant recently with regards to Erdös problem 281, posed by Erdös and Graham in 1980, which was solved recently by Neel Somani through an AI query by an elegant ergodic theory argument. However, shortly after this solution was located, it was discovered by KoishiChan that Rogers’ theorem reduced this problem immediately to a very old result of Davenport and Erdös from 1936. Apparently, Rogers’ theorem was so obscure that even Erdös was unaware of it when posing the problem!

Modern readers may see some similarities between Rogers’ theorem and various rearrangement or monotonicity inequalites, suggesting that the result may be proven by some sort of “symmetrization” or “compression” method. This is indeed the case, and is basically Rogers’ original proof. We can modernize a bit as follows. Firstly, we can abstract {{\bf Z}/Q{\bf Z}} into a finite cyclic abelian group {G}, with residue classes now becoming cosets of various subgroups of {G}. We can take complements and restate Rogers’ theorem as follows:

Theorem 3 (Rogers’ theorem, again) Let {a_1+H_1, \dots, a_k+H_k} be cosets of a finite cyclic abelian group {G}. Then

\displaystyle  |\bigcup_{j=1}^k a_j + H_j| \geq |\bigcup_{j=1}^k H_j|.

Example 4 Take {G = {\bf Z}/6{\bf Z}}, {H_1 = 2{\bf Z}/6{\bf Z}}, {H_2 = 3{\bf Z}/6{\bf Z}}, and {H_3 = 6{\bf Z}/6{\bf Z}}. Then the cosets {1 + H_1}, {1 + H_2}, and {2 + H_3} cover the residues {\{1,2,3,4,5\}}, with a cardinality of {5}; but the subgroups {H_1,H_2,H_3} cover the residues {\{0,2,3,4\}}, having the smaller cardinality of {4}.

Intuitively: “sliding” the cosets {a_i+H_i} together reduces the total amount of space that these cosets occupy. As pointed out in comments, the requirement of cyclicity is crucial; four lines in a finite affine plane already suffice to be a counterexample otherwise.

By factoring the cyclic group into p-groups, Rogers’ theorem is an immediate consequence of two observations:

Theorem 5 (Rogers’ theorem for cyclic groups of prime order) Rogers’ theorem holds when {G = {\bf Z}/p^n {\bf Z}} for some prime power {p^n}.

Theorem 6 (Rogers’ theorem preserved under products) If Rogers’ theorem holds for two finite abelian groups {G_1, G_2} of coprime orders, then it also holds for the product {G_1 \times G_2}.

The case of cyclic groups of prime order is trivial, because the subgroups of {G} are totally ordered. In this case {\bigcup_{j=1}^k H_j} is simply the largest of the {H_j}, which has the same size as {a_j + H_j} and thus has lesser or equal cardinality to {\bigcup_{j=1}^k a_j + H_j}.

The preservation of Rogers’ theorem under products is also routine to verify. By the coprime orders of {G_1,G_2} and standard group theoretic arguments (e.g., Goursat’s lemma, the Schur–Zassenhaus theorem, or the classification of finite abelian groups), one can see that any subgroup {H_j} of {G_1 \times G_2} splits as a direct product {H_j = H_{j,1} \times H_{j,2}} of subgroups of {G_1,G_2} respectively, so the cosets {a_j + H_j} also split as

\displaystyle  a_j + H_j = (a_{j,1} + H_{j,1}) \times (a_{j,2} + H_{j,2}).

Applying Rogers’ theorem for {G_2} to each “vertical slice” of {G_1 \times G_2} and summing, we see that

\displaystyle  |\bigcup_{j=1}^k (a_{j,1} + H_{j,1}) \times (a_{j,2} + H_{j,2})| \geq |\bigcup_{j=1}^k (a_{j,1} + H_{j,1}) \times H_{j,2}|

and then applying Rogers’ theorem for {G_1} to each “horizontal slice” of {G_1 \times G_2} and summing, we obtain

\displaystyle  |\bigcup_{j=1}^k (a_{j,1} + H_{j,1}) \times H_{j,2}| \geq |\bigcup_{j=1}^k H_{j,1} \times H_{j,2}|.

Combining the two inequalities, we obtain the claim.

Like many other areas of modern analysis, analytic number theory often relies on the convenient device of asymptotic notation to express its results. It is common to use notation such as {X = O(Y)} or {X \ll Y}, for instance, to indicate a bound of the form {|X| \leq C Y} for some unspecified constant {C}. Such implied constants {C} vary from line to line, and in most papers, one does not bother to compute them explicitly. This makes the papers easier both to write and to read (for instance, one can use asymptotic notation to conceal a large number of lower order terms from view), and also means that minor numerical errors (for instance, forgetting a factor of two in an inequality) typically has no major impact on the final results. However, the price one pays for this is that many results in analytic number theory are only true in asymptotic sense; a typical example is Vinogradov’s theorem that every sufficiently large odd integer can be expressed as the sum of three primes. In the first few proofs of this theorem, the threshold for “sufficiently large” was not made explicit.

There is however a small portion of the analytic number theory devoted to explicit analytic number theory estimates, in which all constants are made completely explicit (and many lower order terms are retained). For instance, whereas the prime number theorem asserts that the prime counting function {\pi(x)} is asymptotic to the logarithmic integral {\mathrm{Li}(x) = \int_2^x \frac{dt}{\log t}}, in this recent paper of Fiori, Kadiri, and Swidinsky the explicit estimate

\displaystyle  |\pi(x) - \mathrm{Li}(x)| \leq 9.2211 x \sqrt{\log x} \exp(- 0.8476 \sqrt{\log x} )

is proven for all {x \geq 2}.

Such explicit results follow broadly similar strategies of proof to their non-explicit counterparts, but require a significant amount of careful book-keeping and numerical optimization; furthermore, any given explicit analytic number theory paper is likely to rely on the numerical results obtained in previous explicit analytic number theory papers. While the authors make their best efforts to avoid errors and build in some redundancy into their work, there have unfortunately been a few cases in which an explicit result stated in the published literature contained numerical errors that placed the numerical constants in several downstream applications of these papers into doubt.

Because of this propensity for error, updating any given explicit analytic number theory result to take into account computational improvements in other explicit results (such as zero-free regions for the Riemann zeta function) is not done lightly; such updates occur on the timescale of decades, and only by a small number of specialists in such careful computations. This leads to authors needing such explicit results to often be forced to rely on papers that are a decade or more out of date, with constants that they know in principle can be improved by inserting more recent explicit inputs, but do not have the domain expertise to confidently update all the numerical coefficients.

To me, this situation sounds like an appropriate application of modern AI and formalization tools – not to replace the most enjoyable aspects of human mathematical research, but rather to allow extremely tedious and time-consuming, but still necessary, mathematical tasks to be offloaded to semi-automated or fully automated tools.

Because of this, I (acting in my capacity as Director of Special Projects at IPAM) have just launched the integrated explicit analytic number theory network, a project partially hosted within the existing “Prime Number Theorem And More” (PNT+) formalization project. This project will consist of two components. The first is a crowdsourced formalization project to formalize a number of inter-related explicit analytic number theory results in Lean, such as the explicit prime number theorem of Fiori, Kadiri, and Swidinsky mentioned above; already some smaller results have been largely formalized, and we are making good progress (especially with the aid of modern AI-powered autoformalization tools) on several of the larger papers. The second, which will be run at IPAM with the financial and technical support of Math Inc., will be to extract from this network of formalized results an interactive “spreadsheet” of a large number of types of such estimates, with the ability to add or remove estimates from the network and have the numerical impact of these changes automatically propagate to other estimates in the network, similar to how changing one cell in a spreadsheet will automatically update other cells that depend on it. For instance, one could increase or decrease the numerical threshold to which the Riemann hypothesis is verified, and see the impact of this change on the explicit error terms in the prime number theorem; or one could “roll back” all the literature to a given date, and see what the best estimates on various analytic number theory expressions could still be derived from the literature available at that date. Initially, this spreadsheet will be drawn from direct adaptations of the various arguments from papers formalized within the network, but in a more ambitious second stage of the project we plan to use AI tools to modify these arguments to find more efficient relationships between the various numerical parameters than were provided in the source literature.

These more ambitious outcomes will likely take several months before a working proof of concept can be demonstrated; but in the near term I will be grateful for any contributions to the formalization side of the project, which is being coordinated on the PNT+ Zulip channel and on the github repository. We are using a github issues based system to coordinate the project, similar to how it was done for the Equational Theories Project. Any volunteer can select one of the outstanding formalization tasks on the Github issues page and “claim” it as a task to work on, eventually submitting a pull request (PR) to the repository when proposing a solution (or to “disclaim” the task if for whatever reason you are unable to complete it). As with other large formalization projects, an informal “blueprint” is currently under construction that breaks up the proofs of the main results of several explicit analytic number theory papers into bite-sized lemmas and sublemmas, most of which can be formalized independently without requiring broader knowledge of the arguments from the paper that the lemma was taken from. (A graphical display of the current formalization status of this blueprint can be found here. At the current time of writing, many portions of the blueprint are disconnected from each other, but as the formalization progresses, more linkages should be created.)

One minor innovation implemented in this project is to label each task by a “size” (ranging from XS (extra small) to XL (extra large)) that is a subjective assessment of the task difficulty, with the tasks near the XS side of the spectrum particularly suitable for beginners to Lean.

We are permitting AI use in completing the proof formalization tasks, though we require the AI use to be disclosed, and that the code is edited by humans to remove excessive bloat. (We expect some of the AI-generated code to be rather inelegant; but no proof of these explicit analytic number theory estimates, whether human-generated or AI-generated, is likely to be all that pretty or worth reading for its own sake, so the downsides of using AI-generated proofs here are lower than in other use cases.) We of course require all submissions to typecheck correctly in Lean through Github’s Continuous Integration (CI) system, so that any incorrect AI-generated code will be rejected. We are also cautiously experimenting with ways in which AI can also automatically or semi-automatically generate the formalized statements of lemmas and theorems, though here one has to be significantly more alert to the dangers of misformalizing an informally stated result, as this type of error cannot be automatically detected by a proof assistant.

We also welcome suggestions for additional papers or results in explicit analytic number theory to add to the network, and will have some blueprinting tasks in addition to the formalization tasks to convert such papers into a blueprinted sequence of small lemmas suitable for individual formalization.

Update: a personal log documenting the project may be found here.

Asgar Jamneshan, Or Shalom and I have uploaded to the arXiv our paper “ Polynomial towers and inverse Gowers theory for bounded-exponent groups“. This continues our investigation into the ergodic-theory approach to the inverse theory of Gowers norms over finite abelian groups {G}. In this regard, our main result establishes a satisfactory (qualitative) inverse theorem for groups {G} of bounded exponent:

Theorem 1 Let {G} be a finite abelian group of some exponent {m}, and let {f: G \rightarrow {\bf C}} be {1}-bounded with {\|f\|_{U^{k+1}(G)} > \delta}. Then there exists a polynomial {P: G \rightarrow {\bf R}/{\bf Z}} of degree at most {k} such that

\displaystyle  |\mathop{\bf E}_{x \in G} f(x) e(-P(x))| \gg_{k,m,\delta} 1.

This type of result was previously known in the case of vector spaces over finite fields (by work of myself and Ziegler), groups of squarefree order (by work of Candela, González-Sánchez, and Szegedy), and in the {k \leq 2} case (by work of Jamneshan and myself). The case {G = ({\bf Z}/4{\bf Z})^n}, for instance, is treated by this theorem but not covered by previous results. In the aforementioned paper of Candela et al., a result similar to the above theorem was also established, except that the polynomial {P} was defined in an extension of {G} rather than in {G} itself (or equivalently, {f} correlated with a projection of a phase polynomial, rather than directly with a phase polynomial on {G}). This result is consistent with a conjecture of Jamneshan and myself regarding what the “right” inverse theorem should be in any finite abelian group {G} (not necessarily of bounded exponent).

In contrast to previous work, we do not need to treat the “high characteristic” and “low characteristic” cases separately; in fact, many of the delicate algebraic questions about polynomials in low characteristic do not need to be directly addressed in our approach, although this is at the cost of making the inductive arguments rather intricate and opaque.

As mentioned above, our approach is ergodic-theoretic, deriving the above combinatorial inverse theorem from an ergodic structure theorem of Host–Kra type. The most natural ergodic structure theorem one could establish here, which would imply the above theorem, would be the statement that if {\Gamma} is a countable abelian group of bounded exponent, and {X} is an ergodic {\Gamma}-system of order at most {k} in the Host–Kra sense, then {X} would be an Abramov system – generated by polynomials of degree at most {k}. This statement was conjectured many years ago by Bergelson, Ziegler, and myself, and is true in many “high characteristic” cases, but unfortunately fails in low characteristic, as recently shown by Jamneshan, Shalom, and myself. However, we are able to recover a weaker version of this statement here, namely that {X} admits an extension which is an Abramov system. (This result was previously established by Candela et al. in the model case when {\Gamma} is a vector space over a finite field.) By itself, this weaker result would only recover a correlation with a projected phase polynomial, as in the work of Candela et al.; but the extension we construct arises as a tower of abelian extensions, and in the bounded exponent case there is an algebraic argument (hinging on a certain short exact sequence of abelian groups splitting) that allows one to map the functions in this tower back to the original combinatorial group {G} rather than an extension thereof, thus recovering the full strength of the above theorem.

It remains to prove the ergodic structure theorem. The standard approach would be to describe the system {X} as a Host–Kra tower

\displaystyle  Z^{\leq 0}(X) \leq Z^{\leq 1}(X) \leq \dots \leq Z^{\leq k}(X) = X,

where each extension {Z^{\leq j+1}(X)} of {Z^{\leq j}(X)} is a compact abelian group extension by a cocycle of “type” {j}, and them attempt to show that each such cocycle is cohomologous to a polynomial cocycle. However, this appears to be impossible in general, particularly in low characteristic, as certain key short exact sequences fail to split in the required ways. To get around this, we have to work with a different tower, extending various levels of this tower as needed to obtain additional good algebraic properties of each level that enables one to split the required short exact sequences. The precise properties needed are rather technical, but the main ones can be described informally as follows:

  • We need the cocycles to obey an “exactness” property, in that there is a sharp correspondence between the type of the cocycle (or any of its components) and its degree as a polynomial cocycle. (By general nonsense, any polynomial cocycle of degree {\leq d-1} is automatically of type {\leq d}; exactness, roughly speaking, asserts the converse.) Informally, the cocycles should be “as polynomial as possible”.
  • The systems in the tower need to have “large spectrum” in that the set of eigenvalues of the system form a countable dense subgroup of the Pontryagin dual of the acting group {\Gamma} (in fact we demand that a specific countable dense subgroup {\tilde \Gamma} is represented).
  • The systems need to be “pure” in the sense that the sampling map {\iota_{x_0} P(\gamma) := P(T^\gamma x_0)} that maps polynomials on the system to polynomials on the group {\Gamma} is injective for a.e. {x_0}, with the image being a pure subgroup. Informally, this means that the problem of taking roots of a polynomial in the system is equivalent to the problem of taking roots of the corresponding polynomial on the group {\Gamma}. In low characteristic, the root-taking problem becomes quite complicated, and we do not give a good solution to this problem either in the ergodic theory setting or the combinatorial one; however, purity at least lets one show that the two problems are (morally) equivalent to each other, which turns out to be what is actually needed to make the arguments work. There is also a technical “relative purity” condition we need to impose at each level of the extension to ensure that this purity property propagates up the tower, but I will not describe it in detail here.

It is then possible to recursively construct a tower of extensions that eventually reaches an extension of {X}, for which the above useful properties of exactness, large spectrum, and purity are obeyed, and that the system remains Abramov at each level of the tower. This requires a lengthy process of “straightening” the cocycle by differentiating it, obtaining various “Conze–Lesigne” type equations for the derivatives, and then “integrating” those equations to place the original cocycle in a good form. At multiple stages in this process it becomes necessary to have various short exact sequences of (topological) abelian groups split, which necessitates the various good properties mentioned above. To close the induction one then has to verify that these properties can be maintained as one ascends the tower, which is a non-trivial task in itself.

Archives