Download PDFOpen PDF in browserCurrent versionLean on Goldbach's ConjectureEasyChair Preprint 10824, version 15 pages•Date: September 2, 2023AbstractGoldbach'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 sumofdivisors 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 EulerMascheroni constant and $\log$ is the natural logarithm. We use the Lean Programming Language 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, sumofdivisors function
