## Stream: maths

### Topic: Formalizing the ternary Goldbach conjecture

#### 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?

#### 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

#### Mario Carneiro (Aug 07 2020 at 11:29):

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

#### 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.

#### 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?

#### 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

#### Kevin Buzzard (Aug 07 2020 at 11:30):

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

#### Mario Carneiro (Aug 07 2020 at 11:31):

Sure, but that's a problem I understand

#### Mario Carneiro (Aug 07 2020 at 11:31):

I want to know about the mathy parts

#### Mario Carneiro (Aug 07 2020 at 11:31):

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

#### Patrick Massot (Aug 07 2020 at 11:32):

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

#### Mario Carneiro (Aug 07 2020 at 11:32):

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

#### Mario Carneiro (Aug 07 2020 at 11:33):

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

#### 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

#### Mario Carneiro (Aug 07 2020 at 11:44):

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

#### Mario Carneiro (Aug 07 2020 at 11:45):

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

#### 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.