This post contains two unrelated announcements. Firstly, I would like to promote a useful list of resources for AI in Mathematics, that was initiated by Talia Ringer (with the crowdsourced assistance of many others) during the National Academies workshop on “AI in mathematical reasoning” last year. This list is now accepting new contributions, updates, or corrections; please feel free to submit them directly to the list (which I am helping Talia to edit). Incidentally, next week there will be a followup webinar to the aforementioned workshop, building on the topics covered there. Secondly, I w ..read more

Tim Gowers, Ben Green, Freddie Manners, and I have just uploaded to the arXiv our paper “Marton’s conjecture in abelian groups with bounded torsion“. This paper fully resolves a conjecture of Katalin Marton (the bounded torsion case of the Polynomial Freiman–Ruzsa conjecture (first proposed by Katalin Marton): Theorem 1 (Marton’s conjecture) Let be an abelian -torsion group (thus, for all ), and let be such that . Then can be covered by at most translates of a subgroup of of cardinality at most . Moreover, is contained in for some . We had previously established the case of this r ..read more

The first progress prize competition for the AI Mathematical Olympiad has now launched. (Disclosure: I am on the advisory committee for the prize.) This is a competition in which contestants submit an AI model which, after the submissions deadline on June 27, will be tested (on a fixed computational resource, without internet access) on a set of 50 “private” test math problems, each of which has an answer as an integer between 0 and 999. Prior to the close of submission, the models can be tested on 50 “public” test math problems (where the results of the model are public, but not the problems ..read more

Earlier this year, I gave a series of lectures at the Joint Mathematics Meetings at San Francisco. I am uploading here the slides for these talks: “Machine assisted proof” (Video here) “Translational tilings of Euclidean space” (Video here) “Correlations of multiplicative functions” (Video here) I also have written a text version of the first talk, which has been submitted to the Notices of the American Mathematical Society ..read more

Let be a non-empty finite set. If is a random variable taking values in , the Shannon entropy of is defined as There is a nice variational formula that lets one compute logs of sums of exponentials in terms of this entropy: Lemma 1 (Gibbs variational formula) Let be a function. Then Proof: Note that shifting by a constant affects both sides of (1) the same way, so we may normalize . Then is now the probability distribution of some random variable , and the inequality can be rewritten as But this is precisely the Gibbs inequality. (The expression inside the supremum can also be wri ..read more

In my previous post, I walked through the task of formally deducing one lemma from another in Lean 4. The deduction was deliberately chosen to be short and only showcased a small number of Lean tactics. Here I would like to walk through the process I used for a slightly longer proof I worked out recently, after seeing the following challenge from Damek Davis: to formalize (in a civilized fashion) the proof of the following lemma: Lemma. Let and be sequences of real numbers indexed by natural numbers , with non-increasing and non-negative. Suppose also that for all . Then for all . Here ..read more

Since the release of my preprint with Tim, Ben, and Freddie proving the Polynomial Freiman-Ruzsa (PFR) conjecture over , I (together with Yael Dillies and Bhavik Mehta) have started a collaborative project to formalize this argument in the proof assistant language Lean4. It has been less than a week since the project was launched, but it is proceeding quite well, with a significant fraction of the paper already either fully or partially formalized. The project has been greatly assisted by the Blueprint tool of Patrick Massot, which allows one to write a human-readable “blueprint” of the proof ..read more

A common task in analysis is to obtain bounds on sums or integrals where is some simple region (such as an interval) in one or more dimensions, and is an explicit (and elementary) non-negative expression involving one or more variables (such as or , and possibly also some additional parameters. Often, one would be content with an order of magnitude upper bound such as or where we use (or or ) to denote the bound for some constant ; sometimes one wishes to also obtain the matching lower bound, thus obtaining or where is synonymous with . Finally, one may wish to obtain a more preci ..read more

Rachel Greenfeld and I have just uploaded to the arXiv our paper “Undecidability of translational monotilings“. This is a sequel to our previous paper in which we constructed a translational monotiling of a high-dimensional lattice (thus the monotile is a finite set and the translates , of partition ) which was aperiodic (there is no way to “repair” this tiling into a periodic tiling , in which is now periodic with respect to a finite index subgroup of ). This disproved the periodic tiling conjecture of Stein, Grunbaum-Shephard and Lagarias-Wang, which asserted that such aperiodic transl ..read more

I have just uploaded to the arXiv my paper “Monotone non-decreasing sequences of the Euler totient function“. This paper concerns the quantity , defined as the length of the longest subsequence of the numbers from to for which the Euler totient function is non-decreasing. The first few values of are (OEIS A365339). For instance, because the totient function is non-decreasing on the set or , but not on the set . Since for any prime , we have , where is the prime counting function. Empirically, the primes come quite close to achieving the maximum length ; indeed it was conjectured by Po ..read more