> > On the path to the Hardy-Littlewood circle method, at the center of > Goldbach’s conjecture, Is Cauchy’s residue theorem, which is on the list of > obvious omissions to the 100 theorems to be formalized. We should probably > start with a formalization of the line (contour) integrals.
Although it is true that the original Hardy-Littlewood method requires complex analysis, nowadays it's often formulated in the language of exponential sums. In particular, Vinogradov's proof of Goldbach ternary conjecture for large numbers does not require Cauchy's theorem or any complex analysis whatsoever (so good-old ~df-itg is enough). That being said, it does require Siegel-Walfisz theorem (an asymptotic for the sum of log p for primes p = a (mod n)). I'm not sure if there's an elementary proof of that result and if it (possibly) could be derived from metamath's current treatment of Dirichlet's theorem. One can of course start with a simpler application of the circle method, for instance, with Waring's problem. It's solution is more or less elementary and sure many intermediate results will prove to be useful in the formalization of Vinogradov's (or Helfgott's) proof. -- You received this message because you are subscribed to the Google Groups "Metamath" group. To unsubscribe from this group and stop receiving emails from it, send an email to [email protected]. To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/f9d1aea7-b339-49c4-bfb0-669a8a622a9eo%40googlegroups.com.
