You are currently browsing the monthly archive for September 2024.
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 was equal to
. 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 equipped with a binary operation
. Initially, no additional axioms on this operation
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
and one or more indeterminate variables in
. Two familiar examples of such axioms are the commutative axiom
To illustrate the project I have in mind, let me first introduce eleven examples of equational axioms for magmas:
- Equation1:
- Equation2:
- Equation3:
- Equation4:
- Equation5:
- Equation6:
- Equation7:
- Equation8:
- Equation9:
- Equation10:
- Equation11:
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 obeys Equation4, thus
. Specializing to
, we conclude
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
- 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.
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 of equations that use the magma operation
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
is the number of ways one can form an expression out of
applications of a binary operation
(applied to
placeholder variables); and, given a string of
placeholder variables, the Bell number
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
It is not clear to me at all what the geometry of 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 would then require
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
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 , and it should be quite easy to check which of the
laws are implied by either of these two laws. The poset
has a reflection symmetry associated to replacing the binary operator
by its reflection
, 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
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 as input (in which each potential comparison
in
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.
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 and almost all
, whenever
is a measure-preserving system (not necessarily of finite measure), and
,
for some
with
, where
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
The basic strategy is to try to insert the weight everywhere in the proof of the convergence of (1) and adapt as needed. The weighted averages are bilinear averages associated to the bilinear symbol
Given a smooth compact Riemannian manifold , the incompressible Euler equations can be written in abstract index notation as
Conjecture 1 (Finite time blowup) There exists a manifoldand a smooth solution
to the Euler equations that blows up at some finite time
.
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 and
is sufficiently small, there exists a
solution
to the Euler equations on
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 :
Theorem 2 (Finite time blowup for the forced equation) There exists a smooth solution to the forced Euler equations onthat exhibits finite time blowup, in which the forcing term
stays uniformly bounded in
for any
.
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 , which is conducive to generating an exponential “stretching” of a small forcing term at a much higher spatial scale
, 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 , where
is a smooth compact manifold, and the metric on
is just the sum of the standard metric
on the first coordinate and
:
If we now use Greek indices to only denote coordinates in the “vertical” coordinate , the velocity field
now becomes
, and the Euler equations now split as
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 ,
to the equation
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
Nevertheless, one can still attempt to solve this equation by separation of variables. If one makes the ansatz
The metric is hidden in this system through the covariant derivative
. To eliminate the metric, we can lower indices to write
Remark 3 One can also try to directy create a self-similar blowup to (1), (2), for instance by making the ansatz
for
and some fields
and
. 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.
I’ve just uploaded to the arXiv my paper “Planar point sets with forbidden -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) Letbe a set of
points such that any four points in the set determine at least five distinct distances. Must
determine
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 of
points in the plane, without the restriction on four-point configurations. The example of a square grid
(assuming for sake of argument that
is a perfect square), together with some standard analytic number theory calculations, shows that
can determine
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
will determine at least
distances. Note that the lower bound
here is far larger, and in fact comparable to the total number
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
must contain a subset
of cardinality
for which all the
distances generated by
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:
-
: An equilateral triangle plus an arbitrary vertex.
-
: A parallelogram.
-
: An isosceles trapezoid (four points on a line,
, where
, form a degenerate isosceles trapezoid).
-
: A star with three edges of the same length.
-
: A path with three edges of the same length.
-
: A kite.
-
: An isosceles triangle plus an edge incident to a base endpoint, and whose length equals the length of the base.
-
: An isosceles triangle plus an edge incident to the apex, and whose length equals the length of the base.
Given that the grid determine only
distances, one could seek a counterexample to this by finding a set of
points in the grid
that avoided all of the eight patterns
.
Dumitrescu then counted how often each of the patterns occured inside the grid
. The answer is:
-
does not occur at all. (This is related to the irrationality of
.)
-
occurs
times.
-
occurs
times.
-
occurs
times.
-
occurs
times.
-
occurs
times.
-
occurs
times.
-
occurs
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) Ifis sufficiently large, then there exists a subset of
of cardinality
which avoids all of the patterms
.
In particular, this generates a set of points with
distances that avoids seven out of the eight required forbidden patterns; it is only the parallelograms
that are not avoided, and are the only remaining obstacle to a negative answer to the problem.
Proof: Let be a small constant, and let
be a random subset of
, formed by placing each element of
with an independent probability of
. A standard application of Hoeffding’s inequality (or even the second moment method) shows that this set
will have cardinality
with high probability if
is large enough. On the other hand, each of the
patterns
has a probability
of lying inside
, so by linearity of expectation, the total number of such patterns inside
is
on the average. In particular, by Markov’s inequality, we can find a set
of cardinality
with only
such patterns. Deleting all of these patterns from
, we obtain a set
of cardinality
, which is
if
is a sufficiently small constant. This establishes the claim.
Unfortunately, this random set contains far too many parallelograms (
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
points in
that avoids all of the parallelograms
was given:
Theorem 3 (Second near miss) Forlarge, there exists a subset
of
of cardinality
which contains no parallelograms
. Furthermore, this set is in general position: no three points in
are collinear, and no four are concyclic. As a consequence, this set
in fact avoids the three patterns
(the pattern in
is concyclic, and the pattern
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 is a prime between
and
(the existence of which is guaranteed by Bertrand’s postulate). Standard Gauss sum estimates can be used to show that
has cardinality
. If
contained four points that were in a parallelogram or on a circle, or three points in a line, then one could lift up from
to the finite field plane
and conclude that the finite field parabola
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
were four points on a parallelogram that were contained in a parabola, this would imply that an alternating sum of the form
Given that we have one “near-miss” in the literature that avoids , and another “near-miss” that avoids
, it is natural to try to combine these two constructions to obtain a set that avoids all eight patterns
. This inspired the following problem of Dumitrescu (see Problem 2 of this paper):
Problem 4 Does the setin (1) contain a subset of cardinality
that avoids all eight of the patterns
?
Unfortunately, this problem looked difficult, as the number-theoretic task of counting the patterns in
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.


Recent Comments