Lean on Goldbach's conjecture

Stream: maths

[Frank Vega]

We prove that the Goldbach's conjecture is true using the artificial intelligence tools of the math library of Lean 4 as a proof assistant:
Proof of the Goldbach's conjecture
This proof is partially using and applying number theory and finally we implement a project in Lean 4 to support our conclusions.
I'm sharing a Print-screen of my Lean 4 code with the correctness of the proof:
Lean 4 Project
The lean code and the math number theory support is inside of the paper linked as Proof of the Goldbach's conjecture.
Thanks....

[Eric Wieser]

Your screenshot does not show correctness of the proof any more than #check False does, I'm afraid.

[Kevin Buzzard]

A correct Lean proof of Goldbach's conjecture would be a proof of an assertion involving even natural numbers and primes. You've used Lean to prove (or possibly even just state) something else and then are claiming that this other thing implies Goldbach's conjecture, and that's perhaps where the problem lies.

I think that to convince the community that you've proved Goldbach's conjecture you will need to create a term of the relevant type, not this intermediate type.

[Eric Wieser]

From the screenshot, it looks like you've stated goldbach's conjecture in Lean, not proved it.

[Eric Wieser]

To prove it, you need #check foo to output foo : Goldbach_Proof, with Goldbach_Proof on the right of the colon

[Frank Vega]

Here, I'm sending the code in case you have any doubt and wish to test it:
prover.lean

[Kevin Buzzard]

The (poorly-named) Goldbach_Proof is not a proof, it is a statement.

[Kevin Buzzard]

def i_am_not_a_proof : Type := Proof (2 + 2 = 5)

[Kevin Buzzard]

theorem i_am_a_proof : Proof (2 + 2 = 4) := by
  constructor
  rfl

[Frank Vega]

Note that, the statement Proof:

/-- Lean proof. -/
structure Proof (p : Prop) : Type where
proof : p

in the code receives as an argument a proposition

[Kevin Buzzard]

Yes. Do you understand the difference between my two examples where I state that 2+2=5 but then I prove that 2+2=4? You have stated some assertion about real numbers which you're claiming implies Goldbach. You haven't proved anything in the Lean code.

[Kevin Buzzard]

When you're stating something, Proof comes after the :=. When you're proving it, Proof comes before the :=.

[Ruben Van de Velde]

The lack of any kind of, uh, proof is also somewhat suspicious

[Damiano Testa]

As an experiment, you can add ¬ in front of your statement and see that basically nothing changes.

[Eric Wieser]

That is, Proof (¬ ∀ n, ...)

[Eric Wieser]

(as Kevin alludes to, this Proof is misnamed, it's just docs#PLift and is certainly just a distraction here)

[Frank Vega]

Thank you all! You are right! I started to learn Lean since the last Thursday where I watched a Quanta Youtube video about Math and AI and I realized I could apply it to an inequality that is equivalent to Goldbach's conjecture for even numbers N = 2*n > 4 * 10^18 (which is a not a quite difficult result in number theory). Indeed, the merit would be whether the Lean code could solve this issue and whether I could be able to do it or not. Here it is another attempt (any advice, critics and comment is welcome):

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Init.Prelude

/-- Goldbach function. -/
noncomputable def H (n k : ℝ): ℝ :=
  let m: ℝ := n - k
  let myexp: ℝ := n^0.889
  let myconst: ℝ := 1.1229
  let mylog: ℝ := Real.log m
  let myloglog: ℝ := Real.log mylog
  let mydivisor: ℝ := myloglog/myconst
  let myfraction: ℝ := n/m
  let value: ℝ := myfraction/mydivisor + myexp + (m - 1)/2 + 1.0 - n
  value

/-- Goldbach decision. -/
noncomputable def Goldbach_Decide (n k: ℕ): Prop :=
(n - k >= 11 && (H n k) >= 0 && Nat.Prime (n + k))

/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (p : Prop := Goldbach_Decide n k) (q: Prop := Nat.Prime (n - k)) (hp : p) (hq : q) : p ∧ q :=
  by apply And.intro
     exact hp
     exact hq

[Frédéric Dupuis]

Another hint that this couldn't possibly work is that the purported proof in your paper is totally absent from the code.

[Johan Commelin]

@Frank Vega quick tip: you can use #backticks (follow the link for info) to format your code

[Johan Commelin]

Another tip: a working proof doesn't need to use the #check command, you can leave that out.

[Frank Vega]

@Johan Commelin thank you for your help: Let me see if I can edit my previous message to use the blackticks. @Frédéric Dupuis that would be perfect: however learning Lean in so short time makes me less than a junior (thank you for the advice).

[Alex J. Best]

I would humbly recommend you try and learn lean via some of our recommended resources https://leanprover-community.github.io/learn.html covering mathematics which is well understood before jumping in at the deep end with a big open conjecture. I think people here would be happy to help you learn the system but that its much easier with simple examples where the mathematics is something more straightforward

[Frank Vega]

@Alex J. Best thank you for your advice. The part I need to check in order to make a good conclusion is to prove the inequality that I cited in the next message where I did some corrections. I'm sure everybody else could make it better than I'm trying to do it in Lean: that's why I need to follow your advice and go deep :)

[Frank Vega]

@Alex J. Best these are some corrections:
The Goldbach's conjecture is equivalent to state the inequality

$$\frac{2 \cdot n}{e^{\gamma} \cdot (n - k) \cdot \log \log (n - k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n \geq 0$$

holds whenever $(n + k)$ is prime, $(n - k) \geq 11$ and $n > 2 \cdot 10^{18}$ (under these conditions $(n- k)$ is necessarily prime).

[Newell Jensen]

@Frank Vega You can can render LaTeX in zulip.

For example \int_{0}^{1} f(x) dx is:

$$\int_{0}^{1} f(x) dx$$

Checkout the ? symbol below where you input your messages for hints.

[Frank Vega]

@Newell Jensen great!!! It is nicer in that way: I fixed the latex formula and the lean code (good hints!!!)

[Newell Jensen]

You can also render inline LaTeX with double $$. For example here $n > 2 \cdot 10^{18}$

[Yury G. Kudryashov]

If you want to prove the Goldbach's conjecture in Lean, then you need to fill in sorry in

theorem goldbach (n : Nat) (he : Even n) (h2 : 2 < n) : ∃ p q : Nat, p.Prime ∧ q.Prime ∧ p + q = n :=
  sorry

[Frank Vega]

@Yury G. Kudryashov my intention is to use Lean as an assistant to verify a final result obtained by number theory. See the results here: Proof of Goldbach's conjecture
You might find easier to follow the arguments in number theory and understand the final and previous inequality equivalent to the conjecture!.

[Frank Vega]

@Kevin Buzzard , Is my last Lean code correct (the number theory support is correct because it is trivial)?

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Init.Prelude

/-- Goldbach function. -/
noncomputable def H (n k : ℝ): ℝ :=
  let m: ℝ := n - k
  let myexp: ℝ := n^0.889
  let myconst: ℝ := 1.1229
  let mylog: ℝ := Real.log m
  let myloglog: ℝ := Real.log mylog
  let mydivisor: ℝ := myloglog/myconst
  let myfraction: ℝ := n/m
  let value: ℝ := myfraction/mydivisor + myexp + (m - 1)/2 + 1.0 - n
  value

/-- Goldbach decision. -/
noncomputable def Goldbach_Decide (n k: ℕ): Prop :=
(n - k >= 11 && (H n k) >= 0 && Nat.Prime (n + k))

/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (p : Prop := Goldbach_Decide n k) (q: Prop := Nat.Prime (n - k)) (hp : p) (hq : q) : p ∧ q :=
  by apply And.intro
     exact hp
     exact hq

Thanks in advance...

[Kevin Buzzard]

This code is not a proof of the goldbach conjecture no

[Frank Vega]

@Kevin Buzzard , I guess you meant to say that code does not prove the following inequality (Is that the case?)

$$\frac{2 \cdot n}{e^{\gamma} \cdot (n - k) \cdot \log \log (n - k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n \geq 0$$

I would not worry of my number theory results because as I already said is trivial.

[Kevin Buzzard]

That's correct, you are not proving anything other than the fact that if P and Q are true then so is P and Q.

[Yury G. Kudryashov]

Hint: if there is no visible mathematical content in your Lean proofs, then probably you don't prove any meaningful mathematical result.

[Yury G. Kudryashov]

You should expect a Lean proof to be much longer than a traditional proof (with a few exceptions for the cases when we have a tactic that does some dirty work).

[Frank Vega]

@Kevin Buzzard , Notice that And.intro is

And.intro : P → Q → P ∧ Q

but in this case

$$P = \frac{2 \cdot n}{e^{\gamma} \cdot (n - k) \cdot \log \log (n - k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n \geq 0$$

and

$$Q = (n - k) \textit{ is Prime}$$

So, my intention is to show when the inequality (P) is true then this implies that necessary n - k is prime (Q)
Is there a better way to do this or And.intro is just fine in this case?

[Yaël Dillies]

You stated P → (Q → P ∧ Q). You meant to state P → Q. Here's your corrected statement:

theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] :
  Goldbach_Decide n k → Nat.Prime (n - k) := sorry

[Frank Vega]

@Yaël Dillies , Yes that would be

theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (p : Prop := Goldbach_Decide n k) (q: Prop := Nat.Prime (n - k)) (hp : p) (hq : q) : p  →  q := sorry

What is the correct answer here (how would you fill the "sorry" statement in the previous code)?
Thanks in advance...

[Yury G. Kudryashov]

What is the mathematical proof here?

[Yury G. Kudryashov]

You need to write a VERY detailed proof on paper first.

[Yaël Dillies]

That I don't know! Stating something in Lean is much easier than proving it. And you were the one claiming you had a proof :smile:

[Frank Vega]

@Yaël Dillies , In the previous code: Is there a way to put

hp →  hq

?
My experience until now is in number theory: I'm not ashamed to show my ignorance in this language since I'm a beginner.
I was also a beginner in number theory few years ago and I was able to publish a paper in the prestigious Springer journal of The Ramanujan Journal the past year (which is one the best math journal about number theory):
Article published by The Ramanujan Journal about the Riemann Hypothesis
So, @Yury G. Kudryashov is right, there is a probability that I'm wrong in my assumptions, but there is another probability (maybe small) that I running over the correct road.
Thank you in advance

[Yury G. Kudryashov]

Do you have a written proof of your theorem?

[Eric Wieser]

Frank Vega said:

What is the correct answer here (how would you fill the "sorry" statement in the previous code)?
Thanks in advance...

When you write theorem bad (p : Prop := Goldbach_Decide n k) : p := sorry this means something very different to theorem ok : Goldbach_Decide n k := sorry. The first says "let p be any proposition (and if you forget to tell me which one, I'll use GoldBach_Decide). I will prove this arbitrary p". The second says "I will prove GoldBach_Decide".

[Yury G. Kudryashov]

I mean, the theorem you want to formalize in Lean, not the theorem that relates this fact to Goldbach's conjecture.

[Eric Wieser]

Perhaps mathlib should have a linter for default non-Prop arguments in theorems?

[Yury G. Kudryashov]

We often have (μ : Measure := by volume_tac)

[Frank Vega]

@Yury G. Kudryashov : Yes, here it is
Proof of Goldabch's conjecture
It is now a draft because I obviously cannot provide the correct Lean code yet

[Yury G. Kudryashov]

Which thm in this paper do you want to formalize in Lean?

[Frank Vega]

@Eric Wieser Thank you very much. This clarifies much to me...

[Yury G. Kudryashov]

Do you have a written proof of this theorem, not of (this theorem => Goldbach's conjecture)?

[Frank Vega]

@Yury G. Kudryashov the paper has only one theorem (Theorem 1). The end of Theorem 1 is the following conclusions:
The Goldbach's conjecture is equivalent to state the inequality

$$\frac{2 \cdot n}{e^{\gamma} \cdot (n - k) \cdot \log \log (n - k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n \geq 0$$

holds whenever $(n + k)$ is prime, $(n - k) \geq 11$ and $n > 2 \cdot 10^{18}$ (under these conditions $(n- k)$ is necessarily prime). It is not in the way of (this theorem => Goldbach's conjecture) because the theorem is proven that is true: what we do not know is whether the previous inequality always holds. Thanks in advance.

[Yury G. Kudryashov]

So, you can deduce Goldbach's conjecture from some inequality. Do you have a proof of this inequality? I'm not an expert in number theory or tricky inequalities, so I can't help with a mathematical proof here.

[Yury G. Kudryashov]

Also, we don't have an AI that can generate nontrivial proofs yet.

[Yury G. Kudryashov]

And I don't expect that we'll have it in the next few years.

[Frank Vega]

@Yury G. Kudryashov I believe at first that inequality was a waste of time. However, using Wolfram Alpha I realized that the inequality is always true for $k = (\log^{2} n) \cdot \sqrt{n}$ and $n > 2 \cdot 10^{18}$. It will be plenty enough to prove the inequality over those parameters (the number theory proof is trivial: believe me). However, the theorem 1 uses the Robin's inequality for odd numbers that we know is true for all odd numbers greater than 11. For that reason I suggest to attack the inequality as a shortcut, because if you achieve to prove the Robin's inequality for odd numbers in Lean, then you might be able to prove it for even numbers and that implies the Riemann hypothesis by Robin's criterion (1984) (so maybe it is convenience to skip those number theory steps)

[Yury G. Kudryashov]

Let me repeat: while we can help you with translating an existing proof to Lean code, you need to prove your theorem first.

[Frank Vega]

@Yury G. Kudryashov Thank you. The theorem is proven in the manuscript I shared before.

def Goldbach_Prop: Prop :=
  let bound: ℕ := 2000000000000000000
  ∀ n: ℕ, ∃ k: ℕ, (n > bound) → (n - k >= 11 && (H n k) >= 0 && Nat.Prime (n + k))  ```

In number theory I basically proved that

Goldbach_Prop → Nat.Prime (n - k)

and so you only need to prove the proposition Goldbach_Prop in order to complete the proof. That's it. Do I explain myself well this time? Note that, $bound = 2 \cdot 10^{18}$ since for a lower bound has been verified by Oliveira at Goldbach conjecture verification.

[Frank Vega]

@Yury G. Kudryashov Note that, if $(n + k)$ and $(n - k)$ are primes, then the even number $N = (n + k) + (n - k) = 2 \cdot n$ complies with the Goldbach's conjecture

[Frank Vega]

@Yury G. Kudryashov Note also that

$$H(n, k) = \frac{1.1229 \cdot n}{(n - k) \cdot \log \log (n - k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n$$

since

$$\frac{2}{e^{\gamma}} > 1.1229$$

[Frank Vega]

@Yury G. Kudryashov : Feel free to contact me at anytime: Thanks in advance....

[Johan Commelin]

@Frank Vega Are you able to write the Lean statement (not the proof!) of the Goldbach conjecture, in the way that it is usually stated?

[Johan Commelin]

Because I have not found it in any of your code snippets. And I think it would be very useful to state the Goldbach conjecture as a little exercise to demonstrate that you know how Lean statements work.

[Frank Vega]

@Johan Commelin the user @Yury G. Kudryashov already did it some comments above (I copied and pasted his code):

theorem goldbach (n : Nat) (he : Even n) (h2 : 2 < n) : ∃ p q : Nat, p.Prime ∧ q.Prime ∧ p + q = n :=
  sorry

[Johan Commelin]

Ok, that looks good.

[Johan Commelin]

Now, can you also write down the statement of the inequality that you claim is equivalent to Goldbach (for large n)?

[Johan Commelin]

Is that your H from before?

[Frank Vega]

@Johan Commelin Yes, of course. The inequality is (as a proposition):

/-- Goldbach inequality. -/
noncomputable def H (n k : ℝ): Prop :=
  let m: ℝ := n - k
  let myexp: ℝ := n^0.889
  let myconst: ℝ := 1.1229
  let mylog: ℝ := Real.log m
  let myloglog: ℝ := Real.log mylog
  let mydivisor: ℝ := myloglog/myconst
  let myfraction: ℝ := n/m
  let value: ℝ := myfraction/mydivisor + myexp + (m - 1)/2 + 1.0 - n
  value >= 0

Note that, I made some changes to convert it from a real function into a function that returns a proposition!

[Johan Commelin]

I find this statement quite hard to read. I would start with open Real in above this code.

[Johan Commelin]

And then try to make the statement look as close as possible to your LaTeX version

[Johan Commelin]

Need to run now. See you later.

[Frank Vega]

@Johan Commelin we also must introduce some preconditions in order to complete the proof:
$(n > 2000000000000000000) \wedge (n -k) \geq 11 \wedge (n + k) \textit{ is Prime}$

[Frank Vega]

@Johan Commelin the goal is to show (H n k) together to these preconditions. I was a Scala programmer during 3 or 4 years and I spent a hard time to adapt to functional programming: I dealing with the same thing with Lean now. The only thing this time happens: I suspect the proof could be simple in Lean, the number theory that I used is simple as well and the consequences are huge. I hope @Yury G. Kudryashov might be able to understand what I tried to say in my previous messages. I saw he is a moderator, so I feel confident to receive the help I need...

[Frank Vega]

@Johan Commelin any comment, critics, advice, help is welcome. I appreciate the willing to help from you and @Yury G. Kudryashov
I think everybody would need these libraries in order to create and compile the function $H(n, k)$:

import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
 ```
I hope this might help....

[Frank Vega]

@Johan Commelin I saw you are an administrator here: so you and @Yury G. Kudryashov must have plenty experience in Lean.
Thanks in advance.... (see you)

[Frank Vega]

@Johan Commelin and @Yury G. Kudryashov I invite you to post your proof of my inequality here if you wish or by direct message: I don't have any problem to have several authors in my work or project.

[Eric Rodriguez]

Frank Vega said:

Yury G. Kudryashov the paper has only one theorem (Theorem 1). The end of Theorem 1 is the following conclusions:
The Goldbach's conjecture is equivalent to state the inequality

$$\frac{2 \cdot n}{e^{\gamma} \cdot (n - k) \cdot \log \log (n - k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n \geq 0$$

holds whenever $(n + k)$ is prime, $(n - k) \geq 11$ and $n > 2 \cdot 10^{18}$ (under these conditions $(n- k)$ is necessarily prime). It is not in the way of (this theorem => Goldbach's conjecture) because the theorem is proven that is true: what we do not know is whether the previous inequality always holds. Thanks in advance.

Frank, do you have a paper proof of this? Or are you claiming Lean has done this using AI? Because you have not imported any of the AI-powered tactics that have been written in Lean, so this second option is impossible.

[Yaël Dillies]

I think Frank is claiming their inequality implies Goldbach and that this inequality is probably easier to prove than Robin's criterion. I don't think they're claiming they have a proof of that inequality nor of Goldbach.

[Frank Vega]

@Eric Rodriguez Yes I have a paper proof of that (the first option). In the paper everything is fine except the Lean code which tries to prove the previous inequality. Take a look if you wish (it is easy to understand): Poof of Goldbach;s conjecture

[Frank Vega]

@Yaël Dillies is OK if you think that: I don't feel offended about it. I would be indeed worried if you might find a math flaw, but I guess maybe that would not be the case. Now, I'm focusing in the help that @Johan Commelin or @Yury G. Kudryashov might provide in order to collaborate together (it is not another Polymath project, but for me their help is quite enough). Thank you for your opinion.

[Johan Commelin]

@Frank Vega Let me be clear about one thing: I don't have time/energy/motivation to write Lean code for your project.
But I'm happy to answer a few of your questions about Lean. I think it's best if you start a new Lean project (follow the instructions on the website) and collect/organize your code there.

[Johan Commelin]

As I wrote before, your H is not very readable. It should be possible to make it look a lot more like your LaTeX formula

[Frank Vega]

@Johan Commelin thank you for letting me know!

[Frank Vega]

@Johan Commelin one question. How can I fill this theorem:

theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (p : Prop := Goldbach_Decide n k) (q: Prop := Nat.Prime (n - k)) (hp : p) (hq : q) : p  →  q := sorry

I saw in the doc you might apply something like

intro hp
exact hq

However, it is not working for me.
This my first question: Thanks in advance....

[Eric Rodriguez]

Frank Vega said:

Johan Commelin one question. How can I fill this theorem:

theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (p : Prop := Goldbach_Decide n k) (q: Prop := Nat.Prime (n - k)) (hp : p) (hq : q) : p  →  q := sorry

I saw in the doc you might apply something like

intro hp
exact hq

However, it is not working for me.
This my first question: Thanks in advance....

To be clear: this theorem is _not_ the theorem that Goldbach_Decide n k implies Nat.prime (n - k).

[Frank Vega]

Eric Wieser said:

Frank Vega said:

What is the correct answer here (how would you fill the "sorry" statement in the previous code)?
Thanks in advance...

When you write theorem bad (p : Prop := Goldbach_Decide n k) : p := sorry this means something very different to theorem ok : Goldbach_Decide n k := sorry. The first says "let p be any proposition (and if you forget to tell me which one, I'll use GoldBach_Decide). I will prove this arbitrary p". The second says "I will prove GoldBach_Decide".

Second question: it is still bad that theorem bad (p : Prop := Goldbach_Decide n k) : p := sorry when we replace sorry by exact p (etc)

[Eric Rodriguez]

theorem bad (p : Prop := Goldbach_Decide n k) : p := sorry is false.

[Frank Vega]

@Eric Rodriguez suppose to do this:

theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)]: Goldbach_Decide n k  →  Nat.Prime (n - k)  := sorry

where Goldbach_Decide n k and Nat.Prime (n - k) are propositions well defined. How can I introduce the proof! (a hint?)

[Frank Vega]

@Johan Commelin Here you have what you have suggested for:

/-- Goldbach function. -/
noncomputable def H (n k : ℝ): ℝ := (n/(n - k))/((Real.log (Real.log (n - k)))/1.1229) + n^0.889 + (n - k - 1)/2 + 1 - n

[Johan Commelin]

Frank Vega said:

Johan Commelin one question. How can I fill this theorem:

theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (p : Prop := Goldbach_Decide n k) (q: Prop := Nat.Prime (n - k)) (hp : p) (hq : q) : p  →  q := sorry

I saw in the doc you might apply something like

intro hp
exact hq

However, it is not working for me.
This my first question: Thanks in advance....

@Frank Vega I strongly suggest that you work through the Natural Number Game and other tutorials. You are trying to swim across the channel... but you should first try to swim across the swimming pool.

[Yury G. Kudryashov]

Let me repeat once more: at the moment, Lean has no AI that will prove the inequality for you. You need to prove it on paper first, then optionally formalize your proof in Lean.

[Frank Vega]

@Johan Commelin after playing a little with the Natural Number Game and I got this:

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic

/-- Goldbach function. -/
noncomputable def H (n k : ℝ): ℝ := (n/(n - k))/((Real.log (Real.log (n - k)))/1.1229) + n^0.889 + (n - k - 1)/2 + 1 - n

/-- Goldbach decision. -/
noncomputable def Goldbach_Decide (n k: ℕ): Prop :=
(n - k >= 11 && (H n k) >= 0 && Nat.Prime (n + k))

/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] (h: Goldbach_Decide n k -> Nat.Prime (n - k)) : Goldbach_Decide n k -> Nat.Prime (n - k) :=
by intro p
   apply h p

I believe I'm making some progress... (but no so far yet)

[Eric Rodriguez]

Your h is the implication itself. The theorem that you should prove is:

/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] : Goldbach_Decide n k -> Nat.Prime (n - k) :=

[Frank Vega]

@Eric Rodriguez thank you so much. I tried this:

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic

/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] [Fact (n + k).Prime] [Fact (n - k >= 11)] (x := (n/(n - k))/((Real.log (Real.log (n - k)))/1.1229) + n^0.889 + (n - k - 1)/2 + 1 - n) (h : x >= 0 ↔ Nat.Prime (n - k)): x >= 0 ↔ Nat.Prime (n - k) := by
  cases' h with hp hq
  · exact Iff.intro hp hq

Is better now? Or I need to go further?

[Frank Vega]

@Eric Rodriguez this would be my last propose:

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Init.Core
/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} [Fact (n > 2000000000000000000)] [Fact (n + k).Prime] [Fact (n - k >= 11)] (x := (n/(n - k))/((Real.log (Real.log (n - k)))/1.1229) + n^0.889 + (n - k - 1)/2 + 1 - n) (h : x >= 0 ↔ Nat.Prime (n - k)): x >= 0 ↔ Nat.Prime (n - k) := by
  cases' h with hp hq
  · exact Iff.intro hp hq

What do you think? Thanks in advance...

[Eric Rodriguez]

No, I think every member of this community would agree that the only correct statement for what you claim to be the case is the one I posted. And the proof will be far longer than two lines, if it exists.

[Kyle Miller]

That's a proof, but it's not a proof of the Goldbach conjecture. You proved that "assuming x >= 0 ↔ Nat.Prime (n - k), then x >= 0 ↔ Nat.Prime (n - k)". This is a trivial tautology, and there's no need for a roundabout cases proof. It could just be exact h.

I'll assume you're correct with your equivalent statement of the conjecture. In that case, this is what you need to complete (modulo errors on my part from not having read this thread carefully):

import Mathlib.Data.Nat.Prime
import Mathlib.Data.Real.Basic
import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Log.Basic
import Init.Core
/-- Goldbach conjecture. -/
theorem Goldbach_Proof {n k: ℕ} (hnLarge : n > 2000000000000000000) (hnkp : (n + k).Prime) (hnk : n - k >= 11) :
    (n/(n - k))/((Real.log (Real.log (n - k)))/1.1229) + n^0.889 + (n - k - 1)/2 + 1 - n >= 0 ↔ Nat.Prime (n - k) := by
  -- fill in the proof

[Kyle Miller]

If you can fill in the proof without touching anything between theorem and := (without using sorry of course :smile:), then you might be on to something.

[Jireh Loreaux]

@Frank Vega you are missing a key point which has been communicated several times, so I'll just say it once more and that will be my only contribution to this conversation: if the proof in Lean that you provide has very little content (for a new and substantial mathematical result), then you didn't prove anything mathematically meaningful. Lean is not an automated theorem prover, it's an interactive theorem prover. You can't just write the statement and in two or three lines say "Prove it for me." That's not how it works. For simple problems or certain problems with decision procedures, we have tactics that can do some helpful work (e.g., linarith, norm_num, ring), but intro, apply or exact are not these tactics, and even with the "powerful" tactics, any proof of the theorem from your paper will take a considerable (say, easily > 50-100 lines, probably likely much more; I haven't evaluated your argument carefully) amount of coding on your part.

[Dan Velleman]

Frank Vega says he is interested in whether or not

$$\frac{2 \cdot n}{e^\gamma \cdot (n-k) \cdot \log\log(n-k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n \ge 0$$

holds whenever $n + k$ is prime, $n - k \ge 11$, and $n > 2 \cdot 10^{18}$. The answer is no; in fact, the inequality is false if $n-k \ge 11$ and $n > 7000$.

Proof: If $n - k \ge 11$ then $e^\gamma \cdot (n - k) \cdot \log\log (n-k) \ge e^\gamma \cdot 11 \cdot \log\log 11 \approx 17.135 > 16$. Therefore

$$\frac{2 \cdot n}{e^\gamma \cdot (n-k) \cdot \log\log(n-k)} + n^{0.889} + 1 + \frac{n - k - 1}{2} - n < \frac{2 \cdot n}{16} + n^{0.889} + 1 + \frac{n}{2} - n.$$

But

$$\frac{2 \cdot n}{16} + n^{0.889} + 1 + \frac{n}{2} - n = n^{0.889} + 1 - \frac{3n}{8} = n^{0.889}\left(1 + \frac{1}{n^{0.889}} - \frac{3n^{0.111}}{8}\right)$$

Now, the quantity in parentheses above clearly decreases as $n$ increases, and it is negative when $n = 7000$. Therefore if is negative for all $n > 7000$.

[Frank Vega]

@Dan Velleman thank you so much. I understood that I actually showed that $\textit{False} \rightarrow \textit{Goldbach's conjecture}$ since the inequality is indeed false for $n > 2 \cdot 10^{18}$ as you gently and clearly showed. For that reason, there is no merit in my approach even though the steps to get there might be correct. Thank you all to show me that Lean is only a proof assistant and not a magical theorem proof generator using artificial intelligence. Best wishes, Frank....

[Bulhwi Cha]

Well, I prefer handwork to magic!