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. One of the building blocks could be Jeff Madsen’s definition of path concatenation (df-pco), and Mario’s developments.
So the path would be: - Line integrals - Cauchy’s Residue Theorem - Hardy-Littlewood circle method - Goldbach’s conjecture If we want to try an “OpenAI” collaborative method, maybe experienced Metamath users could post definition and theorem statements, letting OpenAI fill-in the proof? >From my experience playing with the OpenAI proof assistant, it is quite good >at filling in the blanks automatically, but did not suggest with a high >confidence the main proof steps. That should complement very well a human, who >sees well the big picture and the main steps, but is much more inefficient in >those smaller steps. Maybe the proof statements could be completed with the >main proof steps? BR, _ Thierry -- 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/F07254FF-36D6-490C-B8D0-5371D239E29E%40gmx.net.
