Given a threshold {y>1}, a {y}-smooth number (or {y}-friable number) is a natural number {n} whose prime factors are all at most {y}. We use {\Psi(x,y)} to denote the number of {y}-smooth numbers up to {x}. In studying the asymptotic behavior of {\Psi(x,y)}, it is customary to write {y} as {x^{1/u}} (or {x} as {y^u}) for some {u>0}. For small values of {u}, the behavior is straightforward: for instance if {0 < u < 1}, then all numbers up to {x} are automatically {y}-smooth, so

\displaystyle \Psi(x,y) \sim x

in this case. If {1 < u < 2}, the only numbers up to {x} that are not {y}-smooth are the multiples of primes {p} between {y} and {x}, so

\displaystyle \Psi(x,y) \sim x - \sum_{y < p \leq x} (\frac{x}{p} + O(1))

\displaystyle \sim x - x (\log\log x - \log\log y)

\displaystyle \sim x (1 - \log u)

where we have employed Mertens’ second theorem. For {2 < u < 3}, there is an additional correction coming from multiples of two primes between {y} and {x}; a straightforward inclusion-exclusion argument (which we omit here) eventually gives

\displaystyle \Psi(x,y) \sim x (1 - \log u + \int_2^u \frac{\log(t-1)}{t} dt)

in this case.

More generally, for any fixed {u>0}, de Bruijn showed that

\displaystyle \Psi(x, y) \sim \rho(u) x

where {\rho(u)} is the Dickman function. This function is a piecewise smooth, decreasing function of {u}, defined by the delay differential equation

\displaystyle u \rho'(u) + \rho(u-1) = 0

with initial condition {\rho(u) = 1} for {0 \leq u \leq 1}.

The asymptotic behavior of {\rho(u)} as {u \rightarrow \infty} is rather complicated. Very roughly speaking, it has inverse factorial behavior; there is a general upper bound {\rho(u) \leq 1/\Gamma(u+1)}, and a crude asymptotic

\displaystyle \rho(u) = u^{-u+o(u)} = \exp( - u \log u + o(u \log u)).

With a more careful analysis one can refine this to

\displaystyle \rho(u) = \exp( - u \log u - u \log\log u + u + o(u)); \ \ \ \ \ (1)

 and with a very careful application of the Laplace inversion formula one can in fact show that

\displaystyle \rho(u) \sim \sqrt{\frac{\xi'(u)}{2\pi}} \exp( \gamma - u \xi(u) + \int_0^{\xi(u)} \frac{e^s - 1}{s} ds) \ \ \ \ \ (2)

 where {\gamma} is the Euler-Mascheroni constant and {\xi(u)} is defined implicitly by the equation

\displaystyle e^{\xi(u)} - 1 = u \xi(u). \ \ \ \ \ (3)

 One cannot write {\xi(u)} in closed form using elementary functions, but one can express it in terms of the Lambert {W} function as {\xi(u) = -W(-\frac{1}{u} e^{-1/u}) - 1/u}. This is not a particularly enlightening expression, though. A more productive approach is to work with approximations. It is not hard to get the initial approximation {\xi(u) \approx \log u} for large {u}, which can then be re-inserted back into (3) to obtain the more accurate approximation

\displaystyle \xi(u) = \log u + \log\log u + O(1)

and inserted once again to obtain the refinement

\displaystyle \xi(u) = \log u + \log\log u + O(\frac{\log\log u}{\log u}).

We can now see that (2) is consistent with previous asymptotics such as (1), after comparing the integral {\int_0^{\xi(u)} \frac{e^s - 1}{s} ds} to

\displaystyle \int_0^{\xi(u)} \frac{e^s - 1}{\xi(u)} ds = u - 1.

For more details of these results, one can see for instance this survey by Granville.

This asymptotic (2) is quite complicated, and so one does not expect there to be any simple argument that could recover it without extensive computation. However, it turns out that one can use a “maximum entropy” analysis to get a reasonably good heuristic approximation to (2), that at least reveals the role of the mysterious function {\xi(u)}. The purpose of this blog post is to give this heuristic.

Viewing {x = y^u}, the task is to try to count the number of {y}-smooth numbers of magnitude {y^u}. We will propose a probabilistic model to generate {y}-smooth numbers as follows: for each prime {p \leq y}, select the prime {p} with an independent probability {c_p/p} for some coefficient {c_p}, and then multiply all the selected primes together. This will clearly generate a random {y}-smooth number {n}, and by the law of large numbers, the (log-)magnitude of this number should be approximately

\displaystyle \log n \approx \sum_{p \leq y} \frac{c_p}{p} \log p, \ \ \ \ \ (4)

(where we will be vague about what “{\approx}” means here), so to obtain a number of magnitude about {y^u}, we should impose the constraint

\displaystyle \sum_{p \leq y} \frac{c_p}{p} \log p = u \log y. \ \ \ \ \ (5)

The indicator {1_{p|n}} of the event that {p} divides this number is a Bernoulli random variable with mean {c_p/p}, so the Shannon entropy of this random variable is

\displaystyle \mathbf{H}(1_{p|n}) = - \frac{c_p}{p} \log(\frac{c_p}{p}) - (1 - \frac{c_p}{p}) \log(1 - \frac{c_p}{p}).

If {c_p} is not too large, then Taylor expansion gives the approximation

\displaystyle \mathbf{H}(1_{p|n}) \approx \frac{c_p}{p} \log p - \frac{c_p}{p} \log c_p + \frac{c_p}{p}.

Because of independence, the total entropy of this random variable {n} is

\displaystyle \mathbf{H}(n) = \sum_{p \leq y} \mathbf{H}(1_{p|n});

inserting the previous approximation as well as (5), we obtain the heuristic approximation

\displaystyle \mathbf{H}(n) \approx u \log y - \sum_{p \leq y} \frac{c_p}{p} (\log c_p - 1).

The asymptotic equipartition property of entropy, relating entropy to microstates, then suggests that the set of numbers {n} that are typically generated by this random process should have cardinality approximately

\displaystyle \exp(\mathbf{H}(n)) \approx \exp\left(u \log y - \sum_{p \leq y} \frac{c_p}{p} (\log c_p - 1)\right)

\displaystyle = \exp\left(- \sum_{p \leq y} \frac{c_p \log c_p - c_p}{p}\right) x.

Using the principle of maximum entropy, one is now led to the approximation

\displaystyle \rho(u) \approx \exp\left(- \sum_{p \leq y} \frac{c_p \log c_p - c_p}{p}\right). \ \ \ \ \ (6)

 where the weights {c_p} are chosen to maximize the right-hand side subject to the constraint (5).

One could solve this constrained optimization problem directly using Lagrange multipliers, but we simplify things a bit by passing to a continuous limit. We take a continuous ansatz {c_p = f(\log p / \log y)}, where {f: [0,1] \rightarrow {\bf R}} is a smooth function. Using Mertens’ theorem, the constraint (5) then heuristically becomes

\displaystyle \int_0^1 f(t)\ dt = u \ \ \ \ \ (7)

and the expression (6) simplifies to

\displaystyle \rho(u) \approx \exp( - \int_0^1 \frac{f(t) \log f(t) - f(t)}{t}\ dt). \ \ \ \ \ (8)

 So the entropy maximization problem has now been reduced to the problem of minimizing the functional {\int_0^1 \frac{f(t) \log f(t) - f(t)}{t}\ dt} subject to the constraint (7). The astute reader may notice that the integral in (8) might diverge at {t=0}, but we shall ignore this technicality for the sake of the heuristic arguments.

This is a standard calculus of variations problem. The Euler-Lagrange equation for this problem can be easily worked out to be

\displaystyle \frac{\log f(t)}{t} = \lambda

for some Lagrange multiplier {\lambda}; in other words, the optimal {f} should have an exponential form {f(t)= e^{\lambda t}}. The constraint (7) then becomes

\displaystyle \frac{e^\lambda - 1}{\lambda} = u

and so the Lagrange multiplier {\lambda} is precisely the mysterious quantity {\xi(u)} appearing in (2)! The formula (8) can now be evaluated as

\displaystyle \rho(u) \approx \exp\left( - \int_0^1 \frac{e^{\xi(u) t} \xi(u) t - e^{\xi(u) t}}{t}\ dt \right)

\displaystyle \approx \exp\left( - e^{\xi(u)} + 1 + \int_0^1 \frac{e^{\xi(u) t} - 1}{t}\ dt + \int_0^1 \frac{1}{t}\ dt \right)

\displaystyle \approx \exp\left( - u \xi(u) + \int_0^{\xi(u)} \frac{e^s - 1}{s}\ ds + C\right)

where {C} is the divergent constant

\displaystyle C = \int_0^1 \frac{1}{t}\ dt.

This recovers a large fraction of (2)! It is not completely accurate for multiple reasons. One is that the hypothesis of joint independence on the events {p|n} is unrealistic when trying to confine {n} to a single scale {x}; this comes down ultimately to the subtle differences between the Poisson and Poisson-Dirichlet processes, as discussed in this previous blog post, and is also responsible for the otherwise mysterious {e^\gamma} factor in Mertens’ third theorem; it also morally explains the presence of the same {e^\gamma} factor in (2). A related issue is that the law of large numbers (4) is not exact, but admits gaussian fluctuations as per the central limit theorem; morally, this is the main cause of the {\sqrt{\frac{\xi'(u)}{2\pi}}} prefactor in (2).

Nevertheless, this demonstrates that the maximum entropy method can achieve a reasonably good heuristic understanding of smooth numbers. In fact we also gain some insight into the “anatomy of integers” of such numbers: the above analysis suggests that a typical {y}-smooth number {n} will be divisible by a given prime {p \sim y^t} with probability about {e^{\xi(u) t}/p}. Thus, for {t = 1 - O(1/\log u)}, the probability of being divisible by {p} is elevated by a factor of about {\asymp e^{\xi(u)} \asymp u \log u} over the baseline probability {1/p} of an arbitrary (non-smooth) number being divisible by {p}; so (by Mertens’ theorem) a typical {y}-smooth number is actually largely comprised of something like {\asymp u} prime factors all of size about {y^{1-O(1/\log u)}}, with the smaller primes contributing a lower order factor. This is in marked contrast with the anatomy of a typical (non-smooth) number {n}, which typically has {O(1)} prime factors in each hyperdyadic scale {[\exp\exp(k), \exp\exp(k+1)]} in {[1,n]}, as per Mertens’ theorem.

Thomas Bloom’s erdosproblems.com site hosts nearly a thousand questions that originated, or were communicated by, Paul Erdős, as well as the current status of these questions (about a third of which are currently solved). The site is now a couple years old, and has been steadily adding features, the most recent of which has been a discussion forum for each individual question. For instance, a discussion I had with Stijn Cambie and Vjeko Kovac on one of these problems recently led to it being solved (and even formalized in Lean!).

A significantly older site is the On-line Encyclopedia of Integer Sequences (OEIS), which records hundreds of thousands of integer sequences that have some mathematician has encountered at some point. It is a highly useful resource, enabling researchers to discover relevant literature for a given problem so long as they can calculate enough of some integer sequence that is “canonically” attached to that problem that they can search for it in the OEIS.

A large fraction of problems in the Erdos problem webpage involve (either explicitly or implicitly) some sort of integer sequence – typically the largest or smallest size {f(n)} of some {n}-dependent structure (such as a graph of {n} vertices, or a subset of {\{1,\dots,n\}}) that obeys a certain property. In some cases, the sequence is already in the OEIS, and is noted in the Erdos problem web page. But in a large number of cases, the sequence either has not yet been entered into the OEIS, or it does appear but has not yet been noted on the Erdos web page.

Thomas Bloom and I are therefore proposing a crowdsourced project to systematically compute the hundreds of sequences associated to the Erdos problems and cross-check them against the OEIS. We have created a github repository to coordinate this process; as a by-product, this repository will also be tracking other relevant statistics about the Erdos problem website, such as the current status of formalizing the statements of these problems in the Formal Conjectures Repository.

The main feature of our repository is a large table recording the current status of each Erdos problem. For instance, Erdos problem #3 is currently listed as open, and additionally has the status of linkage with the OEIS listed as “possible”. This means that there are one or more sequences attached to this problem which *might* already be in the OEIS, or would be suitable for submission to the OEIS. Specifically, if one reads the commentary for that problem, one finds mention of the functions {r_k(N)} for {k=3,4,\dots}, defined as the size of the largest subset of {\{1,\dots,N\}} without a {k}-term progression. It is likely that several of the sequences {r_3(N)}, {r_4(N)}, etc. are in the OEIS, but it is a matter of locating them, either by searching for key words, or by calculating the first few values of these sequences and then looking for a match. (EDIT: a contributor has noted that the first foursequences appear as A003002, A003003, A003004, and A003005 in the OEIS, and the table has been updated accordingly.)

We have set things up so that new contributions (such as the addition of an OEIS number to the table) can be made by a Github pull request, specifically to modify this YAML file. Alternatively, one can create a Github issue for such changes, or simply leave a comment either on the appropriate Erdos problem forum page, or here on this blog.

Many of the sequences do not require advanced mathematical training to compute, and so we hope that this will be a good “citizen mathematics” project that can bring in the broader math-adjacent community to contribute to research-level mathematics problems, by providing experimental data, and potentially locating relevant references or connections that would otherwise be overlooked. This may also be a use case for AI assistance in mathematics through generating code to calculate the sequences in question, although of course one should always stay mindful of potential bugs or hallucinations in any AI-generated code, and find ways to independently verify the output. (But if the AI-generated sequence leads to a match with an existing sequence in the OEIS that is clearly relevant to the problem, then the task has been successfully accomplished, and no AI output needs to be directly incorporated into the database in such cases.)

This is an experimental project, and we may need to adjust the workflow as the project progresses, but we hope that it will be successful and lead to further progress on some fraction of these problems. The comment section of this blog can be used as a general discussion forum for the project, while the github issue page and the erdosproblems.com forum pages can be used for more specialized discussions of specific problems.

The Simons-Laufer Mathematical Sciences institute, or SLMath (formerly the Mathematical Sciences Research Institute, or MSRI) has recently restructured its program formats, and is now announcing three new research initiatives, whose applications open on Sep 1 2025:

  • AxIOM (Accelerating Innovation in Mathematics) is a new, month-long research program at SLMath, designed to accelerate innovation and introduce transformative ideas into the mathematical sciences. Programs begin in Spring 2027.
  • PROOF (Promoting Research Opportunities and Open Forums) is a two-week summer program designed to provide research opportunities for U.S.-based mathematicians, statisticians, and their collaborators in the U.S. and abroad, whose ongoing research may have been impacted by factors such as heavy teaching loads, professional isolation, limited access to funding, heavy administrative duties, personal obligations, or other constraints. Programs begin June-July 2026. The priority application deadline for PROOF 2026 is October 12, 2025.
  • Lasting Alliance Through Team Immersion and Collaborative Exploration (LATTICE) is a yearlong program which provides opportunities for U.S. mathematicians to conduct collaborative research on topics at the forefront of the mathematical and statistical sciences. Programs begin June-July 2026. LATTICE 2026 applications are open through February 1, 2026.

(Disclosure: I am vice-chair of the board of trustees at SLMath.)

First things first: due to an abrupt suspension of NSF funding to my home university of UCLA, the Institute of Pure and Applied Mathematics (which had been preliminarily approved for a five-year NSF grant to run the institute) is currently fundraising to ensure continuity of operations during the suspension, with a goal of raising $500,000. Donations can be made at this page. As incoming Director of Special Projects at IPAM, I am grateful for the support (both moral and financial) that we have already received in the last few days, but we are still short of our fundraising goal.

Back to math. Ayla Gafni and I have just uploaded to the arXiv the paper “Rough numbers between consecutive primes“. In this paper we resolve a question of Erdös concerning rough numbers between consecutive gaps, and with the assistance of modern sieve theory calculations, we in fact obtain quite precise asymptotics for the problem. (As a side note, this research was supported by my personal NSF grant which is also currently suspended; I am grateful to recent donations to my own research fund which have helped me complete this research.)

Define a prime gap to be an interval {(p_n, p_{n+1})} between consecutive primes. We say that a prime gap contains a rough number if there is an integer {m \in (p_n,p_{n+1})} whose least prime factor is at least the length {p_{n+1}-p_n} of the gap. For instance, the prime gap {(3,5)} contains the rough number {4}, but the prime gap {(7,11)} does not (all integers between {7} and {11} have a prime factor less than {4}). The first few {n} for which the {n^\mathrm{th}} prime gap contains a rough number are

\displaystyle 2, 3, 5, 7, 10, 13, 15, 17, 20, \dots.

Numerically, the proportion of {n} for which the {n^\mathrm{th}} prime gap does not contain a rough number decays slowly as {n} increases:

Erdös initially thought that all but finitely many prime gaps should contain a rough number, but changed his mind, as per the following quote:

…I am now sure that this is not true and I “almost” have a counterexample. Pillai and Szekeres observed that for every {t \leq 16}, a set of {t} consecutive integers always contains one which is relatively prime to the others. This is false for {t = 17}, the smallest counterexample being {2184, 2185, \dots, 2200}. Consider now the two arithmetic progressions {2183 + d \cdot 2 \cdot 3 \cdot 5 \cdot 7 \cdot 11 \cdot 13} and {2201 + d \cdot 2 \cdot 3 \cdot 5 \cdot 7 \cdot 11 \cdot 13}. There certainly will be infinitely many values of {d} for which the progressions simultaneously represent primes; this follows at once from hypothesis H of Schinzel, but cannot at present be proved. These primes are consecutive and give the required counterexample. I expect that this situation is rather exceptional and that the integers {k} for which there is no {m} satisfying {p_k < m < p_{k+1}} and {p(m) > p_{k+1} - p_k} have density {0}.

In fact Erdös’s observation can be made simpler: any pair of cousin primes {p_{n+1}=p_n+4} for {p_n > 3} (of which {(7,11)} is the first example) will produce a prime gap that does not contain any rough numbers.

The latter question of Erdös is listed as problem #682 on Thomas Bloom’s Erdös problems website. In this paper we answer Erdös’s question, and in fact give a rather precise bound for the number of counterexamples:

Theorem 1 (Erdos #682) For {X>2}, let {N(X)} be the number of prime gaps {(p_n, p_{n+1})} with {p_n \in [X,2X]} that do not contain a rough number. Then

\displaystyle N(X) \ll \frac{X}{\log^2 X}. \ \ \ \ \ (1)

 Assuming the Dickson–Hardy–Littlewood prime tuples conjecture, we can improve this to

\displaystyle N(X) \sim c \frac{X}{\log^2 X} \ \ \ \ \ (2)

 for some (explicitly describable) constant {c>0}.

In fact we believe that {c \approx 2.8}, although the formula we have to compute {c} converges very slowly. This is (weakly) supported by numerical evidence:

While many questions about prime gaps remain open, the theory of rough numbers is much better understood, thanks to modern sieve theoretic tools such as the fundamental lemma of sieve theory. The main idea is to frame the problem in terms of counting the number of rough numbers in short intervals {[x,x+H]}, where {x} ranges in some dyadic interval {[X,2X]} and {H} is a much smaller quantity, such as {H = \log^\alpha X} for some {0 < \alpha < 1}. Here, one has to tweak the definition of “rough” to mean “no prime factors less than {z}” for some intermediate {z} (e.g., {z = \exp(\log^\beta X)} for some {0 < \beta < \alpha} turns out to be a reasonable choice). These problems are very analogous to the extremely well studied problem of counting primes in short intervals, but one can make more progress without needing powerful conjectures such as the Hardy–Littlewood prime tuples conjecture. In particular, because of the fundamental lemma of sieve theory, one can compute the mean and variance (i.e., the first two moments) of such counts to high accuracy, using in particular some calculations on the mean values of singular series that go back at least to the work of Montgomery from 1970. This second moment analysis turns out to be enough (after optimizing all the parameters) to answer Erdös’s problem with a weaker bound

\displaystyle N(X) \ll \frac{X}{\log^{4/3-o(1)} X}.

To do better, we need to work with higher moments. The fundamental lemma also works in this setting; one now needs precise asymptotics for the mean value of singular series of {k}-tuples, but this was fortunately worked out (in more or less exactly the format we needed) by Montgomery and Soundararajan in 2004. Their focus was establishing a central limit theorem for the distribution of primes in short intervals (conditional on the prime tuples conjecture), but their analysis can be adapted to show (unconditionally) good concentration of measure results for rough numbers in short intervals. A direct application of their estimates improves the upper bound on {N(X)} to

\displaystyle N(X) \ll \frac{X}{\log^{2-o(1)} X}

and some more careful tweaking of parameters allows one to remove the {o(1)} error. This latter analysis reveals that in fact the dominant contribution to {N(X)} will come with prime gaps of bounded length, of which our understanding is still relatively poor (it was only in 2014 that Yitang Zhang famously showed that infinitely many such gaps exist). At this point we finally have to resort to (a Dickson-type form of) the prime tuples conjecture to get the asymptotic (2).

The Salem prize was established in 1968 and named in honor of Raphaël Salem (1898-1963), a mathematician famous notably for his deep study of the links between Fourier series and number theory and for pioneering applications of probabilistic methods to these fields. It was not awarded from 2019-2022, due to both the COVID pandemic and the death of Jean Bourgain who had been almost single-handedly administering the prize, but is now active again, being administered by Akshay Ventakesh and the IAS. I chair the scientific committee for this prize, whose other members are Guy David and Mikhail Sodin. Last year, the prize was awarded to Miguel Walsh and Yilin Wang.

Nominations for the 2025 Salem Prize are now open until September 15th. Nominations should include a CV of the nominee and a nomination letter explaining the significance of the nominee’s work. Supplementary documentation, such as supporting letters of recommendation or key publications, can additionally be provided, but are not required.

Nominees may be individuals from any country or institution. Preference will be given to nominees who have received their PhD in the last ten years, although this rule may be relaxed if there are mitigating personal circumstances, or if there have been few Salem prize winners in recent years. Self-nominations will not be considered, nor are past Prize winners or Scientific Committee members eligible.

The prize does not come with a direct monetary award, but winners will be invited to visit the IAS and to give a lecture associated with the award of the prize.

See also the previous year’s announcement of the Salem prize nomination period.

Boris Alexeev, Evan Conway, Matthieu Rosenfeld, Andrew Sutherland, Markus Uhr, Kevin Ventullo, and I have uploaded to the arXiv a second version of our paper “Decomposing a factorial into large factors“. This is a completely rewritten and expanded version of a previous paper of the same name. Thanks to many additional theoretical and numerical contributors from the other coauthors, we now have much more precise control on the main quantity {t(N)} studied in this paper, allowing us to settle all the previous conjectures about this quantity in the literature.

As discussed in the previous post, {t(N)} denotes the largest integer {t} such that the factorial {N!} can be expressed as a product of {N} factors, each of which is at least {t}. Computing {t(N)} is a special case of the bin covering problem, which is known to be NP-hard in general; and prior to our work, {t(N)} was only computed for {N \leq 599}; we have been able to compute {t(N)} for all {N \leq 10000}. In fact, we can get surprisingly sharp upper and lower bounds on {t(N)} for much larger {N}, with a precise asymptotic

\displaystyle \frac{t(N)}{N} = \frac{1}{e} - \frac{c_0}{\log N} - \frac{O(1)}{\log^{1+c} N}

for an explicit constant {c_0 = 0.30441901\dots}, which we conjecture to be improvable to

\displaystyle \frac{t(N)}{N} = \frac{1}{e} - \frac{c_0}{\log N} - \frac{c_1+o(1)}{\log^{2} N}

for an explicit constant {c_1 = 0.75554808\dots}: … For instance, we can demonstrate numerically that

\displaystyle 0 \leq t(9 \times 10^8) - 316560601 \leq 113.

As a consequence of this precision, we can verify several conjectures of Guy and Selfridge, namely

  • {t(N) \leq N/e} for all {N \neq 1,2,4}.
  • {t(N) \geq \lfloor 2N/7\rfloor} for all {N \neq 56}.
  • {t(N) \geq N/3} for all {N \geq 3 \times 10^5}. (In fact we show this is true for {N \geq 43632}, and that this threshold is best possible.)

Guy and Selfridge also claimed that one can establish {t(N) \geq N/4} for all large {N} purely by rearranging factors of {2} and {3} from the standard factorization {1 \times 2 \times \dots \times N} of {N!}, but surprisingly we found that this claim (barely) fails for all {N > 26244}:

The accuracy of our bounds comes from several techniques:

  • Greedy algorithms, in which one allocates the largest prime factors of {N!} first and then moves to smaller primes, provide quickly computable, though suboptimal, lower bounds on {t(N)} for small, medium, and moderately large values;
  • Linear programming and integer programming methods provides extremely accurate upper and lower bounds on {t(N)} for small and medium values of {N};
  • Rearrangement methods can be analyzed asymptotically via linear programming, and work well for large {N}; and
  • The modified approximate factorization strategy, discussed in the previous post is now sharpened by using {3}-smooth numbers (products of {2} and {3}) as the primary “liquidity pool” to reallocate factors of {N!}, as opposed to the previous approach of only using powers of {2}.

To me, the biggest surprise was just how stunningly accurate the linear programming methods were; the very large number of repeated prime factors here actually make this discrete problem behave rather like a continuous one.

Ayla Gafni and I have just uploaded to the arXiv the paper “On the number of exceptional intervals to the prime number theorem in short intervals“. This paper makes explicit some relationships between zero density theorems and prime number theorems in short intervals which were somewhat implicit in the literature at present.

Zero density theorems are estimates of the form

\displaystyle N(\sigma,T) \ll T^{A(\sigma)(1-\sigma)+o(1)}

for various {0 \leq \sigma < 1}, where {T} is a parameter going to infinity, {N(\sigma,T)} counts the number of zeroes of the Riemann zeta function of real part at least {\sigma} and imaginary part between {-T} and {T}, and {A(\sigma)} is an exponent which one would like to be as small as possible. The Riemann hypothesis would allow one to take {A(\sigma)=-\infty} for any {\sigma > 1/2}, but this is an unrealistic goal, and in practice one would be happy with some non-trivial upper bounds on {A(\sigma)}. A key target here is the density hypothesis that asserts that {A(\sigma) \leq 2} for all {\sigma} (this is in some sense sharp because the Riemann-von Mangoldt formula implies that {A(1/2)=2}); this hypothesis is currently known for {\sigma \leq 1/2} and {\sigma \geq 25/32}, but the known bounds are not strong enough to establish this hypothesis in the remaining region. However, there was a recent advance of Guth and Maynard, which among other things improved the upper bound {A_0} on {\sup_\sigma A(\sigma)} from {12/5=2.4} to {30/13=2.307\dots}, marking the first improvement in this bound in over four decades. Here is a plot of the best known upper bounds on {A(\sigma)}, either unconditionally, assuming the density hypothesis, or the stronger Lindelöf hypothesis:

One of the reasons we care about zero density theorems is that they allow one to localize the prime number theorem to short intervals. In particular, if we have the uniform bound {A(\sigma) \leq A_0} for all {\sigma}, then this leads to the prime number theorem

\displaystyle \sum_{x \leq n < x+x^\theta} \Lambda(n) \sim x^\theta holding for all {x} if {\theta > 1-\frac{1}{A_0}}, and for almost all {x} (possibly excluding a set of density zero) if {\theta > 1 - \frac{2}{A_0}}. For instance, the Guth-Maynard results give a prime number theorem in almost all short intervals for {\theta} as small as {2/15+\varepsilon}, and the density hypotheis would lower this just to {\varepsilon}.

However, one can ask about more information on this exceptional set, in particular to bound its “dimension” {\mu(\theta)}, which roughly speaking amounts to getting an upper bound of {X^{\mu(\theta)+o(1)}} on the size of the exceptional set in any large interval {[X,2X]}. Based on the above assertions, one expects {\mu(\theta)} to only be bounded by {1} for {\theta < 1-2/A}, be bounded by {-\infty} for {\theta > 1-1/A}, but have some intermediate bound for the remaining exponents.

This type of question had been studied in the past, most direclty by Bazzanella and Perelli, although there is earlier work by many authors om some related quantities (such as the second moment {\sum_{n \leq x} (p_{n+1}-p_n)^2} of prime gaps) by such authors as Selberg and Heath-Brown. In most of these works, the best available zero density estimates at that time were used to obtain specific bounds on quantities such as {\mu(\theta)}, but the numerology was usually tuned to those specific estimates, with the consequence being that when newer zero density estimates were discovered, one could not readily update these bounds to match. In this paper we abstract out the arguments from previous work (largely based on the explicit formula for the primes and the second moment method) to obtain an explicit relationship between {\mu(\theta)} and {A(\sigma)}, namely that

\displaystyle \mu(\theta) \leq \inf_{\varepsilon>0} \sup_{0 \leq \theta<1; A(\sigma) \geq \frac{1}{1-\theta}-\varepsilon} \mu_{2,\sigma}(\theta) where

\displaystyle \mu_{2,\theta}(\theta) = (1-\theta)(1-\sigma)A(\sigma)+2\sigma-1. Actually, by also utilizing fourth moment methods, we obtain a stronger bound

\displaystyle \mu(\theta) \leq \inf_{\varepsilon>0} \sup_{0 \leq \theta<1; A(\sigma) \geq \frac{1}{1-\theta}-\varepsilon} \min( \mu_{2,\sigma}(\theta), \mu_{4,\sigma}(\theta) ) where

\displaystyle \mu_{4,\theta}(\theta) = (1-\theta)(1-\sigma)A^*(\sigma)+4\sigma-3 and {A^*(\sigma)} is the exponent in “additive energy zero density theorems”

\displaystyle N^*(\sigma,T) \ll T^{A^*(\sigma)(1-\sigma)+o(1)} where {N^*(\sigma,T)} is similar to {N(\sigma,T)}, but bounds the “additive energy” of zeroes rather than just their cardinality. Such bounds have appeared in the literature since the work of Heath-Brown, and are for instance a key ingredient in the recent work of Guth and Maynard. Here are the current best known bounds:

These explicit relationships between exponents are perfectly suited for the recently launched Analytic Number Theory Exponent Database (ANTEDB) (discussed previously here), and have been uploaded to that site.

This formula is moderately complicated (basically an elaborate variant of a Legendre transform), but easy to calculate numerically with a computer program. Here is the resulting bound on {\mu(\theta)} unconditionally and under the density hypothesis (together with a previous bound of Bazzanella and Perelli for comparison, where the range had to be restricted due to a gap in the argument we discovered while trying to reproduce their results):

For comparison, here is the situation assuming strong conjectures such as the density hypothesis, Lindelof hypothesis, or Riemann hypothesis:

Almost 20 years ago, I wrote a textbook in real analysis called “Analysis I“. It was intended to complement the many good available analysis textbooks out there by focusing more on foundational issues, such as the construction of the natural numbers, integers, rational numbers, and reals, as well as providing enough set theory and logic to allow students to develop proofs at high levels of rigor.

While some proof assistants such as Coq or Agda were well established when the book was written, formal verification was not on my radar at the time. However, now that I have had some experience with this subject, I realize that the content of this book is in fact very compatible with such proof assistants; in particular, the ‘naive type theory’ that I was implicitly using to do things like construct the standard number systems, dovetails well with the dependent type theory of Lean (which, among other things, has excellent support for quotient types).

I have therefore decided to launch a Lean companion to “Analysis I”, which is a “translation” of many of the definitions, theorems, and exercises of the text into Lean. In particular, this gives an alternate way to perform the exercises in the book, by instead filling in the corresponding “sorries” in the Lean code. (I do not however plan on hosting “official” solutions to the exercises in this companion; instead, feel free to create forks of the repository in which these sorries are filled in.)

Currently, the following sections of the text have been translated into Lean:

The formalization has been deliberately designed to be separate from the standard Lean math library Mathlib at some places, but reliant on it at others. For instance, Mathlib already has a standard notion of the natural numbers {{\bf N}}. In the Lean formalization, I first develop “by hand” an alternate construction Chapter2.Nat of the natural numbers (or just Nat, if one is working in the Chapter2 namespace), setting up many of the basic results about these alternate natural numbers which parallel similar lemmas about {{\bf N}} that are already in Mathlib (but with many of these lemmas set as exercises to the reader, with the proofs currently replaced with “sorries”). Then, in an epilogue section, isomorphisms between these alternate natural numbers and the Mathlib natural numbers are established (or more precisely, set as exercises). From that point on, the Chapter 2 natural numbers are deprecated, and the Mathlib natural numbers are used instead. I intend to continue this general pattern throughout the book, so that as one advances into later chapters, one increasingly relies on Mathlib’s definitions and functions, rather than directly referring to any counterparts from earlier chapters. As such, this companion could also be used as an introduction to Lean and Mathlib as well as to real analysis (somewhat in the spirit of the “Natural number game“, which in fact has significant thematic overlap with Chapter 2 of my text).

The code in this repository compiles in Lean, but I have not tested whether all of the (numerous) “sorries” in the code can actually be filled (i.e., if all the exercises can actually be solved in Lean). I would be interested in having volunteers “playtest” the companion to see if this can actually be done (and if the helper lemmas or “API” provided in the Lean files are sufficient to fill in the sorries in a conceptually straightforward manner without having to rely on more esoteric Lean programming techniques). Any other feedback will of course also be welcome.

[UPDATE, May 31: moved the companion to a standalone repository.]

Rachel Greenfeld and I have just uploaded to the arXiv our paper Some variants of the periodic tiling conjecture. This paper explores variants of the periodic tiling phenomenon that, in some cases, a tile that can translationally tile a group, must also be able to translationally tile the group periodically. For instance, for a given discrete abelian group {G}, consider the following question:

Question 1 (Periodic tiling question) Let {F} be a finite subset of {G}. If there is a solution {1_A} to the tiling equation {1_F * 1_A = 1}, must there exist a periodic solution {1_{A_p}} to the same equation {1_F * 1_{A_p} = 1}?

We know that the answer to this question is positive for finite groups {H} (trivially, since all sets are periodic in this case), one-dimensional groups {{\bf Z} \times H} with {H} finite, and in {{\bf Z}^2}, but it can fail for {{\bf Z}^2 \times H} for certain finite {H}, and also for {{\bf Z}^d} for sufficiently large {d}; see this previous blog post for more discussion. But now one can consider other variants of this question:

  • Instead of considering level one tilings {1_F * 1_A = 1}, one can consider level {k} tilings {1_F * 1_A = k} for a given natural number {k} (so that every point in {G} is covered by exactly {k} translates of {F}), or more generally {1_F * 1_A = g} for some periodic function {g}.
  • Instead of requiring {1_F} and {1_A} to be indicator functions, one can allow these functions to be integer-valued, thus we are now studying convolution equations {f*a=g} where {f, g} are given integer-valued functions (with {g} periodic and {f} finitely supported).

We are able to obtain positive answers to three such analogues of the periodic tiling conjecture for three cases of this question. The first result (which was kindly shared with us by Tim Austin), concerns the homogeneous problem {f*a = 0}. Here the results are very satisfactory:

Theorem 2 (First periodic tiling result) Let {G} be a discrete abelian group, and let {f} be integer-valued and finitely supported. Then the following are equivalent.
  • (i) There exists an integer-valued solution {a} to {f*a=0} that is not identically zero.
  • (ii) There exists a periodic integer-valued solution {a_p} to {f * a_p = 0} that is not identically zero.
  • (iii) There is a vanishing Fourier coefficient {\hat f(\xi)=0} for some non-trivial character {\xi \in \hat G} of finite order.

By combining this result with an old result of Henry Mann about sums of roots of unity, as well as an even older decidability result of Wanda Szmielew, we obtain

Corollary 3 Any of the statements (i), (ii), (iii) is algorithmically decidable; there is an algorithm that, when given {G} and {f} as input, determines in finite time whether any of these assertions hold.

Now we turn to the inhomogeneous problem in {{\bf Z}^2}, which is the first difficult case (periodic tiling type results are easy to establish in one dimension, and trivial in zero dimensions). Here we have two results:

Theorem 4 (Second periodic tiling result) Let {G={\bf Z}^2}, let {g} be periodic, and let {f} be integer-valued and finitely supported. Then the following are equivalent.
  • (i) There exists an integer-valued solution {a} to {f*a=g}.
  • (ii) There exists a periodic integer-valued solution {a_p} to {f * a_p = g}.

Theorem 5 (Third periodic tiling result) Let {G={\bf Z}^2}, let {g} be periodic, and let {f} be integer-valued and finitely supported. Then the following are equivalent.
  • (i) There exists an indicator function solution {1_A} to {f*1_A=g}.
  • (ii) There exists a periodic indicator function solution {1_{A_p}} to {f * 1_{A_p} = g}.

In particular, the previously established case of periodic tiling conjecture for level one tilings of {{\bf Z}^2}, is now extended to higher level. By an old argument of Hao Wang, we now know that the statements mentioned in Theorem 5 are now also algorithmically decidable, although it remains open whether the same is the case for Theorem 4. We know from past results that Theorem 5 cannot hold in sufficiently high dimension (even in the classic case {g=1}), but it also remains open whether Theorem 4 fails in that setting.

Following past literature, we rely heavily on a structure theorem for solutions {a} to tiling equations {f*a=g}, which roughly speaking asserts that such solutions {a} must be expressible as a finite sum of functions {\varphi_w} that are one-periodic (periodic in a single direction). This already explains why tiling is easy to understand in one dimension, and why the two-dimensional case is more tractable than the case of general dimension. This structure theorem can be obtained by averaging a dilation lemma, which is a somewhat surprising symmetry of tiling equations that basically arises from finite characteristic arguments (viewing the tiling equation modulo {p} for various large primes {p}).

For Theorem 2, one can take advantage of the fact that the homogeneous equation {f*a=0} is preserved under finite difference operators {\partial_h a(x) := a(x+h)-a(x)}: if {a} solves {f*a=0}, then {\partial_h a} also solves the same equation {f * \partial_h a = 0}. This freedom to take finite differences one to selectively eliminate certain one-periodic components {\varphi_w} of a solution {a} to the homogeneous equation {f*a=0} until the solution is a pure one-periodic function, at which point one can appeal to an induction on dimension, to equate parts (i) and (ii) of the theorem. To link up with part (iii), we also take advantage of the existence of retraction homomorphisms from {{\bf C}} to {{\bf Q}} to convert a vanishing Fourier coefficient {\hat f(\xi)= 0} into an integer solution to {f*a=0}.

The inhomogeneous results are more difficult, and rely on arguments that are specific to two dimensions. For Theorem 4, one can also perform finite differences to analyze various components {\varphi_w} of a solution {a} to a tiling equation {f*a=g}, but the conclusion now is that the these components are determined (modulo {1}) by polynomials of one variable. Applying a retraction homomorphism, one can make the coefficients of these polynomials rational, which makes the polynomials periodic. This turns out to reduce the original tiling equation {f*a=g} to a system of essentially local combinatorial equations, which allows one to “periodize” a non-periodic solution by periodically repeating a suitable block of the (retraction homomorphism applied to the) original solution.

Theorem 5 is significantly more difficult to establish than the other two results, because of the need to maintain the solution in the form of an indicator function. There are now two separate sources of aperiodicity to grapple with. One is the fact that the polynomials involved in the components {\varphi_w} may have irrational coefficients (see Theorem 1.3 of our previous paper for an explicit example of this for a level 4 tiling). The other is that in addition to the polynomials (which influence the fractional parts of the components {\varphi_w}), there is also “combinatorial” data (roughly speaking, associated to the integer parts of {\varphi_w}) which also interact with each other in a slightly non-local way. Once one can make the polynomial coefficients rational, there is enough periodicity that the periodization approach used for the second theorem can be applied to the third theorem; the main remaining challenge is to find a way to make the polynomial coefficients rational, while still maintaining the indicator function property of the solution {a}.

It turns out that the restriction homomorphism approach is no longer available here (it makes the components {\varphi_w} unbounded, which makes the combinatorial problem too difficult to solve). Instead, one has to first perform a second moment analysis to discern more structure about the polynomials involved. It turns out that the components {\varphi_w} of an indicator function {1_A} can only utilize linear polynomials (as opposed to polynomials of higher degree), and that one can partition {{\bf Z}^2} into a finite number of cosets on which only three of these linear polynomials are “active” on any given coset. The irrational coefficients of these linear polynomials then have to obey some rather complicated, but (locally) finite, sentence in the theory of first-order linear inequalities over the rationals, in order to form an indicator function {1_A}. One can then use the Weyl equidistribution theorem to replace these irrational coefficients with rational coefficients that obey the same constraints (although one first has to ensure that one does not accidentally fall into the boundary of the constraint set, where things are discontinuous). Then one can apply periodization to the remaining combinatorial data to conclude.

A key technical problem arises from the discontinuities of the fractional part operator {\{x\}} at integers, so a certain amount of technical manipulation (in particular, passing at one point to a weak limit of the original tiling) is needed to avoid ever having to encounter this discontinuity.

In a recent post, I talked about a proof of concept tool to verify estimates automatically. Since that post, I have overhauled the tool twice: first to turn it into a rudimentary proof assistant that could also handle some propositional logic; and second into a much more flexible proof assistant (deliberately designed to mimic the Lean proof assistant in several key aspects) that is also powered by the extensive Python package sympy for symbolic algebra, following the feedback from previous commenters. This I think is now a stable framework with which one can extend the tool much further; my initial aim was just to automate (or semi-automate) the proving of asymptotic estimates involving scalar functions, but in principle one could keep adding tactics, new sympy types, and lemmas to the tool to handle a very broad range of other mathematical tasks as well.

The current version of the proof assistant can be found here. (As with my previous coding, I ended up relying heavily on large language model assistance to understand some of the finer points of Python and sympy, with the autocomplete feature of Github Copilot being particularly useful.) While the tool can support fully automated proofs, I have decided to focus more for now on semi-automated interactive proofs, where the human user supplies high-level “tactics” that the proof assistant then performs the necessary calculations for, until the proof is completed.

It’s easiest to explain how the proof assistant works with examples. Right now I have implemented the assistant to work inside the interactive mode of Python, in which one enters Python commands one at a time. (Readers from my generation may be familiar with text adventure games, which have a broadly similar interface.) I would be interested developing at some point a graphical user interface for the tool, but for prototype purposes, the Python interactive version suffices. (One can also run the proof assistant within a Python script, of course.)

After downloading the relevant files, one can launch the proof assistant inside Python by typing from main import * and then loading one of the pre-made exercises. Here is one such exercise:

>>> from main import *
>>> p = linarith_exercise()
Starting proof. Current proof state:
x: pos_real
y: pos_real
z: pos_real
h1: x < 2*y
h2: y < 3*z + 1
|- x < 7*z + 2

This is the proof assistant’s formalization of the following problem: If x,y,z are positive reals such that x < 2y and y < 3z+1, prove that x < 7z+2.

The way the proof assistant works is that one directs the assistant to use various “tactics” to simplify the problem until it is solved. In this case, the problem can be solved by linear arithmetic, as formalized by the Linarith() tactic:

>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!

If instead one wanted a bit more detail on how the linear arithmetic worked, one could have run this tactic instead with a verbose flag:

>>> p.use(Linarith(verbose=true))
Checking feasibility of the following inequalities:
1*z > 0
1*x + -7*z >= 2
1*y + -3*z < 1
1*y > 0
1*x > 0
1*x + -2*y < 0
Infeasible by summing the following:
1*z > 0 multiplied by 1/4
1*x + -7*z >= 2 multiplied by 1/4
1*y + -3*z < 1 multiplied by -1/2
1*x + -2*y < 0 multiplied by -1/4
Goal solved by linear arithmetic!
Proof complete!

Sometimes, the proof involves case splitting, and then the final proof has the structure of a tree. Here is one example, where the task is to show that the hypotheses (x>-1) \wedge (x<1) and (y>-2) \wedge (y<2) imply (x+y>-3) \wedge (x+y<3):

>>> from main import *
>>> p = split_exercise()
Starting proof. Current proof state:
x: real
y: real
h1: (x > -1) & (x < 1)
h2: (y > -2) & (y < 2)
|- (x + y > -3) & (x + y < 3)
>>> p.use(SplitHyp("h1"))
Decomposing h1: (x > -1) & (x < 1) into components x > -1, x < 1.
1 goal remaining.
>>> p.use(SplitHyp("h2"))
Decomposing h2: (y > -2) & (y < 2) into components y > -2, y < 2.
1 goal remaining.
>>> p.use(SplitGoal())
Split into conjunctions: x + y > -3, x + y < 3
2 goals remaining.
>>> p.use(Linarith())
Goal solved by linear arithmetic!
1 goal remaining.
>>> p.use(Linarith())
Goal solved by linear arithmetic!
Proof complete!
>>> print(p.proof())
example (x: real) (y: real) (h1: (x > -1) & (x < 1)) (h2: (y > -2) & (y < 2)): (x + y > -3) & (x + y < 3) := by
 split_hyp h1
 split_hyp h2
 split_goal
 . linarith
 linarith

Here at the end we gave a “pseudo-Lean” description of the proof in terms of the three tactics used: a tactic cases h1 to case split on the hypothesis h1, followed by two applications of the simp_all tactic to simplify in each of the two cases.

The tool supports asymptotic estimation. I found a way to implement the order of magnitude formalism from the previous post within sympy. It turns out that sympy, in some sense, already natively implements nonstandard analysis: its symbolic variables have an is_number flag which basically corresponds to the concept of a “standard” number in nonstandard analysis. For instance, the sympy version S(3) of the number 3 has S(3).is_number == True and so is standard, whereas an integer variable n = Symbol("n", integer=true) has n.is_number == False and so is nonstandard. Within sympy, I was able to construct orders of magnitude Theta(X) of various (positive) expressions X, with the property that Theta(n)=Theta(1) if n is a standard number, and use this concept to then define asymptotic estimates such as X \lesssim Y (implemented as lesssim(X,Y)). One can then apply a logarithmic form of linear arithmetic to then automatically verify some asymptotic estimates. Here is a simple example, in which one is given a positive integer N and positive reals x,y such that x \leq 2N^2 and y < 3N, and the task is to conclude that xy \lesssim N^4:

>>> p = loglinarith_exercise()
Starting proof. Current proof state:
N: pos_int
x: pos_real
y: pos_real
h1: x <= 2*N**2
h2: y < 3*N
|- Theta(x)*Theta(y) <= Theta(N)**4
>>> p.use(LogLinarith(verbose=True))
Checking feasibility of the following inequalities:
Theta(N)**1 >= Theta(1)
Theta(x)**1 * Theta(N)**-2 <= Theta(1)
Theta(y)**1 * Theta(N)**-1 <= Theta(1)
Theta(x)**1 * Theta(y)**1 * Theta(N)**-4 > Theta(1)
Infeasible by multiplying the following:
Theta(N)**1 >= Theta(1) raised to power 1
Theta(x)**1 * Theta(N)**-2 <= Theta(1) raised to power -1
Theta(y)**1 * Theta(N)**-1 <= Theta(1) raised to power -1
Theta(x)**1 * Theta(y)**1 * Theta(N)**-4 > Theta(1) raised to power 1
Proof complete!

The logarithmic linear programming solver can also handle lower order terms, by a rather brute force branching method:

>>> p = loglinarith_hard_exercise()
Starting proof. Current proof state:
N: pos_int
x: pos_real
y: pos_real
h1: x <= 2*N**2 + 1
h2: y < 3*N + 4
|- Theta(x)*Theta(y) <= Theta(N)**3
>>> p.use(LogLinarith())
Goal solved by log-linear arithmetic!
Proof complete!

I plan to start developing tools for estimating function space norms of symbolic functions, for instance creating tactics to deploy lemmas such as Holder’s inequality and the Sobolev embedding inequality. It looks like the sympy framework is flexible enough to allow for creating further object classes for these sorts of objects. (Right now, I only have one proof-of-concept lemma to illustrate the framework, the arithmetic mean-geometric mean lemma.)

I am satisfied enough with the basic framework of this proof assistant that I would be open to further suggestions or contributions of new features, for instance by introducing new data types, lemmas, and tactics, or by contributing example problems that ought to be easily solvable by such an assistant, but are currently beyond its ability, for instance due to the lack of appropriate tactics and lemmas.

Archives

AltStyle によって変換されたページ (->オリジナル) /