The equational theories project: a brief tour

Almost three weeks ago, I proposed a collaborative project, combining the efforts of professional and amateur mathematicians, automatic theorem provers, AI tools, and the proof assistant language Lean, to describe the implication graph relating the 4694 equational laws for magmas that can be expressed using up to four invocations of the magma operation. That is to say, one needs to determine the truth or falsity of the {4694*(4694-1)=22028942} possible implications between the these 4694 laws.

The project was launched on the day of the blog post, and has been running for a hectic 19 days thus far; see my personal log of the project for a day-by-day summary of events. From the perspective of raw implications resolved, the project is (of the time of writing) 99.9963% complete: of the {22028942} implications to resolve, {8178279} have been proven to be true, {13854531} have been proven to be false, and only {826} remain open, although even within this set, there are {249} implications that we conjecture to be false and for which we are likely to be able to formally disprove soon. For reasons of compilation efficiency, we do not record the proof of every single one of these assertions in Lean; we only prove a smaller set of {592790} implications in Lean, which then imply the broader set of implications through transitivity (for instance, using the fact that if Equation {X} implies Equation {Y} and Equation {Y} implies Equation {Z}, then Equation {X} implies Equation {Z}); we will also shortly implement a further reduction utilizing a duality symmetry of the implication graph.

Thanks to the tireless efforts of many volunteer contributors to the project, we now have a number of nice visualization tools to inspect various portions of the (not quite completed) implication graph. For instance, this graph depicts all the consequences of Equation 1491: {x = (y \diamond x) \diamond (y \diamond (y \diamond x))}, which I have nicknamed the “Obelix law” (and it has a companion, the “Asterix law“, Equation 65: {x = (y \diamond (x \diamond (y \diamond x)))}). And here is a table of all the equational laws we are studying, together with a count of how many laws they imply, or are implied by. These interfaces are also somewhat integrated with Lean: for instance, you can click here to try your hand at showing that the Obelix law implies Equation 359, {x \diamond x = (x \diamond x) \diamond x}; I’ll leave this as a challenge (a four-line proof in Lean is possible).

Over the last few weeks, I’ve learned that many of these laws have previously appeared in the literature, and compiled a “tour” of these equations here. For instance, in addition to the very well known commutative law (Equation 43) and associative law (Equation 4512), some equations (Equation 14, Equation 29, Equation 381, Equation 3722, and Equation 3744) appeared in some Putnam math competitions; Equation 168 defines a fascinating structure, known as a “central groupoid”, that was studied in particular by Evans and by Knuth, and was a key inspiration for the Knuth-Bendix completion algorithm; and Equation 1571 classifies abelian groups of exponent two.

Thanks to the Birkhoff completeness theorem, if one equational law implies another, then it can be proven by a finite number of rewrite operations; however the number of rewrites needed could be quite lengthy. The implication of 359 from 1491 mentioned above is already moderately challenging, requiring four or five rewrites; the implication of Equation 2 from Equation 1689 is incredibly long (try it!). Nevertheless, standard automated theorem provers, such as Vampire, are quite capable of proving the vast majority of these implications.

More subtle are the anti-implications, in which we have to show that a law {X} does not imply a law {Y}. In principle, one just has to exhibit a magma that obeys {X} but not {Y}. In a large fraction of cases, one can simply search through small finite magmas – such as magmas on two, three, or four elements – to obtain this anti-implication; but they do not always suffice, and in fact we know of anti-implications that can only be proven through a construction of an infinite magma. For instance, the “Asterix law” is now known (from the efforts of this project) to not imply the “Obelix law”, but all counterexamples are necessarily infinite. Curiously, the known constructions have some affinity with the famous technique of forcing in set theory, in that we continually add “generic” elements to a (partial) magma in order to force a counterexample with certain specified properties to exist, though the constructions here are certainly far simpler than in the set-theoretic constructions.

We have also obtained profitable mileage out of constructions of “linear” magmas {x \diamond y = ax + by} in both commutative and non-commutative rings; free magmas associated to “confluent” equational laws, and more generally laws with complete rewriting systems. As such, the number of unresolved implications continues to shrink at a steady pace, although we are not yet ready to declare victory on the project.

After quite hectic amount of back end setup and “putting out fires”, the project is now running fairly smoothly, with activity coordinated on a Lean Zulip channel, and all contributions going through a pull request process on Github, and tracked via an issues-based Github project with the invaluable oversight provided by the other two maintainers of the project, Pietro Monticone and Shreyas Srinivas. In contrast to the prior PFR formalization project, the workflow follows standard Github practices and proceeds roughly as follows: if, during the course of the Zulip discussion, it becomes clear that some specific task needs to be done to move the project forward (e.g., to formalize in Lean the proof of an implication that had been worked out in the discussion threads), an “issue” is made (often by myself or one of the other maintainers), which other contributors can then “claim”, work on separately (using a local copy of the main Github repository), and then submit a “pull request” to merge their contribution back into the main repository. This request can then be reviewed by both maintainers and other contributors, and if approved, closes the relevant issue.

More generally, we are trying to document all of the processes and lessons learned from this setup, and this will be part of a forthcoming paper on this project, which we are now in the preliminary stages of planning, and will likely include dozens of authors.

While the project is still ongoing, I can say that I am quite satisfied with the progress accomplished to date, and that many of my hopes for such a project have already been realized. On the scientific side, we have discovered some new techniques and constructions to show that a given equational theory does not imply another one, and have also discovered some exotic algebraic structures, such as the “Asterix” and “Obelix” pair, that have interesting features, and which would likely not have been discovered by any means other than the type of systematic search conducted here. The participants are very diverse, ranging from mathematicians and computer scientists at all stages of career, to interested students and amateurs. The Lean platform has worked well in integrating both human-generated and machine-generated contributions; the latter are numerically by far the largest source of contributions, but many of the automatically generated results were first obtained in special cases by humans, and then generalized and formalized (often by different members of the project). We still make many informal mathematical arguments on the discussion thread, but they tend to be rapidly formalized in Lean, at which point disputes about correctness disappear, and we can instead focus on how best to deploy various verified techniques to tackle the remaining implications.

Perhaps the only thing that I was expecting to see at this point that has not yet materialized is significant contributions from modern AI tools. They are being used in a number of secondary ways in this project, for instance through tools such as Github copilot to speed up the writing of Lean proofs, the LaTeX blueprint, and other software code, and several of our visualization tools were also largely co-written using large language models such as Claude. However, for the core task of resolving implications, the more “good old-fashioned” automated theorem provers have so far proven superior. However, most of the remaining 700 or so implications are not amenable to these older tools, and several (particularly the ones involving “Asterix” and “Obelix” had stymied the human collaborators for several days), so I can still see a role for modern AI to play a more active role in finishing off the hardest and most stubborn of the remaining implications.

A pilot project in universal algebra to explore new ways to collaborate and use machine assistance?

Traditionally, mathematics research projects are conducted by a small number (typically one to five) of expert mathematicians, each of which are familiar enough with all aspects of the project that they can verify each other’s contributions. It has been challenging to organize mathematical projects at larger scales, and particularly those that involve contributions from the general public, due to the need to verify all of the contributions; a single error in one component of a mathematical argument could invalidate the entire project. Furthermore, the sophistication of a typical math project is such that it would not be realistic to expect a member of the public, with say an undergraduate level of mathematics education, to contribute in a meaningful way to many such projects.

For related reasons, it is also challenging to incorporate assistance from modern AI tools into a research project, as these tools can “hallucinate” plausible-looking, but nonsensical arguments, which therefore need additional verification before they could be added into the project.

Proof assistant languages, such as Lean, provide a potential way to overcome these obstacles, and allow for large-scale collaborations involving professional mathematicians, the broader public, and/or AI tools to all contribute to a complex project, provided that it can be broken up in a modular fashion into smaller pieces that can be attacked without necessarily understanding all aspects of the project as a whole. Projects to formalize an existing mathematical result (such as the formalization of the recent proof of the PFR conjecture of Marton, discussed in this previous blog post) are currently the main examples of such large-scale collaborations that are enabled via proof assistants. At present, these formalizations are mostly crowdsourced by human contributors (which include both professional mathematicians and interested members of the general public), but there are also some nascent efforts to incorporate more automated tools (either “good old-fashioned” automated theorem provers, or more modern AI-based tools) to assist with the (still quite tedious) task of formalization.

However, I believe that this sort of paradigm can also be used to explore new mathematics, as opposed to formalizing existing mathematics. The online collaborative “Polymath” projects that several people including myself organized in the past are one example of this; but as they did not incorporate proof assistants into the workflow, the contributions had to be managed and verified by the human moderators of the project, which was quite a time-consuming responsibility, and one which limited the ability to scale these projects up further. But I am hoping that the addition of proof assistants will remove this bottleneck.

I am particularly interested in the possibility of using these modern tools to explore a class of many mathematical problems at once, as opposed to the current approach of focusing on only one or two problems at a time. This seems like an inherently modularizable and repetitive task, which could particularly benefit from both crowdsourcing and automated tools, if given the right platform to rigorously coordinate all the contributions; and it is a type of mathematics that previous methods usually could not scale up to (except perhaps over a period of many years, as individual papers slowly explore the class one data point at a time until a reasonable intuition about the class is attained). Among other things, having a large data set of problems to work on could be helpful for benchmarking various automated tools and compare the efficacy of different workflows.

One recent example of such a project was the Busy Beaver Challenge, which showed this July that the fifth Busy Beaver number {BB(5)} was equal to {47176870}. Some older crowdsourced computational projects, such as the Great Internet Mersenne Prime Search (GIMPS), are also somewhat similar in spirit to this type of project (though using more traditional proof of work certificates instead of proof assistants). I would be interested in hearing of any other extant examples of crowdsourced projects exploring a mathematical space, and whether there are lessons from those examples that could be relevant for the project I propose here.

More specifically I would like to propose the following (admittedly artificial) project as a pilot to further test out this paradigm, which was inspired by a MathOverflow question from last year, and discussed somewhat further on my Mastodon account shortly afterwards.

The problem is in the field of universal algebra, and concerns the (medium-scale) exploration of simple equational theories for magmas. A magma is nothing more than a set {G} equipped with a binary operation {\circ: G \times G \rightarrow G}. Initially, no additional axioms on this operation {\circ} are imposed, and as such magmas by themselves are somewhat boring objects. Of course, with additional axioms, such as the identity axiom or the associative axiom, one can get more familiar mathematical objects such as groups, semigroups, or monoids. Here we will be interested in (constant-free) equational axioms, which are axioms of equality involving expressions built from the operation {\circ} and one or more indeterminate variables in {G}. Two familiar examples of such axioms are the commutative axiom

\displaystyle  x \circ y = y \circ x

and the associative axiom

\displaystyle  (x \circ y) \circ z = x \circ (y \circ z),

where {x,y,z} are indeterminate variables in the magma {G}. On the other hand the (left) identity axiom {e \circ x = x} would not be considered an equational axiom here, as it involves a constant {e \in G} (the identity element), which we will not consider here.

To illustrate the project I have in mind, let me first introduce eleven examples of equational axioms for magmas:

  • Equation1: {x=y}
  • Equation2: {x \circ y = z \circ w}
  • Equation3: {x \circ y = x}
  • Equation4: {(x \circ x) \circ y = y \circ x}
  • Equation5: {x \circ (y \circ z) = (w \circ u) \circ v}
  • Equation6: {x \circ y = x \circ z}
  • Equation7: {x \circ y = y \circ x}
  • Equation8: {x \circ (y \circ z) = (x \circ w) \circ u}
  • Equation9: {x \circ (y \circ z) = (x \circ y) \circ w}
  • Equation10: {x \circ (y \circ z) = (x \circ y) \circ z}
  • Equation11: {x = x}
Thus, for instance, Equation7 is the commutative axiom, and Equation10 is the associative axiom. The constant axiom Equation1 is the strongest, as it forces the magma {G} to have at most one element; at the opposite extreme, the reflexive axiom Equation11 is the weakest, being satisfied by every single magma.

One can then ask which axioms imply which others. For instance, Equation1 implies all the other axioms in this list, which in turn imply Equation11. Equation8 implies Equation9 as a special case, which in turn implies Equation10 as a special case. The full poset of implications can be depicted by the following Hasse diagram:

This in particular answers the MathOverflow question of whether there were equational axioms intermediate between the constant axiom Equation1 and the associative axiom Equation10.

Most of the implications here are quite easy to prove, but there is one non-trivial one, obtained in this answer to a MathOverflow post closely related to the preceding one:

Proposition 1 Equation4 implies Equation7.

Proof: Suppose that {G} obeys Equation4, thus

\displaystyle  (x \circ x) \circ y = y \circ x \ \ \ \ \ (1)

for all {x,y \in G}. Specializing to {y=x \circ x}, we conclude

\displaystyle (x \circ x) \circ (x \circ x) = (x \circ x) \circ x

and hence by another application of (1) we see that {x \circ x} is idempotent:

\displaystyle  (x \circ x) \circ (x \circ x) = x \circ x. \ \ \ \ \ (2)

Now, replacing {x} by {x \circ x} in (1) and then using (2), we see that

\displaystyle  (x \circ x) \circ y = y \circ (x \circ x),

so in particular {x \circ x} commutes with {y \circ y}:

\displaystyle  (x \circ x) \circ (y \circ y) = (y \circ y) \circ (x \circ x). \ \ \ \ \ (3)

Also, from two applications (1) one has

\displaystyle  (x \circ x) \circ (y \circ y) = (y \circ y) \circ x = x \circ y.

Thus (3) simplifies to {x \circ y = y \circ x}, which is Equation7. \Box

A formalization of the above argument in Lean can be found here.

I will remark that the general question of determining whether one set of equational axioms determines another is undecidable; see Theorem 14 of this paper of Perkins. (This is similar in spirit to the more well known undecidability of various word problems.) So, the situation here is somewhat similar to the Busy Beaver Challenge, in that past a certain point of complexity, we would necessarily encounter unsolvable problems; but hopefully there would be interesting problems and phenomena to discover before we reach that threshold.

The above Hasse diagram does not just assert implications between the listed equational axioms; it also asserts non-implications between the axioms. For instance, as seen in the diagram, the commutative axiom Equation7 does not imply the Equation4 axiom

\displaystyle  (x+x)+y = y + x.

To see this, one simply has to produce an example of a magma that obeys the commutative axiom Equation7, but not the Equation4 axiom; but in this case one can simply choose (for instance) the natural numbers {{\bf N}} with the addition operation {x \circ y := x+y}. More generally, the diagram asserts the following non-implications, which (together with the indicated implications) completely describes the poset of implications between the eleven axioms:
  • Equation2 does not imply Equation3.
  • Equation3 does not imply Equation5.
  • Equation3 does not imply Equation7.
  • Equation5 does not imply Equation6.
  • Equation5 does not imply Equation7.
  • Equation6 does not imply Equation7.
  • Equation6 does not imply Equation10.
  • Equation7 does not imply Equation6.
  • Equation7 does not imply Equation10.
  • Equation9 does not imply Equation8.
  • Equation10 does not imply Equation9.
  • Equation10 does not imply Equation6.
The reader is invited to come up with counterexamples that demonstrate some of these implications. The hardest type of counterexamples to find are the ones that show that Equation9 does not imply Equation8: a solution (in Lean) can be found here. I placed proofs in Lean of all the above implications and anti-implications can be found in this github repository file.

As one can see, it is already somewhat tedious to compute the Hasse diagram of just eleven equations. The project I propose is to try to expand this Hasse diagram by a couple orders of magnitude, covering a significantly larger set of equations. The set I propose is the set {{\mathcal E}} of equations that use the magma operation {\circ} at most four times, up to relabeling and the reflexive and symmetric axioms of equality; this includes the eleven equations above, but also many more. How many more? Recall that the Catalan number {C_n} is the number of ways one can form an expression out of {n} applications of a binary operation {\circ} (applied to {n+1} placeholder variables); and, given a string of {m} placeholder variables, the Bell number {B_m} is the number of ways (up to relabeling) to assign names to each of these variables, where some of the placeholders are allowed to be assigned the same name. As a consequence, ignoring symmetry, the number of equations that involve at most four operations is

\displaystyle  \sum_{n,m \geq 0: n+m \leq 4} C_n C_m B_{n+m+2} = 9131.

The number of equations in which the left-hand side and right-hand side are identical is

\displaystyle  \sum_{n=0}^2 C_n B_{n+1} = 1 * 1 + 1 * 2 + 2 * 5 = 13;

these are all equivalent to reflexive axiom (Equation11). The remaining {9118} equations come in pairs by the symmetry of equality, so the total size of {{\mathcal E}} is

\displaystyle  1 + \frac{9118}{2} = 4560.

I have not yet generated the full list of such identities, but presumably this will be straightforward to do in a standard computer language such as Python (I have not tried this, but I imagine some back-and-forth with a modern AI would let one generate most of the required code). [UPDATE, Sep 26: Amir Livne Bar-on has kindly enumerated all the equations, of which there are actually 4694.]

It is not clear to me at all what the geometry of {{\mathcal E}} will look like. Will most equations be incomparable with each other? Will it stratify into layers of “strong” and “weak” axioms? Will there be a lot of equivalent axioms? It might be interesting to record now any speculations as what the structure of this poset, and compare these predictions with the outcome of the project afterwards.

A brute force computation of the poset {{\mathcal E}} would then require {4560 \times (4560-1) = 20789040} comparisons, which looks rather daunting; but of course due to the axioms of a partial order, one could presumably identify the poset by a much smaller number of comparisons. I am thinking that it should be possible to crowdsource the exploration of this poset in the form of submissions to a central repository (such as the github repository I just created) of proofs in Lean of implications or non-implications between various equations, which could be validated in Lean, and also checked against some file recording the current status (true, false, or open) of all the {20789040} comparisons, to avoid redundant effort. Most submissions could be handled automatically, with relatively little human moderation required; and the status of the poset could be updated after each such submission.

I would imagine that there is some “low-hanging fruit” that could establish a large number of implications (or anti-implications) quite easily. For instance, laws such as Equation2 or Equation3 more or less completely describe the binary operation {\circ}, and it should be quite easy to check which of the {4560} laws are implied by either of these two laws. The poset {{\mathcal E}} has a reflection symmetry associated to replacing the binary operator {\circ} by its reflection {\circ^{\mathrm{op}}: (x,y) \mapsto y \circ x}, which in principle cuts down the total work by a factor of about two. Specific examples of magmas, such as the natural numbers with the addition operation, obey some set of equations in {{\mathcal E}} but not others, and so could be used to generate a large number of anti-implications. Some existing automated proving tools for equational logic, such as Prover9 and Mace4 (for obtaining implications and anti-implications respectively), could then be used to handle most of the remaining “easy” cases (though some work may be needed to convert the outputs of such tools into Lean). The remaining “hard” cases could then be targeted by some combination of human contributors and more advanced AI tools.

Perhaps, in analogy with formalization projects, we could have a semi-formal “blueprint” evolving in parallel with the formal Lean component of the project. This way, the project could accept human-written proofs by contributors who do not necessarily have any proficiency in Lean, as well as contributions from automated tools (such as the aforementioned Prover9 and Mace4), whose output is in some other format than Lean. The task of converting these semi-formal proofs into Lean could then be done by other humans or automated tools; in particular I imagine modern AI tools could be particularly valuable for this portion of the workflow. I am not quite sure though if existing blueprint software can scale to handle the large number of individual proofs that would be generated by this project; and as this portion would not be formally verified, a significant amount of human moderation might also be needed here, and this also might not scale properly. Perhaps the semi-formal portion of the project could instead be coordinated on a forum such as this blog, in a similar spirit to past Polymath projects.

It would be nice to be able to integrate such a project with some sort of graph visualization software that can take an incomplete determination of the poset {{\mathcal E}} as input (in which each potential comparison {E \implies E'} in {{\mathcal E}} is marked as either true, false, or open), completes the graph as much as possible using the axioms of partial order, and then presents the partially known poset in a visually appealing way. If anyone knows of such a software package, I would be happy to hear of it in the comments.

Anyway, I would be happy to receive any feedback on this project; in addition to the previous requests, I would be interested in any suggestions for improving the project, as well as gauging whether there is sufficient interest in participating to actually launch it. (I am imagining running it vaguely along the lines of a Polymath project, though perhaps not formally labeled as such.)

UPDATE, Sep 30 2024: The project is up and running (and highly active), with the main page being this Github repository. See also the Lean Zulip chat for some (also very active) discussion on the project.

Pointwise convergence of bilinear polynomial averages over the primes

Ben Krause, Hamed Mousavi, Joni Teräväinen, and I have just uploaded to the arXiv the paper “Pointwise convergence of bilinear polynomial averages over the primes“. This paper builds upon a previous result of Krause, Mirek, and myself, in which we demonstrated the pointwise almost everywhere convergence of the ergodic averages

\displaystyle  \frac{1}{N} \sum_{n=1}^N f(T^n x) g(T^{P(n)} x) \ \ \ \ \ (1)

as {N \rightarrow \infty} and almost all {x \in X}, whenever {(X,T,\mu)} is a measure-preserving system (not necessarily of finite measure), and {f \in L^{p_1}(X,\mu)}, {g \in L^{p_2}(X,\mu)} for some {1 < p_1,p_2 < \infty} with {1/p_1 + 1/p_2 \leq 1}, where {P} is a polynomial with integer coefficients and degree at least two. Here we establish the prime version of this theorem, that is to say we establish the pointwise almost everywhere convergence of the averages

\displaystyle  \frac{1}{\pi(N)} \sum_{p \leq N} f(T^p x) g(T^{P(p)} x)

under the same hypotheses on {(X,T,\mu)}, {f, g}. By standard arguments this is equivalent to the pointwise almost everywhere convergence of the weighted averages

\displaystyle  \frac{1}{N} \sum_{n \leq N} \Lambda(n) f(T^n x) g(T^{P(n)} x) \ \ \ \ \ (2)

where {\Lambda} is the von Mangoldt function. Our argument also borrows from results in a recent paper of Teräväinen, who showed (among other things) that the similar averages

\displaystyle  \frac{1}{N} \sum_{n \leq N} \mu(n) f(T^n x) g(T^{P(n)} x)

converge almost everywhere (quite fast) to zero, at least if {X} is assumed to be finite measure. Here of course {\mu} denotes the Möbius function.

The basic strategy is to try to insert the weight {\Lambda} everywhere in the proof of the convergence of (1) and adapt as needed. The weighted averages are bilinear averages associated to the bilinear symbol

\displaystyle  (\xi_1,\xi_2) \mapsto \frac{1}{N} \sum_{n \leq N} \Lambda(n) e(n \xi_1 + P(n) \xi_2).

In the unweighted case, results from the additive combinatorics theory of Peluse and Prendiville were used to essentially reduce matters to the contribution where {\xi_1,\xi_2} were “major arc”, at which point this symbol could be approximated by a more tractable symbol. Setting aside the Peluse-Prendiville step for now, the first obstacle is that the natural approximation to the symbol does not have sufficiently accurate error bounds if a Siegel zero exists. While one could in principle fix this by adding a Siegel correction term to the approximation, we found it simpler to use the arguments of Teräväinen to essentially replace the von Mangoldt weight {\Lambda} by a “Cramér approximant”

\displaystyle  \Lambda_{\mathrm{Cramer}, w}(n) := \frac{W}{\phi(W)} 1_{(n,W)=1}

where {W = \prod_{p \leq w} p} and {w} is a parameter (we make the quasipolynomial choice {w = \exp(\log^{1/C_0} N)} for a suitable absolute constant {N}). This approximant is then used for most of the argument, with relatively routine changes; for instance, an {L^p} improving estimate needs to be replaced by a weighted analogue that is relatively easy to establish from the unweighted version due to an {L^2} smoothing effect, and a sharp {p}-adic bilinear averaging estimate for large {p} can also be adapted to handle a suitable {p}-adic weight by a minor variant of the arguments. The most tricky step is to obtain a weighted version of the Peluse-Prendiville inverse theorem. Here we encounter the technical problem that the Cramér approximant, despite having many good properties (in particular, it is non-negative and has well-controlled correlations thanks to the fundamental lemma of sieve theory), is not of “Type I”, which turns out to be quite handy when establishing inverse theorems. So for this portion of the argument, we switch from the Cramér approximant to the Heath-Brown approximant

\displaystyle  \Lambda_{\mathrm{HB},Q}(n) := \sum_{q<Q} \frac{\mu(q)}{\phi(q)} c_q(n)

where {c_q(n)} is the Ramanujan sum

\displaystyle  c_q(n) := \sum_{r \in ({\bf Z}/q{\bf Z})^\times} e(-rn/q).

While this approximant is no longer non-negative, it is of Type I, and thus well suited for inverse theory. In our paper we set up some basic comparison theorems between {\Lambda}, {\Lambda_{\mathrm{Cramer},w}}, and {\Lambda_{\mathrm{HB},Q}} in various Gowers uniformity-type norms, which allows us to switch relatively easily between the different weights in practice; hopefully these comparison theorems will be useful in other applications as well.

A possible approach to finite time blowup for the Euler equations

Given a smooth compact Riemannian manifold {M = (M,g)}, the incompressible Euler equations can be written in abstract index notation as

\displaystyle  \partial_t u^\alpha + u^\beta \nabla_\beta u^\alpha = - \nabla^\alpha p

\displaystyle  \nabla_\alpha u^\alpha = 0

where {p: [0,T) \rightarrow C^\infty(M)} is a time-dependent scalar field (representing pressure), and {u: [0,T) \rightarrow \Gamma(TM)} is a time-dependent vector field (representing fluid velocity). Here {\nabla} is the Levi-Civita connection associated to {g}. One can recover {p} from {u} (up to constants), so I will abuse notation and refer to the solution to this system as {u} rather than {(u,p)}. Over the last few years I have been interested in the following conjecture:

Conjecture 1 (Finite time blowup) There exists a manifold {M} and a smooth solution {u} to the Euler equations that blows up at some finite time {T}.

This remains open, however there has been progress on rougher versions of this problem. For instance, there is the well-known result of Elgindi (discussed in this previous post) that when {M = {\bf R}^3} and {\alpha>0} is sufficiently small, there exists a {C^{1,\alpha}} solution {u} to the Euler equations on {{\bf R}^3} that blows up in finite time. There has also been progress in establishing various “universality” properties of the Euler flow on manifolds (which informally state that “fluid computers” are possible); see for instance this recent survey of Cardona, Miranda, and Peralta-Salas. Unfortunately, these “fluid computers” do not combine well with scaling symmetries, and so thus far have not been able to produce (finite energy) blowups.

I have been playing with one approach to this conjecture, which reduces to solving a certain underdetermined system of partial differential equations, and then establishing some stability result for the resulting solution. However, I have not been able to make headway on solving this latter system despite its underdetermined nature; so I thought I would record my partial attempt here in case anyone is interested in pursuing it further (and also to contribute to the practice of sharing unsuccessful attempts to solve a problem, which is still quite infrequently done in our community).

To avoid technicalities let us simplify the problem by adding a forcing term {f: [0,T) \rightarrow \Gamma(TM)}:

\displaystyle  \partial_t u^\alpha + u^\beta \nabla_\beta u^\alpha = - \nabla^\alpha p + f^\alpha

\displaystyle  \nabla_\alpha u^\alpha = 0.

Standard local well-posedness theory (using the vorticity-stream formulation of the Euler equations) tells us that this problem is well-posed if the initial data {u_0} is divergence free and in {C^{1,\alpha}(M)} for some {\alpha>0}, and the forcing term {f} is in {L^1_t C^{1,\alpha}(M)}. We have the following recent result of Córdoba and Martínez-Zoroa, solving a version of the above conjecture in the presence of a reasonably regular forcing term:

Theorem 2 (Finite time blowup for the forced equation) There exists a smooth solution to the forced Euler equations on {{\bf R}^3} that exhibits finite time blowup, in which the forcing term {f} stays uniformly bounded in {C^{1,\alpha}({\bf R}^3)} for any {\alpha < 1/2}.

Roughly speaking, their argument proceeds by a multiscale construction, in which the solution is set up to eventually have some presence at a spatial scale {1/N}, which is conducive to generating an exponential “stretching” of a small forcing term at a much higher spatial scale {1/M}, which one then introduces to then set up the solution for the next scale.

As a model problem, I tried to reproduce this type of result from a more geometric perspective, trying to aim for a more “self-similar” blowup than a “multi-scale” one, in the hope that this latter type of blowup might be more tractable to analyze and eventually resolve Conjecture 1. I didn’t fully succeed; but I think the approach I outline below is in principle feasible.

The manifold I will work on is a cylinder {M = {\bf R} \times N}, where {N = (N,h)} is a smooth compact manifold, and the metric on {M} is just the sum of the standard metric {dx_1^2} on the first coordinate and {h}:

\displaystyle  dg^2 = dx_1^2 + dh^2.

(I have experimented with working with more warped metrics to gain more flexibility, but this seems to only influence lower order terms. However, such tricks may be useful to improve the regularity of the forcing term, or perhaps even to eliminate it entirely.) The idea is to try to create a solution that blows up on a slice {\{0\} \times N} on this cylinder, but stays smooth until the blowup time, and also uniformly smooth away from this slice. As such, one can localize the solution away from this slice, and replace the unbounded component {{\bf R}} of {M} by a compact circle {{\bf R}/L{\bf Z}} for some large {L} if desired. However, I prefer to work with the unbounded component {{\bf R}} here in order to scale in this direction.

If we now use Greek indices to only denote coordinates in the “vertical” coordinate {N}, the velocity field {u} now becomes {(u^1, u^\alpha)}, and the Euler equations now split as

\displaystyle  \partial_t u^1 + u^1 \partial_1 u^1 + u^\beta \nabla_\beta u^1 = - \partial_1 p + f^1

\displaystyle  \partial_t u^\alpha + u^1 \partial_1 u^\alpha + u^\beta \nabla_\beta u^\alpha = - \nabla^\alpha p + f^\alpha

\displaystyle  \partial_1 u^1 + \nabla_\alpha u^\alpha = 0.

If the solution is concentrating in a narrow neighborhood of the slice {\{0\} \times N}, we expect the terms involving {\partial_1} to be quite large, and the terms involving {u_1} to be rather small. This suggests that the {\partial_1 p} pressure term is going to be more significant than the {\nabla^\alpha p} term. We therefore select the forcing term to cancel this term by choosing

\displaystyle  f^1 = 0; f^\alpha = \nabla^\alpha p

leaving us with the simplified equation

\displaystyle  \partial_t u^1 + u^1 \partial_1 u^1 + u^\beta \nabla_\beta u^1 = - \partial_1 p

\displaystyle  \partial_t u^\alpha + u^1 \partial_1 u^\alpha + u^\beta \nabla_\beta u^\alpha = 0

\displaystyle  \partial_1 u^1 + \nabla_\alpha u^\alpha = 0.

The nice thing about this latter equation is that the first equation is basically just a formula for {p} and so can be dropped, leaving us with

\displaystyle  \partial_t u^\alpha + u^1 \partial_1 u^\alpha + u^\beta \nabla_\beta u^\alpha = 0 \ \ \ \ \ (1)

\displaystyle  \partial_1 u^1 + \nabla_\alpha u^\alpha = 0. \ \ \ \ \ (2)

This equation now admits a two-parameter family of scale invariances

\displaystyle  u^1(t,x^1,y) \mapsto \frac{\lambda}{\mu} u^1(t/\mu, x/\lambda,y); u^\alpha(t,x^1,y) \mapsto \frac{1}{\mu} u^1(t/\mu, x/\lambda,x^\alpha)

for {\lambda, \mu > 0}, where we use {y} to ednote the {N} coordinate. It also inherits an energy conservation law from the original Euler equations; the conserved energy is

\displaystyle  \frac{1}{2} \int_{\bf R} \int_N u^\alpha(t,x^1,y) u_\alpha(t,x^1,y)\ dy dx^1

using the metric on {N} to raise and lower the Greek indices.

It is now tempting to try to set up an approximately scale-invariant blowup solution. It seems that the first step in this is to construct a “soliton” type localized steady state solution, that is a solution {u_1 \in C^\infty({\bf R} \times N)}, {u^\alpha : {\bf R} \rightarrow \Gamma(TN)} to the equation

\displaystyle  u^1 \partial_1 u^\alpha + u^\beta \nabla_\beta u^\alpha = 0

\displaystyle  \partial_1 u^1 + \nabla_\alpha u^\alpha = 0.

that decays in the {x_1} variable; one can then hope to do a suitable stability (or instability) analysis of this soliton to perturb it to a blowup solution, as there are many results of this type for other equations that one could use as a model. The energy conservation law does constrain to some extent the nature of the blowup (basically, the two scaling parameters {\mu,\lambda} above become linked by the relation {\mu \sim \lambda^{1/2}}), but does not seem to otherwise prevent such a blowup from occuring.

Analytically, this is not a particularly pleasant equation to try to solve; one can substitute the second equation into the first to obtain a single equation

\displaystyle  -(\partial_1^{-1} \nabla_\beta u^\beta) \partial_1 u^\alpha + u^\beta \nabla_\beta u^\alpha = 0

but the inverse derivative {\partial_1^{-1}} is difficult to work with and seems to create ill-posedness (somewhat reminiscent of the ill-posedness of the Prandtl boundary layer equation).

Nevertheless, one can still attempt to solve this equation by separation of variables. If one makes the ansatz

\displaystyle  u^1(x^1,y) = \frac{1}{1+(x^1)^2} \varphi(y)

\displaystyle  u^\alpha(x^1,y) = \frac{v^\alpha(y) + x^1 w^\alpha(y)}{(1+(x^1)^2)^2}

for some smooth {\varphi \in C^\infty(N)} and {v,w \in \Gamma(TN)}, some calculation shows that the system now reduces to a system purely on {N}:

\displaystyle  \varphi w^\alpha + v^\beta \nabla_\beta v^\alpha = 0

\displaystyle  -2 \varphi v^\alpha + v^\beta \nabla_\beta w^\alpha + w^\beta \nabla_\beta v^\alpha = 0

\displaystyle  -3 \varphi w^\alpha + w^\beta \nabla_\beta w^\beta = 0

\displaystyle  \nabla_\alpha v^\alpha = 0.

\displaystyle  \nabla_\alpha w^\alpha = 2\varphi.

The metric {h} is hidden in this system through the covariant derivative {\nabla}. To eliminate the metric, we can lower indices to write

\displaystyle  \varphi w_\alpha + v^\beta \nabla_\beta v_\alpha = 0

\displaystyle  -2 \varphi v_\alpha + v^\beta \nabla_\beta w_\alpha + w^\beta \nabla_\beta v_\alpha = 0

\displaystyle  -3 \varphi w_\alpha + w^\beta \nabla_\beta w_\beta = 0

\displaystyle  \mathrm{div}_h v = 0.

\displaystyle  \mathrm{div}_h w = 2\varphi.

Here the divergence is relative to the volume form induced by {h}, but by a dimension lifting trick (see Section 3 of this paper of mine) one can replace this divergence with a divergence {\mathrm{div}_{vol}} with respect to any other volume form on {N}. We have the identity

\displaystyle  v^\beta \nabla_\beta v_\alpha = v^\beta (\nabla_\beta v_\alpha - \nabla_\alpha v_\beta) + \frac{1}{2} \partial_\alpha (v^\beta v_\beta)

\displaystyle v \neg d\theta + \frac{1}{2} d (\theta(v))

where we have switched to coordinate-free notation, and {\theta = h \cdot v} is the {1}-form associated to {v}. If we similarly let {\lambda} be the {1}-form associated to {w}, and eliminate {\varphi}, the system now becomes

\displaystyle  \frac{1}{2} \lambda \mathrm{div}_{vol} w + v \neg d\theta + \frac{1}{2} d (\theta(v)) = 0 \ \ \ \ \ (3)

\displaystyle  -\theta \mathrm{div}_{vol} w + v \neg d\lambda + w \neg d\theta + \frac{1}{2} d (\theta(w) + \lambda(v)) = 0 \ \ \ \ \ (4)

\displaystyle  -\frac{3}{2}\lambda \mathrm{div}_{vol} w + w \neg d\lambda + \frac{1}{2} d (\lambda(w)) = 0 \ \ \ \ \ (5)

\displaystyle  \mathrm{div}_{vol} v = 0. \ \ \ \ \ (6)

Also, the fact that {\lambda,\theta} are dual to {v,w} with respect to some unspecified Riemannian metric {h} turns out to essentially be equivalent to the assumption that the Gram matrix is positive definite,

\displaystyle  \begin{pmatrix} \lambda(v) & \lambda(w) \\ \theta(v) & \theta(w) \end{pmatrix} \succ 0; \ \ \ \ \ (7)

see Section 4 of the aforementioned paper. This looks like a rather strange system; but it is three vector equations (3), (4), (5) in four vector (or one-form) unknowns {v, w, \theta, \lambda}, together with a divergence-free condition (6) and a positive definiteness condition (7), which I view as basically being scalar conditions. Thus, this system becomes underdetermined when the dimension of {N} is large enough (in fact a naive count of degrees of freedom suggests that dimension at least three should be sufficient). It should thus be possible to locate an abundant number of solutions to this system; but to my frustration, the system is just barely complicated enough to prevent me from simplifying it to the point where it becomes evident how to construct solutions; in particular, I have not been able to find a viable further ansatz to transform the system to a more tractable one. Part of the problem is that while the system is technically underdetermined, there are not that many degrees of freedom to spare to ensure this underdetermined nature, so one cannot afford to make an ansatz that sacrifices too many of these degrees of freedom. In my previous paper I was able to use a very symmetric construction (taking {N} to basically be the product of an orthogonal group and a torus) to solve a similar system that was in fact quite overdetermined, but I have not been able to exploit such symmetries here. I have also experimented with other separation of variable ansatzes, but they tend to give similar systems to the ones here (up to some changes in the coefficients).

Remark 3 One can also try to directy create a self-similar blowup to (1), (2), for instance by making the ansatz

\displaystyle  u^1(t,x^1,y) = (t^6+(x^1)^2)^{1/3} \varphi(y)

\displaystyle  u^\alpha(t,x^1,y) = \frac{v^\alpha(y)}{(t^6+(x^1)^2)^{1/3}} + \frac{w^\alpha(y) + x^1 q^\alpha(y)}{(t^6+(x^1)^2)^{2/3}} + \frac{r^\alpha(y) + x^1 s^\alpha(y)}{(t^6+(x^1)^2)}

for {t<0} and some fields {\varphi \in C^\infty(N)} and {v,w,q,r,s \in \Gamma(TN)}. This particular ansatz seems consistent with all known conservation laws; however it works out to basically be ten vector equations (plus some additional scalar constraints) on ten vector field unknowns, so is just barely overdetermined. I have not been able to locate a self-similar blowup ansatz that is underdetermined.

Planar point sets with forbidden four-point patterns and few distinct distances

I’ve just uploaded to the arXiv my paper “Planar point sets with forbidden {4}-point patterns and few distinct distance“. This (very) short paper was a byproduct of my recent explorations of the Erdös problem website in recent months, with a vague emerging plan to locate a suitable problem that might be suitable for some combination of a crowdsourced “Polymath” style project and/or a test case for emerging AI tools. The question below was one potential candidate; however, upon reviewing the literature on the problem, I noticed that the existing techniques only needed one additional tweak to fully resolve the problem. So I ended up writing this note instead to close off the problem.

I’ve arranged this post so that this additional trick is postponed to below the fold, so that the reader can, if desired, try to guess for themselves what the final missing ingredient needed to solve the problem was. Here is the problem (Erdös problem #135), which was asked multiple times by Erdös over more than two decades (and who even offered a small prize for the solution on one of these occasions):

Problem 1 (Erdös #135) Let {A \subset {\bf R}^2} be a set of {n} points such that any four points in the set determine at least five distinct distances. Must {A} determine {\gg n^2} many distances?

This is a cousin of the significantly more famous Erdös distinct distances problem (Erdös problem #89), which asks what is the minimum number of distances determined by a set {A \subset {\bf R}^2} of {n} points in the plane, without the restriction on four-point configurations. The example of a square grid {\{0,\dots,\sqrt{n}-1\}^2} (assuming for sake of argument that {n} is a perfect square), together with some standard analytic number theory calculations, shows that {A} can determine {\asymp n/\sqrt{\log n}} distances, and it is conjectured that this is best possible up to constants. A celebrated result of Guth and Katz, discussed in this previous blog post, shows that {A} will determine at least {\gg n/\log n} distances. Note that the lower bound {\gg n^2} here is far larger, and in fact comparable to the total number {\binom{n}{2}} of distances available, thus expressing the belief that the “local” condition that every four points determine at least five distances forces the global collection distances to be almost completely distinct. In fact, in one of the papers posing the problem, Erdös made the even stronger conjecture that the set {A} must contain a subset {A'} of cardinality {\gg n} for which all the {\binom{|A'|}{2}} distances generated by {A} are distinct.

A paper of Dumitrescu came close to resolving this problem. Firstly, the number of ways in which four points could fail to determine five distinct distances was classified in that paper, with the four-point configurations necessarily being one of the following eight patterns:

  • {\pi_1}: An equilateral triangle plus an arbitrary vertex.
  • {\pi_2}: A parallelogram.
  • {\pi_3}: An isosceles trapezoid (four points on a line, {P_1,P_2,P_3,P_4}, where {\overleftrightarrow{P_1P_2} = \overleftrightarrow{P_3P_4}}, form a degenerate isosceles trapezoid).
  • {\pi_4}: A star with three edges of the same length.
  • {\pi_5}: A path with three edges of the same length.
  • {\pi_6}: A kite.
  • {\pi_7}: An isosceles triangle plus an edge incident to a base endpoint, and whose length equals the length of the base.
  • {\pi_8}: An isosceles triangle plus an edge incident to the apex, and whose length equals the length of the base.
(See Figure 1 and Lemma 1 of Dumitrescu’s paper.) So the question is asking whether if an {n} point set {A} avoids all of these patterns {\pi_1,\dots,\pi_8}, then it must generate {\gg n^2} distances.

Given that the grid {\{0,\dots,n-1\}^2} determine only {\asymp n^2 / \sqrt{\log n}} distances, one could seek a counterexample to this by finding a set of {\asymp n} points in the grid {\{0,\dots,n-1\}^2} that avoided all of the eight patterns {\pi_1,\dots,\pi_8}.

Dumitrescu then counted how often each of the patterns {\pi_1,\dots,\pi_8} occured inside the grid {\{0,\dots,n-1\}^2}. The answer is:

  • {\pi_1} does not occur at all. (This is related to the irrationality of {\sin \pi/3 = \sqrt{3}/2}.)
  • {\pi_2} occurs {\asymp n^6} times.
  • {\pi_3} occurs {\asymp n^5} times.
  • {\pi_4} occurs {O(n^{14/3} \log n)} times.
  • {\pi_5} occurs {O(n^{14/3} \log n)} times.
  • {\pi_6} occurs {\asymp n^5} times.
  • {\pi_7} occurs {O(n^{14/3} \log n)} times.
  • {\pi_8} occurs {O(n^{14/3} \log n)} times.
(The bounds involving {O(n^{14/3} \log n)} were obtained using the Szemerédi-Trotter theorem, and might not be optimal for this problem.) In particular, with the exception of the parallelogram pattern {\pi_2}, the other seven forbidden {4}-point patterns {\pi_1,\pi_3,\dots,\pi_8} occur at most {O(n^5)} times.

Using this and a standard probabilistic argument, Dumitrescu then established the following “near miss” to a negative answer to the above problem:

Theorem 2 (First near miss) If {n} is sufficiently large, then there exists a subset of {\{0,\dots,n-1\}^2} of cardinality {\asymp n} which avoids all of the patterms {\pi_1, \pi_3,\dots,\pi_8}.

In particular, this generates a set of {\asymp n} points with {O(n^2/\sqrt{\log n})} distances that avoids seven out of the eight required forbidden patterns; it is only the parallelograms {\pi_2} that are not avoided, and are the only remaining obstacle to a negative answer to the problem.

Proof: Let {\varepsilon>0} be a small constant, and let {A} be a random subset of {\{0,\dots,n-1\}^2}, formed by placing each element of {\{0,\dots,n-1\}^2} with an independent probability of {\varepsilon/n}. A standard application of Hoeffding’s inequality (or even the second moment method) shows that this set {A} will have cardinality {\asymp \varepsilon n} with high probability if {n} is large enough. On the other hand, each of the {O(n^5)} patterns {\pi_1,\pi_3,\dots,\pi_8} has a probability {\varepsilon^4/n^4} of lying inside {A}, so by linearity of expectation, the total number of such patterns inside {A} is {O( n^5 \varepsilon^4 / n^4 ) = O(\varepsilon^4 n)} on the average. In particular, by Markov’s inequality, we can find a set {A} of cardinality {\asymp \varepsilon n} with only {O(\varepsilon^4 n)} such patterns. Deleting all of these patterns from {A}, we obtain a set {A'} of cardinality {\asymp \varepsilon n - O(\varepsilon^4 n)}, which is {\asymp n} if {\varepsilon} is a sufficiently small constant. This establishes the claim. \Box

Unfortunately, this random set contains far too many parallelograms {\pi_2} ({\asymp n^2} such parallelograms, in fact) for this deletion argument to work. On the other hand, in earlier work of Thiele and of Dumitrescu, a separate construction of a set of {\asymp n} points in {\{0,\dots,n-1\}^2} that avoids all of the parallelograms {\pi_2} was given:

Theorem 3 (Second near miss) For {n} large, there exists a subset {S} of {\{0,\dots,n-1\}^2} of cardinality {\asymp n} which contains no parallelograms {\pi_2}. Furthermore, this set is in general position: no three points in {S} are collinear, and no four are concyclic. As a consequence, this set {S} in fact avoids the three patterns {\pi_1, \pi_2, \pi_3} (the pattern in {\pi_3} is concyclic, and the pattern {\pi_1} does not occur at all in the grid).

Proof: One uses an explicit algebraic construction, going back to an old paper of Erdös and Turán involving constructions of Sidon sets. Namely, one considers the set

\displaystyle  S := \{ (x,y) \in \{0,\dots,n-1\}^2: y = x^2 \hbox{ mod } p \} \ \ \ \ \ (1)

where {p} is a prime between {4n} and {8n} (the existence of which is guaranteed by Bertrand’s postulate). Standard Gauss sum estimates can be used to show that {S} has cardinality {\asymp n}. If {S} contained four points that were in a parallelogram or on a circle, or three points in a line, then one could lift up from {\{0,\dots,n-1\}^2} to the finite field plane {{\mathbf F}_p^2} and conclude that the finite field parabola {\{ (x,x^2): x \in {\bf F}_p \}} also contained four points in a parallelogram or a circle, or three points on a line. But straightforward algebraic calculations can be performed to show that none of these scenarios can occur. For instance, if {P, P+H, P+K, P+H+K} were four points on a parallelogram that were contained in a parabola, this would imply that an alternating sum of the form

\displaystyle  (x, x^2) - (x+h, (x+h)^2) - (x+k, (x+k)^2) + (x+h+k, (x+h+k)^2)

would vanish for some non-zero {h,k}; but this expression simplifies to {(0, 2hk)}, which cannot vanish for non-zero {h,k} as {p} is odd. (For the concylic claim, the parabola in {{\mathbf F}_p^2} can in fact contain four points on a circle, but only if their {x} coordinates sum to zero, and this cannot happen in {S})

Given that we have one “near-miss” in the literature that avoids {\pi_1, \pi_3, \dots, \pi_8}, and another “near-miss” that avoids {\pi_1, \pi_2, \pi_3}, it is natural to try to combine these two constructions to obtain a set that avoids all eight patterns {\pi_1,\dots,\pi_8}. This inspired the following problem of Dumitrescu (see Problem 2 of this paper):

Problem 4 Does the set {S} in (1) contain a subset of cardinality {\gg n} that avoids all eight of the patterns {\pi_1, \dots, \pi_8}?

Unfortunately, this problem looked difficult, as the number-theoretic task of counting the patterns {\pi_4,\dots,\pi_8} in {S} looked quite daunting.

This ends the survey of the prior literature on this problem. Can you guess the missing ingredient needed to resolve the problem? I will place the answer below the fold.

Continue reading