Post #1421415

For all the excitement about Math Inc.'s AI tool Gauss proving Erdős problem #1196 (4 typeset pages), and then it being formalised in Lean in 7000-ish ('golfed', i.e. reduced, to 4000-ish) lines of code, @tao [1] has mathematician-golfed the proof to two paragraphs using standard analytic number theory tools, with one very easy helper lemma about weighted graphs. It suppresses some details about how some estimates are achieved, but it reads like something Tao would blog anyway. I think a proper formalisation of this proof should be much less than 4000 lines, and should leverage good general-purpose analytic number theory estimates. [1] https://www.erdosproblems.com/forum/thread/1196#post-5521