# Zulip Chat Archive

## 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.

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

#### Jack Auchterlounie (Nov 30 2020 at 00:14):

oh i also misread that

#### Mario Carneiro (Nov 30 2020 at 02:58):

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"

Last updated: Dec 20 2023 at 11:08 UTC