You are currently browsing the category archive for the ‘math.CA’ category.
A function of one variable can be translated in space by a spatial shift
to obtain a new function
Some functions obey finite linear relations between their time-frequency shifts. For instance, a sinusoid obeys the relation
Conjecture 1 (HRT conjecture) Ifis non-zero, then there is no relation of the form
for some distinct points
and some coefficients
, not all zero.
A special case of the HRT conjecture, which was also open, makes the additional assumption that was Schwartz.
Many positive results towards this conjecture were known. I will mention only a few here. There is a result of Linnell that the conjecture is true if lie in a translate of a discrete subgroup of
; this (together with an argument handling the collinear case) establishes all cases where
, and several partial results involving the
cases are also known. The conjecture is also known if
is decays at a suitably super-exponential rate, by work of Bownik and Speegle.
I was aware of this conjecture through various talks and conversations with colleagues, and even briefly tried my hand at it for a while, though not with particularly serious effort (or progress). It was thus a nice surprise to see that it has just been resolved by Faulhuber, Petersen, van Velthoven, and Voigtlaender, even in the Schwartz case:
Theorem 2 There exist complex numbers, not all zero, distinct points
, and a non-zero Schwartz function
such that
It is perhaps unsurprising in this current era that this result is AI-assisted. However, I think the authors have disclosed their AI use responsibly, with the final arguments written by hand with a readable overview of the argument, as well as proper discussion of methods, relation to past literature, and other independent numerical checks on the result.
The negative result lies only a little beyond the positive results: is now increased to
, and all but one of the points
lie in (a translate of) a discrete subgroup of
(in fact the explicit subgroup
is used). The functions constructed are smooth and rapidly decaying, but not analytic or super-exponentially decaying, which would start being in conflict with the known positive results.
In addition to AI being used to come up with the initial proof strategy, a more traditional numerical computation was used to verify one step of the argument.
I have not had the time to do a full digestion of the result, but (after reading the introduction, and using a little AI assistance of my own) I was able to understand the main ideas at a high level. The first few reductions are relatively standard. Setting and
, one can view the problem as one of solving an eigenvalue problem
How to solve this equation? The motivating scenario here is if the matrix function was replaced by a rank one function
The main remaining obstacle is that the “eigenvalue function” is varying in the parameter
rather than constant. (This issue was, by the way, anticipated to some extent in previous work of Demeter, who observed that eigenfunctions of the almost Matthieu discrete Schrödinger operator gave a near-miss counterexample to the HRT conjecture, but with an eigenvalue that depended on an auxiliary phase shift parameter rather than constant.) However, if one was able to solve the scalar cocycle equation
I’ve just uploaded to the arXiv my paper “Local Bernstein theory, and lower bounds for Lebesgue constants“. This paper was initially motivated by a problem of Erdős} on Lagrange interpolation, but in the course of solving that problem, I ended up modifying some very classical arguments of Bernstein and his contemporaries (Boas, Duffin, Schaeffer, Riesz, etc.) to obtain “local” versions of these classical “Bernstein-type inequalities” that may be of independent interest.
Bernstein proved many estimates concerning the derivatives of polynomials, trigonometric polynomials, and entire functions of exponential type, but perhaps his most famous inequality in this direction is:
Lemma 1 (Bernstein’s inequality for trigonometric polynomials) Letbe a trigonometric polynomial of degree at most
, with
for all
. Then
for all
.
Similar inequalities concerning norms of derivatives of Littlewood-Paley components of functions are now ubiquitious in the modern theory of nonlinear dispersive PDE (where they are also called Bernstein estimates), but this will not be the focus of this current post.
A trigonometric polynomial of degree
is of exponential type
in the sense that
for complex
. Bernstein in fact proved a more general result:
Lemma 2 (Bernstein’s inequality for functions of exponential type) Letbe an entire function of exponential type at most
, with
for all
. Then
for all
.
There are several proofs of this lemma – see for instance this survey of Queffélec and Zarouf. In the case that is real-valued on
, there is a nice proof by Duffin and Schaeffer, which we sketch as follows. Suppose we normalize
, and adjust
by a suitable damping factor so that
actually decays slower than
as
. Then, for any
and
, one can use Rouche’s theorem to show that the function
has the same number of zeroes as
in a suitable large rectangle; but on the other hand one can use the intermediate value theorem to show that
has at least as many zeroes than
in the same rectangle. Among other things, this prevents double zeroes from occuring, which turns out to give the desired claim
after some routine calculations (in fact one obtains the stronger bound
for all real
).
The first main result of the paper is to obtain localized versions of Lemma 2 (as well as some related estimates). Roughly speaking, these estimates assert that if is holomorphic on a wide thin rectangle passing through the real axis, is bounded by
on the intersection of the real axis with this rectangle, and is “locally of exponential type” in the sense that it is bounded by
on the upper and lower edges of this rectangle (and obeys some very mild growth conditions on the remaining sides of this rectangle), then
can be bounded by
plus small errors on the real line, with some additional estimates away from the real line also available. The proof proceeds by a modification of the Duffin–Schaeffer argument, together with the two-constant theorem of Nevanlinna (and some standard estimates of harmonic measures on rectangles) to deal with the effect of the localization. (As a side note, this latter argument was provided to me by ChatGPT, as I was not previously aware of the Nevanlinna two-constant theorem.)
Once one localizes this “Bernstein theory”, it becomes suitable for the analysis of (real-rooted, monic) polynomials of a high degree
, which are not bounded globally on
(and grow polynomially rather than exponentially at infinity), but which can exhibit “local exponential type” behavior on various intervals, particularly in regions where the logarithmic potential
This becomes relevant in the theory of Lagrange interpolation. Recall that if are real numbers and
is a polynomial of degree less than
then one has the interpolation formula
If one chooses the interpolation points poorly, then the Lebesgue constant can be extremely large. However, if one selects these points to be the roots of the aforementioned monic Chebyshev polynomials, then it is known that
for all fixed intervals
in
. In the case
, it was shown by Erdős} that this is the best possible value of the Lebesgue constant up to
errors for interpolation on
, thus
In terms of the monic polynomial , these two estimates can be written as
Problem 3 Letbe a trigonometric polynomial of degree
with
roots
in
.
It is easy to check that the lower bounds of and
are sharp by considering the case when
is a sinusoid
.
The bound (3) is immediate from Bernstein’s inequality (Lemma 1). By applying a local version of this inequality, I was able to get a weak version of the claim (1) in which was replaced with
; see this early version of the paper, which was developed through conversations with Nat Sothanaphan and Aron Bhalla. By combining this argument with ideas from the older work of Erdős}, I was able to establish (1).
The bound (2) took me longer to establish, and involved a non-trivial amount of playing around with AI tools, the story of which I would like to share here. I had discovered the toy problem (4), but initially was not able to establish this inequality; AlphaEvolve seemed to confirm it numerically (with sinusoids appearing to be the extremizer), but did not offer direct clues on how to prove this rigorously. At some point I realized that the left-hand side factorized into the expressions and
, and tried to bound these expressions separately. Perturbing around a sinusoid
, I was able to show that the
norm
was a local minimum as long as one only perturbed by lower order Fourier modes, keeping the frequency
coefficients unchanged. Guessing that this local minimum was actually a global minimum, this led me to conjecture the general lower bound
Problem 1026 on the Erdős problem web site recently got solved through an interesting combination of existing literature, online collaboration, and AI tools. The purpose of this blog post is to try to tell the story of this collaboration, and also to supply a complete proof.
The original problem of Erdős, posed in 1975, is rather ambiguous. Erdős starts by recalling his famous theorem with Szekeres that says that given a sequence of distinct real numbers, one can find a subsequence of length
which is either increasing or decreasing; and that one cannot improve the
to
, by considering for instance a sequence of
blocks of length
, with the numbers in each block decreasing, but the blocks themselves increasing. He also noted a result of Hanani that every sequence of length
can be decomposed into the union of
monotone sequences. He then wrote “As far as I know the following question is not yet settled. Let
be a sequence of distinct numbers, determine
This problem was added to the Erdős problem site on September 12, 2025, with a note that the problem was rather ambiguous. For any fixed , this is an explicit piecewise linear function of the variables
that could be computed by a simple brute force algorithm, but Erdős was presumably seeking optimal bounds for this quantity under some natural constraint on the
. The day the problem was posted, Desmond Weisenberg proposed studying the quantity
, defined as the largest constant such that
Though not stated on the web site, one can formulate this problem in game theoretic terms. Suppose that Alice has a stack of coins for some large
. She divides the coins into
piles of consisting of
coins each, so that
. She then passes the piles to Bob, who is allowed to select a monotone subsequence of the piles (in the weak sense) and keep all the coins in those piles. What is the largest fraction
of the coins that Bob can guarantee to keep, regardless of how Alice divides up the coins? (One can work with either a discrete version of this problem where the
are integers, or a continuous one where the coins can be split fractionally, but in the limit
the problems can easily be seen to be equivalent.)
AI-generated images continue to be problematic for a number of reasons, but here is one such image that somewhat manages at least to convey the idea of the game:
For small , one can work out
by hand. For
, clearly
: Alice has to put all the coins into one pile, which Bob simply takes. Similarly
: regardless of how Alice divides the coins into two piles, the piles will either be increasing or decreasing, so in either case Bob can take both. The first interesting case is
. Bob can again always take the two largest piles, guaranteeing himself
of the coins. On the other hand, if Alice almost divides the coins evenly, for instance into piles
for some small
, then Bob cannot take all three piles as they are non-monotone, and so can only take two of them, allowing Alice to limit the payout fraction to be arbitrarily close to
. So we conclude that
.
An hour after Desmond’s comment, Stijn Cambie noted (though not in the language I used above) that a similar construction to the one above, in which Alice divides the coins into pairs that are almost even, in such a way that the longest monotone sequence is of length
, gives the upper bound
. It is also easy to see that
is a non-increasing function of
, so this gives a general bound
. Less than an hour after that, Wouter van Doorn noted that the Hanani result mentioned above gives the lower bound
, and posed the problem of determining the asymptotic limit of
as
, given that this was now known to range between
and
. This version was accepted by Thomas Bloom, the moderator of the Erdős problem site, as a valid interpretation of the original problem.
The next day, Stijn computed the first few values of exactly:
The problem then lay dormant for almost two months, until December 7, 2025, in which Boris Alexeev, as part of a systematic sweep of the Erdős problems using the AI tool Aristotle, was able to get this tool to autonomously solve this conjecture in the proof assistant language Lean. The proof converted the problem to a rectangle-packing problem.
This was one further addition to a recent sequence of examples where an Erdős problem had been automatically solved in one fashion or another by an AI tool. Like the previous cases, the proof turned out to not be particularly novel. Within an hour, Koishi Chan gave an alternate proof deriving the required bound from the original Erdős-Szekeres theorem by a standard “blow-up” argument which we can give here in the Alice-Bob formulation. Take a large
, and replace each pile of
coins with
new piles, each of size
, chosen so that the longest monotone subsequence in this collection is
. Among all the new piles, the longest monotone subsequence has length
. Applying Erdős-Szekeres, one concludes the bound
Once this proof was found, it was natural to try to see if it had already appeared in the literature. AI deep research tools have successfully located such prior literature in the past, but in this case they did not succeed, and a more “old-fashioned” Google Scholar job turned up some relevant references: a 2016 paper by Tidor, Wang and Yang contained this precise result, citing an earlier paper of Wagner as inspiration for applying “blowup” to the Erdős-Szekeres theorem.
But the story does not end there! Upon reading the above story the next day, I realized that the problem of estimating was a suitable task for AlphaEvolve, which I have used recently as mentioned in this previous post. Specifically, one could task to obtain upper bounds on
by directing it to produce real numbers (or integers)
summing up to a fixed sum (I chose
) with a small a value of
as possible. After an hour of run time, AlphaEvolve produced the following upper bounds on
for
, with some intriguingly structured potential extremizing solutions:

Proposition 1 Ifand
, then
.
Proof: Consider a sequence of numbers clustered around the “red number”
and “blue number”
, consisting of
blocks of
“blue” numbers, followed by
blocks of
“red” numbers, and then
further blocks of
“blue” numbers. When
, one should take all blocks to be slightly decreasing within each block, but the blue blocks should be are increasing between each other, and the red blocks should also be increasing between each other. When
, all of these orderings should be reversed. The total number of elements is indeed
Here is a figure illustrating the above construction in the case (obtained after starting with a ChatGPT-provided file and then manually fixing a number of placement issues):
Here is a plot of (produced by ChatGPT Pro), showing that it is basically a piecewise linear approximation to the square root function:
Shortly afterwards, Lawrence Wu clarified the connection between this problem and a square packing problem, which was also due to Erdős (Problem 106). Let be the least number such that, whenever one packs
squares of sidelength
into a square of sidelength
, with all sides parallel to the coordinate axes, one has
Proposition 2 For any, one has
Proof: Given and
, let
be the maximal sum over all increasing subsequences ending in
, and
be the maximal sum over all decreasing subsequences ending in
. For
, we have either
(if
) or
(if
). In particular, the squares
and
are disjoint. These squares pack into the square
, so by definition of
, we have
This idea of using packing to prove Erdős-Szekeres type results goes back to a 1959 paper of Seidenberg, although it was a discrete rectangle-packing argument that was not phrased in such an elegantly geometric form. It is possible that Aristotle was “aware” of the Seidenberg argument via its training data, as it had incorporated a version of this argument in its proof.
Here is an illustration of the above argument using the AlphaEvolve-provided example
for to convert it to a square packing (image produced by ChatGPT Pro):
At this point, Lawrence performed another AI deep research search, this time successfully locating a paper from just last year by Baek, Koizumi, and Ueoro, where they show that
Theorem 3 For any, one has
which, when combined with a previous argument of Praton, implies
Theorem 4 For anyand
with
, one has
This proves the conjecture!
There just remained the issue of putting everything together. I did feed all of the above information into a large language model, which was able to produce a coherent proof of (1) assuming the results of Baek-Koizumi-Ueoro and Praton. Of course, LLM outputs are prone to hallucination, so it would be preferable to formalize that argument in Lean, but this looks quite doable with current tools, and I expect this to be accomplished shortly. But I was also able to reproduce the arguments of Baek-Koizumi-Ueoro and Praton, which I include below for completeness.
Proof: (Proof of Theorem 3, adapted from Baek-Koizumi-Ueoro) We can normalize . It then suffices to show that if we pack the length
torus
by
axis-parallel squares of sidelength
, then
Pick . Then we have a
grid
UPDATE: Actually, the above argument also proves Theorem 4 with only minor modifications. Nevertheless, we give the original derivation of Theorem 4 using the embedding argument of Praton below for sake of completeness.
Proof: (Proof of Theorem 4, adapted from Praton) We write with
. We can rescale so that the square one is packing into is
. Thus, we pack
squares of sidelength
into
, and our task is to show that
- The sequence can be numerically computed as a sequence of rational numbers.
- When appropriately normalized and arranged, visible patterns in this sequence appear that allow one to conjecture the form of the sequence.
- This problem is a weighted version of the Erdős-Szekeres theorem.
- Among the many proofs of the Erdős-Szekeres theorem is the proof of Seidenberg in 1959, which can be interpreted as a discrete rectangle packing argument.
- This problem can be reinterpreted as a continuous square packing problem, and in fact is closely related to (a generalized axis-parallel form of) Erdős problem 106, which concerns such packings.
- The axis-parallel form of Erdős problem 106 was recently solved by Baek-Koizumi-Ueoro.
- The paper of Praton shows that Erdős Problem 106 implies the generalized version needed for this problem. This implication specializes to the axis-parallel case.
Another key ingredient was the balanced AI policy on the Erdős problem website, which encourages disclosed AI usage while strongly discouraging undisclosed use. To quote from that policy: “Comments prepared with the assistance of AI are permitted, provided (a) this is disclosed, (b) the contents (including mathematics, code, numerical data, and the existence of relevant sources) have been carefully checked and verified by the user themselves without the assistance of AI, and (c) the comment is not unreasonably long.”
Bogdan Georgiev, Javier Gómez-Serrano, Adam Zsolt Wagner, and I have uploaded to the arXiv our paper “Mathematical exploration and discovery at scale“. This is a longer report on the experiments we did in collaboration with Google Deepmind with their AlphaEvolve tool, which is in the process of being made available for broader use. Some of our experiments were already reported on in a previous white paper, but the current paper provides more details, as well as a link to a repository with various relevant data such as the prompts used and the evolution of the tool outputs.
AlphaEvolve is a variant of more traditional optimization tools that are designed to extremize some given score function over a high-dimensional space of possible inputs. A traditional optimization algorithm might evolve one or more trial inputs over time by various methods, such as stochastic gradient descent, that are intended to locate increasingly good solutions while trying to avoid getting stuck at local extrema. By contrast, AlphaEvolve does not evolve the score function inputs directly, but uses an LLM to evolve computer code (often written in a standard language such as Python) which will in turn be run to generate the inputs that one tests the score function on. This reflects the belief that in many cases, the extremizing inputs will not simply be an arbitrary-looking string of numbers, but will often have some structure that can be efficiently described, or at least approximated, by a relatively short piece of code. The tool then works with a population of relatively successful such pieces of code, with the code from one generation of the population being modified and combined by the LLM based on their performance to produce the next generation. The stochastic nature of the LLM can actually work in one’s favor in such an evolutionary environment: many “hallucinations” will simply end up being pruned out of the pool of solutions being evolved due to poor performance, but a small number of such mutations can add enough diversity to the pool that one can break out of local extrema and discover new classes of viable solutions. The LLM can also accept user-supplied “hints” as part of the context of the prompt; in some cases, even just uploading PDFs of relevant literature has led to improved performance by the tool. Since the initial release of AlphaEvolve, similar tools have been developed by others, including OpenEvolve, ShinkaEvolve and DeepEvolve.
We tested this tool on a large number (67) of different mathematics problems (both solved and unsolved) in analysis, combinatorics, and geometry that we gathered from the literature, and reported our outcomes (both positive and negative) in this paper. In many cases, AlphaEvolve achieves similar results to what an expert user of a traditional optimization software tool might accomplish, for instance in finding more efficient schemes for packing geometric shapes, or locating better candidate functions for some calculus of variations problem, than what was previously known in the literature. But one advantage this tool seems to offer over such custom tools is that of scale, particularly when when studying variants of a problem that we had already tested this tool on, as many of the prompts and verification tools used for one problem could be adapted to also attack similar problems; several examples of this will be discussed below. The following graphic illustrates the performance of AlphaEvolve on this body of problems:

Another advantage of AlphaEvolve was robustness adaptability: it was relatively easy to set up AlphaEvolve to work on a broad array of problems, without extensive need to call on domain knowledge of the specific task in order to tune hyperparameters. In some cases, we found that making such hyperparameters part of the data that AlphaEvolve was prompted to output was better than trying to work out their value in advance, although a small amount of such initial theoretical analysis was helpful. For instance, in calculus of variation problems, one is often faced with the need to specify various discretization parameters in order to estimate a continuous integral, which cannot be computed exactly, by a discretized sum (such as a Riemann sum), which can be evaluated by computer to some desired precision. We found that simply asking AlphaEvolve to specify its own discretization parameters worked quite well (provided we designed the score function to be conservative with regards to the possible impact of the discretization error); see for instance this experiment in locating the best constant in functional inequalities such as the Hausdorff-Young inequality.
A third advantage of AlphaEvolve over traditional optimization methods was the interpretability of many of the solutions provided. For instance, in one of our experiments we sought to find an extremum to a functional inequality such as the Gagliardo–Nirenberg inequality (a variant of the Sobolev inequality). This is a relatively well-behaved optimization problem, and many standard methods can be deployed to obtain near-optimizers that are presented in some numerical format, such as a vector of values on some discretized mesh of the domain. However, when we applied AlphaEvolve to this problem, the tool was able to discover the exact solution (in this case, a Talenti function), and create code that sampled from that function on a discretized mesh to provide the required input for the scoring function we provided (which only accepted discretized inputs, due to the need to compute the score numerically). This code could be inspected by humans to gain more insight as to the nature of the optimizer. (Though in some cases, AlphaEvolve’s code would contain some brute force search, or a call to some existing optimization subroutine in one of the libraries it was given access to, instead of any more elegant description of its output.)
For problems that were sufficiently well-known to be in the training data of the LLM, the LLM component of AlphaEvolve often came up almost immediately with optimal (or near-optimal) solutions. For instance, for variational problems where the gaussian was known to be the extremizer, AlphaEvolve would frequently guess a gaussian candidate during one of the early evolutions, and we would have to obfuscate the problem significantly to try to conceal the connection to the literature in order for AlphaEvolve to experiment with other candidates. AlphaEvolve would also propose similar guesses for other problems for which the extremizer was not known. For instance, we tested this tool on the sum-difference exponents of relevance to the arithmetic Kakeya conjecture, which can be formulated as a variational entropy inequality concerning certain two-dimensional discrete random variables. AlphaEvolve initially proposed some candidates for such variables based on discrete gaussians, which actually worked rather well even if they were not the exact extremizer, and already generated some slight improvements to previous lower bounds on such exponents in the literature. Inspired by this, I was later able to rigorously obtain some theoretical results on the asymptotic behavior on such exponents in the regime where the number of slopes was fixed, but the “rational complexity” of the slopes went to infinity; this will be reported on in a separate paper.
Perhaps unsurprisingly, AlphaEvolve was extremely good at locating “exploits” in the verification code we provided, for instance using degenerate solutions or overly forgiving scoring of approximate solutions to come up with proposed inputs that technically achieved a high score under our provided code, but were not in the spirit of the actual problem. For instance, when we asked it (link under construction) to find configurations to extremal geometry problems such as locating polygons with each vertex having four equidistant other vertices, we initially coded the verifier to accept distances that were equal only up to some high numerical precision, at which point AlphaEvolve promptly placed many of the points in virtually the same location so that the distances they determined were indistinguishable. Because of this, a non-trivial amount of human effort needs to go into designing a non-exploitable verifier, for instance by working with exact arithmetic (or interval arithmetic) instead of floating point arithmetic, and taking conservative worst-case bounds in the presence of uncertanties in measurement to determine the score. For instance, in testing AlphaEvolve against the “moving sofa” problem and its variants, we designed a conservative scoring function that only counted those portions of the sofa that we could definitively prove to stay inside the corridor at all times (not merely the discrete set of times provided by AlphaEvolve to describe the sofa trajectory) to prevent it from exploiting “clipping” type artefacts. Once we did so, it performed quite well, for instance rediscovering the optimal “Gerver sofa” for the original sofa problem, and also discovering new sofa designs for other problem variants, such as a 3D sofa problem.
For well-known open conjectures (e.g., Sidorenko’s conjecture, Sendov’s conjecture, Crouzeix’s conjecture, the ovals problem, etc.), AlphaEvolve generally was able to locate the previously known candidates for optimizers (that are conjectured to be optimal), but did not locate any stronger counterexamples: thus, we did not disprove any major open conjecture. Of course, one obvious possible explanation for this is that these conjectures are in fact true; outside of a few situations where there is a matching “dual” optimization problem, AlphaEvolve can only provide one-sided bounds on such problems and so cannot definitively determine if the conjectural optimizers are in fact the true optimizers. Another potential explanation is that AlphaEvolve essentially tried all the “obvious” constructions that previous researchers working on these problems had also privately experimented with, but did not report due to the negative findings. However, I think there is at least value in using these tools to systematically record negative results (roughly speaking, that a search for “obvious” counterexamples to a conjecture did not disprove the claim), which currently only exist as “folklore” results at best. This seems analogous to the role LLM Deep Research tools could play by systematically recording the results (both positive and negative) of automated literature searches, as a supplement to human literature review which usually reports positive results only. Furthermore, when we shifted attention to less well studied variants of famous conjectures, we were able to find some modest new observations. For instance, while AlphaEvolve only found the standard conjectural extremizer to Sendov’s conjecture, as well as for variants such as Borcea’s conjecture, Schmeisser’s conjecture, or Smale’s conjecture it did reveal some potential two-parameter extensions to a conjecture of de Bruin and Sharma that had not previously been stated in the literature. (For this problem, we were not directly optimizing some variational scalar quantity, but rather a two-dimensional range of possible values, which we could adapt the AlphaEvolve framework to treat). In the future, I can imagine such tools being a useful “sanity check” when proposing any new conjecture, in that it will become common practice to run one of these tools against such a conjecture to make sure there are no “obvious” counterexamples (while keeping in mind that this is still far from conclusive evidence in favor of such a conjecture).
AlphaEvolve did not perform equally well across different areas of mathematics. When testing the tool on analytic number theory problems, such as that of designing sieve weights for elementary approximations to the prime number theorem, it struggled to take advantage of the number theoretic structure in the problem, even when given suitable expert hints (although such hints have proven useful for other problems). This could potentially be a prompting issue on our end, or perhaps the landscape of number-theoretic optimization problems is less amenable to this sort of LLM-based evolutionary approach. On the other hand, AlphaEvolve does seem to do well when the constructions have some algebraic structure, such as with the finite field Kakeya and Nikodym set problems, which we will turn to shortly.
For many of our experiments we worked with fixed-dimensional problems, such as trying to optimally pack shapes in a larger shape for a fixed value of
. However, we found in some cases that if we asked AlphaEvolve to give code that took parameters such as
as input, and tested the output of that code for a suitably sampled set of values of
of various sizes, then it could sometimes generalize the constructions it found for small values of this parameter to larger ones; for instance, in the infamous sixth problem of this year’s IMO, it could use this technique to discover the optimal arrangement of tiles, which none of the frontier models could do at the time (although AlphaEvolve has no capability to demonstrate that this arrangement was, in fact, optimal). Another productive use case of this technique was for finding finite field Kakeya and Nikodym sets of small size in low-dimensional vector spaces over finite fields of various sizes. For Kakeya sets in
, it located the known optimal construction based on quadratic residues in two dimensions, and very slightly beat (by an error term of size
) the best construction in three dimensions; this was an algebraic construction (still involving quadratic residues) discovered empirically that we could then prove to be correct by first using Gemini’s “Deep Think” tool to locate an informal proof, which we could then convert into a formalized Lean proof by using Google Deepmind’s “AlphaProof” tool. At one point we thought it had found a construction in four dimensions which achieved a more noticeable improvement (of order
) of what we thought was the best known construction, but we subsequently discovered that essentially the same construction had appeared already in a paper of Bukh and Chao, although it still led to a more precise calculation of the error term (to accuracy
rather than
, where the error term now involves the Lang-Weil inequality and is unlikely to have a closed form). Perhaps AlphaEvolve had somehow absorbed the Bukh-Chao construction within its training data to accomplish this. However, when we tested the tool on Nikodym sets (which are expected to have asymptotic density
, although this remains unproven), it did find some genuinely new constructions of such sets in three dimensions, based on removing quadratic varieties from the entire space. After using “Deep Think” again to analyze these constructions, we found that they were inferior to a purely random construction (which in retrospect was an obvious thing to try); however, they did inspire a hybrid construction in which one removed random quadratic varieties and performed some additional cleanup, which ends up outperforming both the purely algebraic and purely random constructions. This result (with completely human-generated proofs) will appear in a subsequent paper.
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:
- Section 2.1: The natural numbers
- Section 2.2: Addition
- Section 2.3: Multiplication
- Chapter 2 epilogue: Isomorphism with the Mathlib natural numbers
- Section 3.1: Basic set theory
- Section 4.1: The integers
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 . 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 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 , consider the following question:
Question 1 (Periodic tiling question) Letbe a finite subset of
. If there is a solution
to the tiling equation
, must there exist a periodic solution
to the same equation
?
We know that the answer to this question is positive for finite groups (trivially, since all sets are periodic in this case), one-dimensional groups
with
finite, and in
, but it can fail for
for certain finite
, and also for
for sufficiently large
; see this previous blog post for more discussion. But now one can consider other variants of this question:
- Instead of considering level one tilings
, one can consider level
tilings
for a given natural number
(so that every point in
is covered by exactly
translates of
), or more generally
for some periodic function
.
- Instead of requiring
and
to be indicator functions, one can allow these functions to be integer-valued, thus we are now studying convolution equations
where
are given integer-valued functions (with
periodic and
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 . Here the results are very satisfactory:
Theorem 2 (First periodic tiling result) Letbe a discrete abelian group, and let
be integer-valued and finitely supported. Then the following are equivalent.
- (i) There exists an integer-valued solution
to
that is not identically zero.
- (ii) There exists a periodic integer-valued solution
to
that is not identically zero.
- (iii) There is a vanishing Fourier coefficient
for some non-trivial character
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 givenand
as input, determines in finite time whether any of these assertions hold.
Now we turn to the inhomogeneous problem in , 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, let
be periodic, and let
be integer-valued and finitely supported. Then the following are equivalent.
- (i) There exists an integer-valued solution
to
.
- (ii) There exists a periodic integer-valued solution
to
.
Theorem 5 (Third periodic tiling result) Let, let
be periodic, and let
be integer-valued and finitely supported. Then the following are equivalent.
- (i) There exists an indicator function solution
to
.
- (ii) There exists a periodic indicator function solution
to
.
In particular, the previously established case of periodic tiling conjecture for level one tilings of , 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
), but it also remains open whether Theorem 4 fails in that setting.
Following past literature, we rely heavily on a structure theorem for solutions to tiling equations
, which roughly speaking asserts that such solutions
must be expressible as a finite sum of functions
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
for various large primes
).
For Theorem 2, one can take advantage of the fact that the homogeneous equation is preserved under finite difference operators
: if
solves
, then
also solves the same equation
. This freedom to take finite differences one to selectively eliminate certain one-periodic components
of a solution
to the homogeneous equation
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
to
to convert a vanishing Fourier coefficient
into an integer solution to
.
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 of a solution
to a tiling equation
, but the conclusion now is that the these components are determined (modulo
) 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
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 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
), there is also “combinatorial” data (roughly speaking, associated to the integer parts of
) 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
.
It turns out that the restriction homomorphism approach is no longer available here (it makes the components 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
of an indicator function
can only utilize linear polynomials (as opposed to polynomials of higher degree), and that one can partition
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
. 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 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 are positive reals such that
and
, prove that
.
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 and
imply
:
>>> 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 (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 and positive reals
such that
and
, and the task is to conclude that
:
>>> 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.
This post was inspired by some recent discussions with Bjoern Bringmann.
Symbolic math software packages are highly developed for many mathematical tasks in areas such as algebra, calculus, and numerical analysis. However, to my knowledge we do not have similarly sophisticated tools for verifying asymptotic estimates – inequalities that are supposed to hold for arbitrarily large parameters, with constant losses. Particularly important are functional estimates, where the parameters involve an unknown function or sequence (living in some suitable function space, such as an space); but for this discussion I will focus on the simpler situation of asymptotic estimates involving a finite number of positive real numbers, combined using arithmetic operations such as addition, multiplication, division, exponentiation, and minimum and maximum (but no subtraction). A typical inequality here might be the weak arithmetic mean-geometric mean inequality
where are arbitrary positive real numbers, and the
here indicates that we are willing to lose an unspecified (multiplicative) constant in the estimates.
I have wished in the past (e.g., in this MathOverflow answer) for a tool that could automatically determine whether such an estimate was true or not (and provide a proof if true, or an asymptotic counterexample if false). In principle, simple inequalities of this form could be automatically resolved by brute force case splitting. For instance, with (1), one first observes that is comparable to
up to constants, so it suffices to determine if
Next, to resolve the maximum, one can divide into three cases: ;
; and
. Suppose for instance that
. Then the estimate to prove simplifies to
and this is (after taking logarithms) a positive linear combination of the hypotheses ,
. The task of determining such a linear combination is a standard linear programming task, for which many computer software packages exist.
Any single such inequality is not too difficult to resolve by hand, but there are applications in which one needs to check a large number of such inequalities, or split into a large number of cases. I will take an example at random from an old paper of mine (adapted from the equation after (51), and ignoring some epsilon terms for simplicity): I wanted to establish the estimate
for any obeying the constraints
where ,
, and
are the maximum, median, and minimum of
respectively, and similarly for
,
, and
, and
. This particular bound could be dispatched in three or four lines from some simpler inequalities; but it took some time to come up with those inequalities, and I had to do a dozen further inequalities of this type. This is a task that seems extremely ripe for automation, particularly with modern technology.
Recently, I have been doing a lot more coding (in Python, mostly) than in the past, aided by the remarkable facility of large language models to generate initial code samples for many different tasks, or to autocomplete partially written code. For the most part, I have restricted myself to fairly simple coding tasks, such as computing and then plotting some mildly complicated mathematical functions, or doing some rudimentary data analysis on some dataset. But I decided to give myself the more challenging task of coding a verifier that could handle inequalities of the above form. After about four hours of coding, with frequent assistance from an LLM, I was able to produce a proof of concept tool for this, which can be found at this Github repository. For instance, to verify (1), the relevant Python code is
a = Variable("a")
b = Variable("b")
c = Variable("c")
assumptions = Assumptions()
assumptions.can_bound((a * b * c) ** (1 / 3), max(a, b, c))
and the (somewhat verbose) output verifying the inequality is
Checking if we can bound (((a * b) * c) ** 0.3333333333333333) by max(a, b, c) from the given axioms.
We will split into the following cases:
[[b <~ a, c <~ a], [a <~ b, c <~ b], [a <~ c, b <~ c]]
Trying case: ([b <~ a, c <~ a],)
Simplify to proving (((a ** 0.6666666666666667) * (b ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1.
Bound was proven true by multiplying the following hypotheses :
b <~ a raised to power 0.33333333
c <~ a raised to power 0.33333333
Trying case: ([a <~ b, c <~ b],)
Simplify to proving (((b ** 0.6666666666666667) * (a ** -0.3333333333333333)) * (c ** -0.3333333333333333)) >= 1.
Bound was proven true by multiplying the following hypotheses :
a <~ b raised to power 0.33333333
c <~ b raised to power 0.33333333
Trying case: ([a <~ c, b <~ c],)
Simplify to proving (((c ** 0.6666666666666667) * (a ** -0.3333333
333333333)) * (b ** -0.3333333333333333)) >= 1.
Bound was proven true by multiplying the following hypotheses :
a <~ c raised to power 0.33333333
b <~ c raised to power 0.33333333
Bound was proven true in all cases!
This is of course an extremely inelegant proof, but elegance is not the point here; rather, that it is automated. (See also this recent article of Heather Macbeth for how proof writing styles change in the presence of automated tools, such as formal proof assistants.)
The code is close to also being able to handle more complicated estimates such as (3); right now I have not written code to properly handle hypotheses such as that involve complex expressions such as
, as opposed to hypotheses that only involve atomic variables such as
,
, but I can at least handle such complex expressions in the left and right-hand sides of the estimate I am trying to verify.
In any event, the code, being a mixture of LLM-generated code and my own rudimentary Python skills, is hardly an exemplar of efficient or elegant coding, and I am sure that there are many expert programmers who could do a much better job. But I think this is proof of concept that a more sophisticated tool of this form could be quite readily created to do more advanced tasks. One such example task was the one I gave in the above MathOverflow question, namely being able to automatically verify a claim such as
for all . Another task would be to automatically verify the ability to estimate some multilinear expression of various functions, in terms of norms of such functions in standard spaces such as Sobolev spaces; this is a task that is particularly prevalent in PDE and harmonic analysis (and can frankly get somewhat tedious to do by hand). As speculated in that MO post, one could eventually hope to also utilize AI to assist in the verification process, for instance by suggesting possible splittings of the various sums or integrals involved, but that would be a long-term objective.
This sort of software development would likely best be performed as a collaborative project, involving both mathematicians and expert programmers. I would be interested to receive advice on how best to proceed with such a project (for instance, would it make sense to incorporate such a tool into an existing platform such as SageMATH), and what features for a general estimate verifier would be most desirable for mathematicians. One thing on my wishlist is the ability to give a tool an expression to estimate (such as a multilinear integral of some unknown functions), as well as a fixed set of tools to bound that integral (e.g., splitting the integral into pieces, integrating by parts, using the Hölder and Sobolev inequalities, etc.), and have the computer do its best to optimize the bound it can produce with those tools (complete with some independently verifiable proof certificate for its output). One could also imagine such tools having the option to output their proof certificates in a formal proof assistant language such as Lean. But perhaps there are other useful features that readers may wish to propose.
A basic type of problem that occurs throughout mathematics is the lifting problem: given some space that “sits above” some other “base” space
due to a projection map
, and some map
from a third space
into the base space
, find a “lift”
of
to
, that is to say a map
such that
. In many applications we would like to have
preserve many of the properties of
(e.g., continuity, differentiability, linearity, etc.).
Of course, if the projection map is not surjective, one would not expect the lifting problem to be solvable in general, as the map
to be lifted could simply take values outside of the range of
. So it is natural to impose the requirement that
be surjective, giving the following commutative diagram to complete:
If no further requirements are placed on the lift , then the axiom of choice is precisely the assertion that the lifting problem is always solvable (once we require
to be surjective). Indeed, the axiom of choice lets us select a preimage
in the fiber of each point
, and one can lift any
by setting
. Conversely, to build a choice function for a surjective map
, it suffices to lift the identity map
to
.
Of course, the maps provided by the axiom of choice are famously pathological, being almost certain to be discontinuous, non-measurable, etc.. So now suppose that all spaces involved are topological spaces, and all maps involved are required to be continuous. Then the lifting problem is not always solvable. For instance, we have a continuous projection from
to
, but the identity map
cannot be lifted continuously up to
, because
is contractable and
is not.
However, if is a discrete space (every set is open), then the axiom of choice lets us solve the continuous lifting problem from
for any continuous surjection
, simply because every map from
to
is continuous. Conversely, the discrete spaces are the only ones with this property: if
is a topological space which is not discrete, then if one lets
be the same space
equipped with the discrete topology, then the only way one can continuously lift the identity map
through the “projection map”
(that maps each point to itself) is if
is itself discrete.
These discrete spaces are the projective objects in the category of topological spaces, since in this category the concept of an epimorphism agrees with that of a surjective continuous map. Thus can be viewed as the unique (up to isomorphism) projective object in this category that has a bijective continuous map to
.
Now let us narrow the category of topological spaces to the category of compact Hausdorff (CH) spaces. Here things should be better behaved; for instance, it is a standard fact in this category that continuous bijections are homeomorphisms, and it is still the case that the epimorphisms are the continuous surjections. So we have a usable notion of a projective object in this category: CH spaces such that any continuous map
into another CH space can be lifted via any surjective continuous map
to another CH space.
By the previous discussion, discrete CH spaces will be projective, but this is an extremely restrictive set of examples, since of course compact discrete spaces must be finite. Are there any others? The answer was worked out by Gleason:
Proposition 1 A compact Hausdorff spaceis projective if and only if it is extremally disconnected, i.e., the closure of every open set is again open.
Proof: We begin with the “only if” direction. Let was projective, and let
be an open subset of
. Then the closure
and complement
are both closed, hence compact, subsets of
, so the disjoint union
is another CH space, which has an obvious surjective continuous projection map
to
formed by gluing the two inclusion maps together. As
is projective, the identity map
must then lift to a continuous map
. One easily checks that
has to map
to the first component
of the disjoint union, and
ot the second component; hence
, and so
is open, giving extremal disconnectedness.
Conversely, suppose that is extremally disconnected, that
is a continuous surjection of CH spaces, and
is continuous. We wish to lift
to a continuous map
.
We first observe that it suffices to solve the lifting problem for the identity map , that is to say we can assume without loss of generality that
and
is the identity. Indeed, for general maps
, one can introduce the pullback space
So now we are trying to lift the identity map via a continuous surjection
. Let us call this surjection
minimally surjective if no restriction
of
to a proper closed subset
of
remains surjective. An easy application of Zorn’s lemma shows that every continuous surjection
can be restricted to a minimally surjective continuous map
. Thus, without loss of generality, we may assume that
is minimally surjective.
The key claim now is that every minimally surjective map into an extremally disconnected space is in fact a bijection. Indeed, suppose for contradiction that there were two distinct points
in
that mapped to the same point
under
. By taking contrapositives of the minimal surjectivity property, we see that every open neighborhood of
must contain at least one fiber
of
, and by shrinking this neighborhood one can ensure the base point is arbitrarily close to
. Thus, every open neighborhood of
must intersect every open neighborhood of
, contradicting the Hausdorff property.
It is well known that continuous bijections between CH spaces must be homeomorphisms (they map compact sets to compact sets, hence must be open maps). So is a homeomorphism, and one can lift the identity map to the inverse map
.
Remark 2 The property of being “minimally surjective” sounds like it should have a purely category-theoretic definition, but I was unable to match this concept to a standard term in category theory (something along the lines of a “minimal epimorphism”, I would imagine).
In view of this proposition, it is now natural to look for extremally disconnected CH spaces (also known as Stonean spaces). The discrete CH spaces are one class of such spaces, but they are all finite. Unfortunately, these are the only “small” examples:
Lemma 3 Any first countable extremally disconnected CH spaceis discrete.
Proof: If such a space were not discrete, one could find a sequence
in
converging to a limit
such that
for all
. One can sparsify the elements
to all be distinct, and from the Hausdorff property one can construct neighbourhoods
of each
that avoid
, and are disjoint from each other. Then
and then
are disjoint open sets that both have
as an adherent point, which is inconsistent with extremal disconnectedness: the closure of
contains
but is disjoint from
, so cannot be open.
Thus for instance there are no extremally disconnected compact metric spaces, other than the finite spaces; for instance, the Cantor space is not extremally disconnected, even though it is totally disconnected (which one can easily see to be a property implied by extremal disconnectedness). On the other hand, once we leave the first-countable world, we have plenty of such spaces:
Lemma 4 Letbe a complete Boolean algebra. Then the Stone dual
of
(i.e., the space of boolean homomorphisms
) is an extremally disconnected CH space.
Proof: The CH properties are standard. The elements of
give a basis of the topology given by the clopen sets
. Because the Boolean algebra is complete, we see that the closure of the open set
for any family
of sets is simply the clopen set
, which obviously open, giving extremal disconnectedness.
Remark 5 In fact, every extremally disconnected CH spaceis homeomorphic to a Stone dual of a complete Boolean algebra (and specifically, the clopen algebra of
); see Gleason’s paper.
Corollary 6 Every CH spaceis the surjective continuous image of an extremally disconnected CH space.
Proof: Take the Stone-Čech compactification of
equipped with the discrete topology, or equivalently the Stone dual of the power set
(i.e., the ultrafilters on
). By the previous lemma, this is an extremally disconnected CH space. Because every ultrafilter on a CH space has a unique limit, we have a canonical map from
to
, which one can easily check to be continuous and surjective.
Remark 7 In fact, to each CH spaceone can associate an extremally disconnected CH space
with a minimally surjective continuous map
. The construction is the same, but instead of working with the entire power set
, one works with the smaller (but still complete) Boolean algebra of domains – closed subsets of
which are the closure of their interior, ordered by inclusion. This
is unique up to homoeomorphism, and is thus a canonical choice of extremally disconnected space to project onto
. See the paper of Gleason for details.
Several facts in analysis concerning CH spaces can be made easier to prove by utilizing Corollary 6 and working first in extremally disconnected spaces, where some things become simpler. My vague understanding is that this is highly compatible with the modern perspective of condensed mathematics, although I am not an expert in this area. Here, I will just give a classic example of this philosophy, due to Garling and presented in this paper of Hartig:
Theorem 8 (Riesz representation theorem) Letbe a CH space, and let
be a bounded linear functional. Then there is a (unique) Radon measure
on
(on the Baire
-algebra, generated by
) such
for all
.
Uniqueness of the measure is relatively straightforward; the difficult task is existence, and most known proofs are somewhat complicated. But one can observe that the theorem “pushes forward” under surjective maps:
Proposition 9 Supposeis a continuous surjection between CH spaces. If the Riesz representation theorem is true for
, then it is also true for
.
Proof: As is surjective, the pullback map
is an isometry, hence every bounded linear functional on
can be viewed as a bounded linear functional on a subspace of
, and hence by the Hahn–Banach theorem it extends to a bounded linear functional on
. By the Riesz representation theorem on
, this latter functional can be represented as an integral against a Radon measure
on
. One can then check that the pushforward measure
is then a Radon measure on
, and gives the desired representation of the bounded linear functional on
.
In view of this proposition and Corollary 6, it suffices to prove the Riesz representation theorem for extremally disconnected CH spaces. But this is easy:
Proposition 10 The Riesz representation theorem is true for extremally disconnected CH spaces.
Proof: The Baire -algebra is generated by the Boolean algebra of clopen sets. A functional
induces a finitely additive measure
on this algebra by the formula
. This is in fact a premeasure, because by compactness the only way to partition a clopen set into countably many clopen sets is to have only finitely many of the latter sets non-empty. By the Carathéodory extension theorem,
then extends to a Baire measure, which one can check to be a Radon measure that represents
(the finite linear combinations of indicators of clopen sets are dense in
).
There has been some spectacular progress in geometric measure theory: Hong Wang and Joshua Zahl have just released a preprint that resolves the three-dimensional case of the infamous Kakeya set conjecture! This conjecture asserts that a Kakeya set – a subset of that contains a unit line segment in every direction, must have Minkowski and Hausdorff dimension equal to three. (There is also a stronger “maximal function” version of this conjecture that remains open at present, although the methods of this paper will give some non-trivial bounds on this maximal function.) It is common to discretize this conjecture in terms of small scale
. Roughly speaking, the conjecture then asserts that if one has a family
of
tubes of cardinality
, and pointing in a
-separated set of directions, then the union
of these tubes should have volume
. Here we shall be a little vague as to what
means here, but roughly one should think of this as “up to factors of the form
for any
“; in particular this notation can absorb any logarithmic losses that might arise for instance from a dyadic pigeonholing argument. For technical reasons (including the need to invoke the aforementioned dyadic pigeonholing), one actually works with slightly smaller sets
, where
is a “shading” of the tubes in
that assigns a large subset
of
to each tube
in the collection; but for this discussion we shall ignore this subtlety and pretend that we can always work with the full tubes.
Previous results in this area tended to center around lower bounds of the form , that one would like to make as large as possible. For instance, just from considering a single tube in this collection, one can easily establish (1) with
. By just using the fact that two lines in
intersect in a point (or more precisely, a more quantitative estimate on the volume between the intersection of two
tubes, based on the angle of intersection), combined with a now classical
-based argument of Córdoba, one can obtain (1) with
(and this type of argument also resolves the Kakeya conjecture in two dimensions). In 1995, building on earlier work by Bourgain, Wolff famously obtained (1) with
using what is now known as the “Wolff hairbrush argument”, based on considering the size of a “hairbrush” – the union of all the tubes that pass through a single tube (the hairbrush “stem”) in the collection.
In their new paper, Wang and Zahl established (1) for . The proof is lengthy (127 pages!), and relies crucially on their previous paper establishing a key “sticky” case of the conjecture. Here, I thought I would try to summarize the high level strategy of proof, omitting many details and also oversimplifying the argument at various places for sake of exposition. The argument does use many ideas from previous literature, including some from my own papers with co-authors; but the case analysis and iterative schemes required are remarkably sophisticated and delicate, with multiple new ideas needed to close the full argument.
A natural strategy to prove (1) would be to try to induct on : if we let
represent the assertion that (1) holds for all configurations of
tubes of dimensions
, with
-separated directions, we could try to prove some implication of the form
for all
, where
is some small positive quantity depending on
. Iterating this, one could hope to get
arbitrarily close to
.
A general principle with these sorts of continuous induction arguments is to first obtain the trivial implication in a non-trivial fashion, with the hope that this non-trivial argument can somehow be perturbed or optimized to get the crucial improvement
. The standard strategy for doing this, since the work of Bourgain and then Wolff in the 1990s (with precursors in older work of Córdoba), is to perform some sort of “induction on scales”. Here is the basic idea. Let us call the
tubes
in
“thin tubes”. We can try to group these thin tubes into “fat tubes” of dimension
for some intermediate scale
; it is not terribly important for this sketch precisely what intermediate value is chosen here, but one could for instance set
if desired. Because of the
-separated nature of the directions in
, there can only be at most
thin tubes in a given fat tube, and so we need at least
fat tubes to cover the
thin tubes. Let us suppose for now that we are in the “sticky” case where the thin tubes stick together inside fat tubes as much as possible, so that there are in fact a collection
of
fat tubes
, with each fat tube containing about
of the thin tubes. Let us also assume that the fat tubes
are
-separated in direction, which is an assumption which is highly consistent with the other assumptions made here.
If we already have the hypothesis , then by applying it at scale
instead of
we conclude a lower bound on the volume occupied by fat tubes:
Now, inside each fat tube , we are assuming that we have about
thin tubes that are
-separated in direction. If we perform a linear rescaling around the axis of the fat tube by a factor of
to turn it into a
tube, this would inflate the thin tubes to be rescaled tubes of dimensions
, which would now be
-separated in direction. This rescaling does not affect the multiplicity of the tubes. Applying
again, we see morally that the multiplicity
of the rescaled tubes, and hence the thin tubes inside
, should be
.
We now observe that the multiplicity of the full collection
of thin tubes should morally obey the inequality
fat tubes, and within each fat tube a given point lies in at most
thin tubes in that fat tube, then it should only be able to lie in at most
tubes overall. This heuristically gives
, which then recovers (1) in the sticky case.
In their previous paper, Wang and Zahl were roughly able to squeeze a little bit more out of this argument to get something resembling in the sticky case, loosely following a strategy of Nets Katz and myself that I discussed in this previous blog post from over a decade ago. I will not discuss this portion of the argument further here, referring the reader to the introduction to that paper; instead, I will focus on the arguments in the current paper, which handle the non-sticky case.
Let’s try to repeat the above analysis in a non-sticky situation. We assume (or some suitable variant thereof), and consider some thickened Kakeya set
A typical non-sticky setup is when there are now fat tubes for some multiplicity
(e.g.,
for some small constant
), with each fat tube containing only
thin tubes. Now we have an unfortunate imbalance: the fat tubes form a “super-Kakeya configuration”, with too many tubes at the coarse scale
for them to be all
-separated in direction, while the thin tubes inside a fat tube form a “sub-Kakeya configuration” in which there are not enough tubes to cover all relevant directions. So one cannot apply the hypothesis
efficiently at either scale.
This looks like a serious obstacle, so let’s change tack for a bit and think of a different way to try to close the argument. Let’s look at how intersects a given
-ball
. The hypothesis
suggests that
might behave like a
-dimensional fractal (thickened at scale
), in which case one might be led to a predicted size of
of the form
. Suppose for sake of argument that the set
was denser than this at this scale, for instance we have
and some
. Observe that the
-neighborhood
is basically
, and thus has volume
by the hypothesis
(indeed we would even expect some gain in
, but we do not attempt to capture such a gain for now). Since
-balls have volume
, this should imply that
needs about
balls to cover it. Applying (3), we then heuristically have
The set , being the union of tubes of thickness
, is essentially the union of
cubes. But it has been observed in several previous works (starting with a paper of Nets Katz, Izabella Laba, and myself) that these Kakeya type sets tend to organize themselves into larger “grains” than these cubes – in particular, they can organize into
disjoint prisms (or “grains”) in various orientations for some intermediate scales
. The original “graininess” argument of Nets, Izabella and myself required a stickiness hypothesis which we are explicitly not assuming (and also an “x-ray estimate”, though Wang and Zahl were able to find a suitable substitute for this), so is not directly available for this argument; however, there is an alternate approach to graininess developed by Guth, based on the polynomial method, that can be adapted to this setting. (I am told that Guth has a way to obtain this graininess reduction for this paper without invoking the polynomial method, but I have not studied the details.) With rescaling, we can ensure that the thin tubes inside a single fat tube
will organize into grains of a rescaled dimension
. The grains associated to a single fat tube will be essentially disjoint; but there can be overlap between grains from different fat tubes.
The exact dimensions of the grains are not specified in advance; the argument of Guth will show that
is significantly larger than
, but other than that there are no bounds. But in principle we should be able to assume without loss of generality that the grains are as “large” as possible. This means that there are no longer grains of dimensions
with
much larger than
; and for fixed
, there are no wider grains of dimensions
with
much larger than
.
One somewhat degenerate possibility is that there are enormous grains of dimensions approximately (i.e.,
), so that the Kakeya set
becomes more like a union of planar slabs. Here, it turns out that the classical
arguments of Córdoba give good estimates, so this turns out to be a relatively easy case. So we can assume that least one of
or
is small (or both).
We now revisit the multiplicity inequality (2). There is something slightly wasteful about this inequality, because the fat tubes used to define occupy a lot of space that is not in
. An improved inequality here is
is the multiplicity, not of the fat tubes
, but rather of the smaller set
. The point here is that by the graininess hypotheses, each
is the union of essentially disjoint grains of some intermediate dimensions
. So the quantity
is basically measuring the multiplicity of the grains.
It turns out that after a suitable rescaling, the arrangement of grains looks locally like an arrangement of tubes. If one is lucky, these tubes will look like a Kakeya (or sub-Kakeya) configuration, for instance with not too many tubes in a given direction. (More precisely, one should assume here some form of the Wolff axioms, which the authors refer to as the “Katz-Tao Convex Wolff axioms”). A suitable version if the hypothesis
will then give the bound
So the remaining case is when the grains do not behave like a rescaled Kakeya or sub-Kakeya configuration. Wang and Zahl introduce a “structure theorem” to analyze this case, concluding that the grains will organize into some larger convex prisms , with the grains in each prism
behaving like a “super-Kakeya configuration” (with significantly more grains than one would have for a Kakeya configuration). However, the precise dimensions of these prisms
is not specified in advance, and one has to split into further cases.
One case is when the prisms are “thick”, in that all dimensions are significantly greater than
. Informally, this means that at small scales,
looks like a super-Kakeya configuration after rescaling. With a somewhat lengthy induction on scales argument, Wang and Zahl are able to show that (a suitable version of)
implies an “x-ray” version of itself, in which the lower bound of super-Kakeya configurations is noticeably better than the lower bound for Kakeya configurations. The upshot of this is that one is able to obtain a Frostman violation bound of the form (3) in this case, which as discussed previously is already enough to win in this case.
It remains to handle the case when the prisms are “thin”, in that they have thickness
. In this case, it turns out that the
arguments of Córdoba, combined with the super-Kakeya nature of the grains inside each of these thin prisms, implies that each prism is almost completely occupied by the set
. In effect, this means that these prisms
themselves can be taken to be grains of the Kakeya set. But this turns out to contradict the maximality of the dimensions of the grains (if everything is set up properly). This treats the last remaining case needed to close the induction on scales, and obtain the Kakeya conjecture!


Recent Comments