Formalizing the ternary Goldbach conjecture

Stream: maths

[Mario Carneiro]

A conversation recently started on the metamath board about formalizing Helfgott's proof of the ternary goldbach conjecture. Could someone with some expertise in analytic number theory take a look at the proof and estimate what would be needed to formalize the paper part of the proof (for C large)? There are also some tricks used to reduce TGB <= 10^30 to RH <= 10^10, and then more tricks to prove RH <= 10^10. Ignoring the computational aspect, how does a formalization of the TGB toolbox compare to, for example, the FLT toolbox?

[Kevin Buzzard]

You're not going to be able to formalise the brute force computational search I shouldn't think -- this was in some sense one of the hardest parts of the proof and it's not formalised

[Mario Carneiro]

It's never a brute force search with these things, that's the point

[Patrick Massot]

I think Assia worked on some required integral estimates, and found a mistake that is fortunately not fatal.

[Kevin Buzzard]

To do the analysis part you're going to have to formalise the circle method I guess, and also have a way of rigorously computing integrals very accurately. Did you see @Assia Mahboubi 's talk on this?

[Mario Carneiro]

you look at the numbers and see "we checked TGB <= 10^30" and think "gee that's a lot of horsepower" but of course the these folks know how to do maths too and they use lots of tricks to bring them under the realm of feasibility

[Kevin Buzzard]

yes but they're writing custom C++ code or whatever to do this part

[Mario Carneiro]

Sure, but that's a problem I understand

[Mario Carneiro]

I want to know about the mathy parts

[Mario Carneiro]

like what do all these integrals have to do with ternary goldbach

[Patrick Massot]

See page 19 of https://hal.inria.fr/hal-01630143v2/document

[Mario Carneiro]

how much work would it be to formalize the paper part of the proof?

[Mario Carneiro]

I have no doubt that it's possible to estimate integrals by a myriad of methods

[Mario Carneiro]

oh boy, it depends on https://arxiv.org/pdf/1305.2897.pdf which has another 80 pages of integrals

[Mario Carneiro]

And https://arxiv.org/pdf/1205.5252.pdf, another 80 pages

[Mario Carneiro]

I think the author just had an 80 page limit and spread out the publications

[Kevin Buzzard]

I am a bit annoyed that I can't find Assia's video lecture which was given as part of Leroy's type theory lectures from 2018 -- links like https://www.college-de-france.fr/site/xavier-leroy/course-2018-11-28-10h00.htm are not working for me. He gave a series of lectures and others gave some guest lectures -- Assia talked in part about Helfgott's estimate. But Patrick has posted a pdf now.

Warning: I am not an expert.

Helfgott's main contribution is to tighten up the arguments used (it has been known for nearly a century that all sufficiently large odd integers are the sum of three primes) until the estimates given by the techniques were sufficiently strong that the search space became (just) feasible. So really if you want to understand what is going on you may as well look at the original proofs e.g. Vinogradov's work from the '30s, which proved the result but with a much worse explicit bound. Helfgott "just" did the error estimates far far far more precisely.

The idea is to come up with a function F(x) which is bounded below by a positive constant such that for n odd and sufficiently large, the number of ways expressing n as a sum of three primes is at least F(n). Here F is some kind of analytic function like N^2/(log N)^3.

https://en.wikipedia.org/wiki/Vinogradov%27s_theorem

Vinogradov used the circle method to get this estimate.

https://en.wikipedia.org/wiki/Hardy%E2%80%93Littlewood_circle_method

The idea here is very elegant -- it says that for the kind of functions which come up in this area, if you want to integrate them from 0 to 1 then you can break up the interval into two pieces -- the "major arcs" (which are small neighbourhoods of rational numbers with denominator bounded by some D) and the "minor arcs" (all the rest). By estimating the integral over the major and minor arcs you get bounds for the integral. The trick for estimating these things is basically to use Fourier inversion to interpret what's going on near a rational number as some contribution to a function from a period function with small period.