Lean on Goldbach's Conjecture

EasyChair Preprint no. 10824, version 4

Abstract

Goldbach's conjecture is one of the most difficult unsolved problems in mathematics. This states that every even natural number greater than 2 is the sum of two prime numbers. The Goldbach's conjecture has been verified for every even number $N \leq 4 \cdot 10^{18}$. In this note, we prove that for every even number $N \geq 4 \cdot 10^{18}$, if there is a prime $p$ and a natural number $m$ such that $n < p < N - 1$, $p + m = N$, $\frac{N}{\sigma(m)} + n^{0.889} + 1 + \frac{m - 1}{2} \geq n$ and $p$ is coprime with $m$, then $m$ is necessarily a prime number when $N = 2 \cdot n$ and $\sigma(m)$ is the sum-of-divisors function of $m$. The previous inequality $\frac{N}{\sigma(m)} + n^{0.889} + 1 + \frac{m - 1}{2} \geq n$ holds whenever $\frac{N}{e^{\gamma} \cdot m \cdot \log \log m} + n^{0.889} + 1 + \frac{m - 1}{2} \geq n$ also holds and $m \geq 11$ is an odd number, where $\gamma \approx 0.57721$ is the Euler-Mascheroni constant and $\log$ is the natural logarithm. We use a Lean Programming Language Code to show that this inequality always holds for some natural number $m \geq 11$ and every even number $N > 4 \cdot 10^{18}$. In this way, 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.

Keyphrases: Euler's totient function, Goldbach's conjecture, prime numbers, sum-of-divisors function

@Booklet{EasyChair:10824,
  author = {Frank Vega},
  title = {Lean on Goldbach's Conjecture},
  howpublished = {EasyChair Preprint no. 10824},

  year = {EasyChair, 2023}}