Goldbach's conjecture

Stream: new members

[Lars Ericson]

One of the chapter 4 exercises is

def goldbach_conjecture : Prop := ∀ (n: ℕ), my_even(n) → ∃ (p₁: ℕ), ∃ (p₂ : ℕ), my_prime(p₁) ∧ my_prime(p₂) ∧ n = p₁ + p₂

There is a proof in Arxiv that might be suited to a Lean verification: https://arxiv.org/pdf/1811.02415.pdf

This seems to be a popular topic in the Lean space: https://www.codewars.com/kata/5eb718d0e7c54e001a6e03b8, including this topic by @Jeremy Avigad : http://www.andrew.cmu.edu/user/avigad/Talks/oxford_formal_methods.pdf

Not asking a question, just reflecting on the exercise.

[Alex J. Best]

The proof on arxiv seems unlikely to be correct, Goldbach's conjecture (when stated properly) is still an open problem in math.

[Bhavik Mehta]

I should say that I made that kata as a bit of fun about checking the statement you're trying to prove, not as any serious attempt to resolve the Goldbach conjecture

[Lars Ericson]

Thanks @Bhavik Mehta. @Alex J. Best , precisely because it is likely to be incorrect, it seems like it would fun to see if it is clean enough to formalize in Lean, and then to find the flaw.

[Reid Barton]

Generally the way these things go is that it will be harder to find any part that is correct.

[Jack Auchterlounie]

I can tell you there is at least one flaw at the bottom of page 6 because what he claims is an overestimate is in fact an underestimate for eg 4, 10 (I didn't spot this, shamelessly stealing from someone else). I also think the only thing he actually proves is that at there exists at least one sum of prime + composite odd numbers which is.... obvious. Could be wrong about that though I haven't really read it.

[Chris Hughes]

Jack Auchterlounie said:

I can tell you there is at least one flaw at the bottom of page 6 because what he claims is an overestimate is in fact an underestimate for eg 4, 10 (I didn't spot this, shamelessly stealing from someone else). I also think the only thing he actually proves is that at there exists at least one sum of prime + composite odd numbers which is.... obvious. Could be wrong about that though I haven't really read it.

I might have been wrong about this. I misread a definition.

[Jack Auchterlounie]

oh i also misread that

[Mario Carneiro]

I was underwhelmed. There is a lot of imprecise thinking and bad notation, and ultimately what is derived is an approximation at large numbers (without watching the approximation bounds), not an actual lower bound, and on page 13, to compare to the real value, it amounts to "I plotted it and it looks pretty good up to 5000"