Zulip Chat Archive

Stream: maths

Topic: Formalizing the ternary Goldbach conjecture


view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:27):

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?

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:28):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:29):

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

view this post on Zulip Patrick Massot (Aug 07 2020 at 11:30):

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

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:30):

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?

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:30):

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

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:30):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:31):

Sure, but that's a problem I understand

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:31):

I want to know about the mathy parts

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:31):

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

view this post on Zulip Patrick Massot (Aug 07 2020 at 11:32):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:32):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:33):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:43):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:44):

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

view this post on Zulip Mario Carneiro (Aug 07 2020 at 11:45):

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

view this post on Zulip Kevin Buzzard (Aug 07 2020 at 11:50):

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.


Last updated: May 09 2021 at 11:09 UTC