## Stream: new members

### Topic: Goldbach's conjecture

#### Lars Ericson (Nov 29 2020 at 23:02):

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 (Nov 29 2020 at 23:13):

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

#### Bhavik Mehta (Nov 29 2020 at 23:28):

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 (Nov 29 2020 at 23:53):

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 (Nov 29 2020 at 23:54):

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

#### Jack Auchterlounie (Nov 29 2020 at 23:57):

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 (Nov 30 2020 at 00:08):

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.