Formalizing Goldbach Conjecture Basics - Seeking Feedback

Stream: new members

[Frank Vega]

As a Lean learner, I've created a small project around Goldbach's Conjecture: GoldbachConjecture

What's included:

• Formal definitions related to the conjecture
• Proofs of some basic properties
• A structure for investigating specific even numbers

I wrote all the code manually as part of my Lean education.
Would love feedback on whether this approach follows mathlib conventions
or how I might improve the proof techniques.

[Mirek Olšák]

It is quite non-standard to use axioms. If these are results that should be true but you haven't proven them yet, then write theorem thm_name : thm_statement := sorry. If it is an assumption that some add as an extra assumption but we have no idea if it holds, then add it explicitly as an assumption (you could define the proposition representing it).

[Frank Vega]

@Mirek Olšák Thank you: I will change it right now!

[Frank Vega]

@Mirek Olšák I've updated the code to replace axioms with sorry or explicit assumptions where appropriate. Regarding the statements based on experimental results: I kept those as axioms since they're computational calculations rather than mathematical proofs. Should I convert them as well? Thanks for your guidance!

[Weiyi Wang]

:sweat_smile: It is quite hard to grasp what the file actually proved when there are that many axiom / sorries

[Frank Vega]

@Weiyi Wang maybe this preprint accepted in a moderated preprint server could help to understand better: Geometric Insights into the Goldbach Conjecture

[Mirek Olšák]

I would also close them with sorry, with the intention of eventually letting Lean do the calculation too. How much HW-demanding are these calculations?

[Frank Vega]

@Mirek Olšák I've updated the code following your feedback on axioms. Regarding the experimental results: I'm including the Python script used for computational verification. This approach reminds me of the Goldbach partition verification example in Lean's documentation - while different, it might provide a similar foundation for building confidence in those statements. The Python code is attached: experiment.py and also the logging output: experimental_results.txt I'm considering whether this computational verification could be formalized in Lean itself as part of the proof strategy.

[Frank Vega]

I should mention that my formalization likely has gaps. Specifically, the Corollary in my code depends on Theorem 2 from the referenced preprint, and I haven't fully formalized that dependency. I'm hoping for guidance on how to properly connect these results in Lean. The current implementation might be incomplete or incorrect in this regard—this is a genuine mathematical gap I'm trying to bridge, not automated code generation.

[Frank Vega]

Now, I have created the Theorem that supports the Corollary: I used ":= sorry" in this case.

[Frank Vega]

Complete Theorem 2 based on analytics assumptions where I used ":= sorry". However, I think it could be do it better.

[Frank Vega]

@Mirek Olšák I uploaded the experimental data results in lean. Thank you for your pieces of advice!

[Mirek Olšák]

I still don't understand something -- are you claiming that you have proved Goldbach conjecture? The theorem

/-- Corollary: Every even integer ≥ 8 is sum of two distinct primes -/
theorem goldbach_for_even_integers :
    ∀ n : ℕ, n ≥ 8 → Even n →
    ∃ p q : ℕ, Nat.Prime p ∧ Nat.Prime q ∧ p ≠ q ∧ p + q = n := by

looks like that. I thought you have proven it under some extra assumption.

[Mirek Olšák]

By the way, the first lemma is quite straightforward

/-- Area of L-shaped region: N² - M² = (N-M)(N+M) -/
theorem LShape_area (N M : ℕ) (hN : N ≥ M + 3) :
    N^2 - M^2 = (N - M) * (N + M) := by
  zify
  have le : M ≤ N := by linarith
  have le2 : M^2 ≤ N^2 := by gcongr
  rw [Int.ofNat_sub le2, Int.ofNat_sub le]
  push_cast
  ring

[Mirek Olšák]

I would distinguish

• Easy results / results within the scope of the article. These should be temporarily filled with sorry, and you should work on filling them with actual proofs.
• Deep theoretical results, something about prime distribution. Lean can have something in its library too (check with leansearch.net) but probably not as much as you need. Then I think it is fine to write those as axiom, and add a mathematical reference to the doc-string where this result can be found. As far as I know, @Kevin Buzzard is doing something similar with FLT.
• Computational results. So far, fill it with sorry too. Eventually, there are two ways of proving it with Lean
  * (a) Write the search algorithm in Lean in a way it can be reasoned about. Then executing it through kernel will probably not be feasible, so you will prove that the algorithm outputs what it outputs using native_decide. This is considered less trustworthy but should be fine.
  * (b) Write a meta-code that builds the proofs efficiently. First, you could write a code that builds plenty of lemmas about numbers below 2^15 being a prime or not -- you prove this with an optimized short proof, explicit decomposition for a non-prime, only checking primes below square root for primes. Then it could be possible to efficiently (constant time per number) prove Golbach-like claims for numbers below 2^15.
• Conjectures. If your proof of Goldbach conjecture depends on some other conjectures (I expect that, Goldbach conjecture is a long-standing open problem), state them as assumptions, and do not hide them with axioms / sorries.

[Snir Broshi]

Mirek Olšák said:

By the way, the first lemma is quite straightforward

/-- Area of L-shaped region: N² - M² = (N-M)(N+M) -/
theorem LShape_area (N M : ℕ) (hN : N ≥ M + 3) :
    N^2 - M^2 = (N - M) * (N + M) := by
  zify
  have le : M ≤ N := by linarith
  have le2 : M^2 ≤ N^2 := by gcongr
  rw [Int.ofNat_sub le2, Int.ofNat_sub le]
  push_cast
  ring

Maybe we should add a version of docs#sq_sub_sq for semirings?

[Eric Wieser]

we have it already, docs#sq_tsub_sq:

theorem LShape_area (N M : ℕ) (_hN : N ≥ M + 3) :
    N^2 - M^2 = (N - M) * (N + M) := by
  rw [sq_tsub_sq, mul_comm]

[suhr]

Mirek Olšák said:

I would distinguish

It seems like we need more guidelines in addition to https://leanprover-community.github.io/did_you_prove_it.html. Not only about whether something is proved but also about how to work on a problem.

[Frank Vega]

@Mirek Olšák I have written the Deep theoretical results as axiom as you suggested. Honestly, I cannot assure without any doubt that the preprint paper Geometric Insights into the Goldbach Conjecture is a complete/valid proof: I'm skeptical about it. However, I hope you/we/I could be able to formalize in Lean since it is based on well-known analytical results.

[Frank Vega]

@suhr @Eric Wieser @Snir Broshi Thank you for your feedback and guidance too.

[Mirek Olšák]

Pidgeonhole principle, and a bound on log are not any deep theoretical results. These are among the "simple facts" that you can prove in Lean with more or less effort (so I don't see any reason why they should be axioms).

[Frank Vega]

@Mirek Olšák you are right!

[Mirek Olšák]

On the other hand, you still didn't address my main mystery -- do you

• claim that Goldbach conjecture is true
• you know how to prove it,
• and are trying to write the main part of the proof in Lean?

[Frank Vega]

@Mirek Olšák The answer is yes. However, I don't want to sound too pretentious.

[Mirek Olšák]

Good luck then. As I said, first try to fill the remaining mathematical sorries except the three prime density results. Second step would be convincing Lean of the calculation facts (happy to help), and then maybe looking at the library results too -- that might be too hard, needing number theorists... but at that point, people could have a reasonable confidence that it works.

[Mirek Olšák]

I have noticed that in prime_counting_lower_bound, if you want to follow the assumption from the source, it should be N ≥ 18, because you shifted by 1. On the other hand, experimentally, it seems to be true since 12, so I don't know how they came up with 17...

[Mirek Olšák]

And I don't quite understand what you are trying to say with the Dussart prime density:

axiom dusart_prime_density (n : ℕ) (hn : n ≥ 3275) :
    ∃ (k : ℕ), k ≥ 2 * (Real.log n)^2 ∧
    ∀ i < k, ∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

To me, it looks like Bertrand's postulate, with some dummy quantifiers around. the k and i is not used anywhere, right?

[Mirek Olšák]

Note that Lean has Bertrand's postulate: Nat.bertrand (n : ℕ) (hn0 : n ≠ 0) : ∃ p, Nat.Prime p ∧ n < p ∧ p ≤ 2 * n

[Mirek Olšák]

So if the hardest theoretical result this depends on is $\pi(n) > n / \log(n)$, for $n \ge 11$ then it should be possible to fully formalize in Lean (assuming there is no mistake).

[Mirek Olšák]

I guess you are interested in the primeCounting of the interval, but I would prefer if the axiom theorems were closely matching the library results, so we can easily check that they are valid. So rather than counting, write that the interval (n, n + n/(2·log²n) has a prime number (as a library axiom), and then prove whatever you want from that.

[Frank Vega]

@Mirek Olšákthe dussart theorem is basically to support the current theorem and another one similar:

/-- Theorem: Growth rate of |D_N| based on Bertrand-type results.
    Over intervals [N, 2N], |D_N| grows by at least Ω(N/log²N) on average. -/
theorem card_D_N_growth (N : ℕ) (hN : N ≥ 25) :
    ∃ (c : ℝ), c > 0 ∧
    (card_D_N (2 * N) : ℝ) ≥ (card_D_N N : ℝ) + c * (N : ℝ) / (Real.log N)^2 := by
  sorry -- This follows from combining Bertrand's postulate refinements with prime pairing analysis

In this way, the dussart theorem is basically used to sustain the growing by at least Ω(N/log²N) on average.

[Frank Vega]

I have also created a lean code for the experimental results: maybe you could start from that point [I'm happy also that you could collaborate on this too]. Here it is that lean code:
Experimental.lean

[Frank Vega]

Your question reminds me that the purpose of the axiom that you mention:

axiom prime_counting_lower_bound (N : ℕ) (hN : N ≥ 17) :
    (Nat.primeCounting (N - 1) : ℝ) > (N - 1) / Real.log (N - 1)

is for proving a chain of inequalities

(Nat.primeCounting (N - 1) : ℝ) > (N - 1) / Real.log (N - 1)  > (Real.log (2 * N))^2

and thus using the pigeonhole_principle to support that the "good" values overcome the "bad ones".

[Mirek Olšák]

It feels a bit overcomplicated, I don't need plenty of code to generate primes in an interval (that I would then need to reason about),

#eval ((List.range (2^15)).filter Nat.Prime).length  -- 3512

[Mirek Olšák]

To be honest, I haven't yet decided on how much I should believe it will work out. But if you would like me to look at the computational results, could you write down the list of all computational results you need for the full proof (and the relevant definitions) but without any other lemmas. I prefer looking directly at the math rather than code.

[Mirek Olšák]

I expect letting Lean verify the computation should be reasonably easy (as long as we are fine with native_decide). Only we will have to detach the float arithmetics from it -- Lean cannot really mix proofs with floats.

[Frank Vega]

@Mirek Olšák right now, I'm struggling just filling these theorems:

theorem ratio_bound (N : ℕ) (hN : N ≥ 2 ^ 10) :
    (N : ℝ) / Real.log N > (Real.log (2 * N))^2 := by
  sorry

theorem pigeonhole_principle (N : ℕ) (hN : N ≥ 4)
    (h_exceed : (numCandidates N : ℝ) > (N - 3 : ℝ) - (card_D_N N : ℝ)) :
    ∃ P, Nat.Prime P ∧ 3 ≤ P ∧ P < N ∧ (N - P) ∈ D_N N := by
  sorry

I realized they might be easy to prove for a senior and even a junior in lean. If you feel that is feasible to help me on that part and maybe omit the experimental results, then it will be less painful moving forward and doing better.

[Mirek Olšák]

Regarding ratio_bound, it is indeed somewhat annoying, as far as I know, Lean doesn't have a tool for this, so you have to prove it manually. First, write down a detailed proof of this on paper (how you rewrite, substitute, ...) without relying on a calculator. Eventually, it could be simplified to some basic inequality like $x+1 \le e^x$.

[Frank Vega]

@Mirek Olšák I will put all the details that we may find during the formalization, but to avoid multiple versions with only minor details, then it is better to consider all of them in the preprint at the end of this process. Nevertheless, I could explain you how can we prove that in math. It is simple: we only need to prove that the function (i.e., the subtraction instead of an inequality)

(N : ℝ) / Real.log N - (Real.log (2 * N))^2

is increasing and positive for the value N =2 ^ 10 which immediately will prove this for all N in the interval:

N ≥ 2 ^ 10

To prove that is increasing you could check whether the derivative s greater than 0 in the interval [2^10, infinity]. I guess it's not so easier to formalize in lean: I hope this comment could help.

[Mirek Olšák]

There are also more elementary ways, you don't have to pull up canons like derivatives.

[Mirek Olšák]

Just basic estimates & rearrangements.

[Mirek Olšák]

But yes, it is more annoying than one would like...

[Frank Vega]

@Mirek Olšák I think it is wiser to lead all that part until the end and focus in theorems which are with "sorry" at this moment in order to gain confidence by ourselves and for others who might be able to check later. For example, these theorems are fundamentals for the math proof:

/-- Theorem: Growth rate of |D_N| based on Bertrand-type results.
    Over intervals [N, 2N], |D_N| grows by at least Ω(N/log²N) on average. -/
theorem card_D_N_growth (N : ℕ) (hN : N ≥ 25) :
    ∃ (c : ℝ), c > 0 ∧
    (card_D_N (2 * N) : ℝ) ≥ (card_D_N N : ℝ) + c * (N : ℝ) / (Real.log N)^2 := by
  sorry -- This follows from combining Bertrand's postulate refinements with prime pairing analysis

/-- Helper: G(N) increases on average due to |D_N| growth outpacing linear growth -/
lemma G_growth_from_card_D_N (N : ℕ) (hN : N ≥ 25) :
    ∃ (c : ℝ), c > 0 ∧ G (2 * N) ≥ G N + c / (Real.log N)^2 := by
  obtain ⟨c, hc_pos, hgrowth⟩ := card_D_N_growth N hN
  use c
  constructor
  · exact hc_pos
  · unfold G
    -- G(N) = log²(2N) - ((N-3) - |D_N|)
    -- The growth in |D_N| by c·N/log²N over interval [N, 2N]
    -- outpaces the linear growth in (N-3), after accounting for
    -- the logarithmic increase in log²(2N)
    sorry
/--
On a dyadic scale `2^m ≥ 25`, the growth lemma at `2^m`
actually forces a uniform lower bound on the whole next dyadic interval
`[2^(m+1), 2^(m+2)]`. This is the analytic strengthening we need. -/
lemma G_growth_on_next_dyadic_interval
    (m : ℕ) (hm : m ≥ 2) (hlarge : 2 ^ m ≥ 25)
    (c : ℝ) (hc_pos : 0 < c)
    (hgrowth : G (2 * 2 ^ m) ≥ G (2 ^ m) + c / (Real.log (2 ^ m)) ^ 2) :
    ∀ ⦃N : ℕ⦄, 2^(m+1) ≤ N → N ≤ 2^(m+2) →
      G N ≥ G (2^m) + c / (Real.log (2^m))^2 :=
by
  -- This is where the extra analytic input would go.
  sorry

/-- Theorem: G(N) is monotonically increasing in the minimum across dyadic intervals -/
theorem G_increasing_dyadic_minima (N : ℕ) (hN : N ≥ 4) :
    ∃ (m : ℕ), 2^m ≤ N ∧ N < 2^(m+1) ∧ G N > 0 := by
  sorry

If we achieve to formalize them, then everything else are only details that can be assumed as correct right now.

[Mirek Olšák]

Sure, focus on what you consider important at the moment. I was looking at the pidgeonhole which also needs quite some massaging but looks doable. You understand your proof, I don't, so follow your math proof, and ask if you will need something Lean-specific, ideally possible to express without much other context.

[Frank Vega]

I'm going to take a break now and come back with more intensity next few days. I hope we'll stay in touch via this web site through this chat: Thanks a lot in advance for that!

[Eric Wieser]

Is this a continuation of https://leanprover.zulipchat.com/#narrow/channel/116395-maths/topic/Lean.20on.20Goldbach's.20conjecture/near/388817318?

[Frank Vega]

@Eric Wieser no, it is not the same.

[Eric Wieser]

But I assume you are the same Frank Vega?

[Frank Vega]

@Eric Wieser I was banned for the same information I shared in this current channel. My first intention was trying to do it as a continuation in the thread that you mentioned above, but my original account was banned forever in Zulip and my new messages were all deleted. In those messages, I was also trying to explain to @Yury G. Kudryashov that I have actually a possible proof since he asked me for a concrete demonstration in that thread. @Mirek Olšák I restored the axiom tactic into the GitHub Repository under a possible ban in Zulip again. I really would like to learn Lean and at least try to formalize my attempts and discover some possible flaws during that process, but it is difficult for doing here (in this community) because of their drastic moderation.

[Ruben Van de Velde]

You realize that creating a new account to avoid a ban is also a bannable offence? @maintainers

[Patrick Massot]

@Frank Vega your first account was suspended for 24 hours and has been reactivated since then. Please delete your second account and stop posting that kind of very low effort content.

[Mirek Olšák]

What a mess... I have to admit that I would be even more skeptical & reluctant if I interacted with @Frank Vega / @Frank Vega in the previous thread, I can understand that moderators couldn't stand it anymore. But if it was just a temporary ban (which makes much more sense) I agree with Patrick Massot that you should go back to use your original account (only).

On the other hand, that also implies that I consider the quality of this thread better than the previous one. Unfortunately, I don't know how much Lean you actually know, or if all the proofs in GoldbachConjecture.lean are AI-generated. In case you understand how to write proofs such as those in your repository, then you should be able to work on the rest mostly yourself, and ask for help with specific questions.

For example, the two problems ratio_bound & pigeonhole_principle are in my view reasonable beginner questions. Just with the latter, it helps a lot when you abstract away your definitions, and ask something like the approach for

theorem pigeonhole_principle (A B : Set ℕ) (N : ℕ) (hN : N ≥ 4)
    (h_exceed : (Nat.card {n : ℕ | n ≤ N - 1 ∧ n ∈ A} : ℤ) - 1 > (N - 3) - (Nat.card {M | M ∈ B ∧ M ≤ N - 3} : ℤ)) :
    ∃ x, x ∈ A ∧ 2 ≠ x ∧ x < N ∧ (N - x) ∈ B := by
  sorry

(which is false by the way, N = 4, A = {2,3}, B = {0}, but almost, you will need to find a question which is true)

I do suspect that most likely, there is something wrong with the main math argument. That is why I am saying that if (which is a big if) you manage to get the proof depending only on literature results & computation, you could be really up to something.

@Mirek Olšák I restored the axiom tactic into the GitHub Repository under a possible ban in Zulip again

Sorry, this sentence is a nonsense. axiom is not a tactic, and there is no connection between using / not using it, and a ban.

[Frank Vega]

Back to my original account. Sorry for that mess and thanks for the understanding and consideration about it. @Mirek Olšák you are right: I only need to remark to your comments that the original math proof does not apply to pigeonhole principle starting for 4 but for 328 to overcome the lower magnitude \ln^2(2n) using a better refinement of Dusart result:

$$\pi(n) > \frac{n}{\ln(n) + 2}$$

for n greater than or equal to 6. I decided to use 2 ^ 10 instead of 328 to simplify more the proof and to use a well-known result instead, that is

$$\pi(n) > \frac{n}{\ln(n)}$$

for n greater than or equal to 18 (I introduced N ≥ 4 by mistake in the lean code and not in the math argument).

[Mirek Olšák]

To be honest, I don't think the PHP would be the main issue because it looks just as some off-by-constant error, which should be possible to fix in the asymptotic arguments. But you should realize that we are not really here to judge a math proof of an open problem, nor to be searching for mistakes in it. We are here to help with Lean.

So just focus on one of your sorries, work on filling it, and when you get stuck, ask for a help with a minimal example. If you focus on a sorry which is more mathematically challenging, and therefore closer to a potential issue, good for you. Just bare in mind that the minimal example should be obviously mathematically true, and ideally not depending on extra definitions. Try to ask about single steps in Lean (which are typically even more basic than single steps in math).

[Frank Vega]

@Mirek Olšák Of course, it is as you remarked: The purpose is to formalize my math proof using Lean. If it turns out that the math proof is flawed, then something good could come out over all this (i.e., I will learn lean) :+1:

[Bbbbbbbbba]

Mirek Olšák said:

Regarding ratio_bound, it is indeed somewhat annoying, as far as I know, Lean doesn't have a tool for this, so you have to prove it manually. First, write down a detailed proof of this on paper (how you rewrite, substitute, ...) without relying on a calculator. Eventually, it could be simplified to some basic inequality like $x+1 \le e^x$.

I am trying to do this as a beginner's exercise, and I find that eventually it boils down to something like $\forall x > x_0, x^c < e^x$, where $c$ and $x_0$ are constants. Does Mathlib have lemmas that help with this part or could it be further simplified? I think if I really want I could prove this by induction on something like $\lfloor x \rfloor$ but that seems like it would be worse than using derivatives.

[Aaron Liu]

we have docs#Real.pow_div_factorial_le_exp

[suhr]

Frank Vega said:

If it turns out that the math proof is flawed, then something good could come out over all this (i.e., I will learn lean) :+1:

A flawed proof is not the end of the story though: every flawed proof demands a counterexample.

[Bbbbbbbbba]

import Mathlib

theorem ratio_bound (N : ℕ) (hN : N ≥ 2 ^ 10) :
    (N : ℝ) / Real.log N > (Real.log (2 * N))^2 := by
  rify at hN
  have h_nonneg : 0 ≤ (N : ℝ) := Nat.cast_nonneg' N
  have h_pos : 0 < (N : ℝ) := lt_of_lt_of_le (by norm_num) hN
  apply (lt_div_iff₀ ((Real.log_pos_iff h_nonneg).mpr (lt_of_lt_of_le (by norm_num) hN))).mpr
  have h1 : Real.log (2 * N) ^ 2 * Real.log N ≤ Real.log (2 * N) ^ 3 := by
    rw [pow_succ (Real.log (2 * N)) 2]
    refine mul_le_mul_of_nonneg_left ?_ (sq_nonneg (Real.log (2 * N)))
    exact Real.log_le_log h_pos (le_mul_of_one_le_left h_nonneg one_le_two)
  apply lt_of_le_of_lt h1
  let x := (N : ℝ) ^ (3 : ℝ)⁻¹
  have hx : x ^ 3 = N := Eq.trans (Eq.symm (Real.rpow_ofNat x 3))
    (Real.rpow_inv_rpow h_nonneg (NeZero.ne 3))
  nth_rewrite 2 [← hx]
  apply (Odd.pow_lt_pow (Nat.odd_iff.mpr rfl)).mpr
  apply Real.exp_lt_exp.mp
  rw [Real.exp_log ((mul_pos_iff_of_pos_left zero_lt_two).mpr h_pos)]
  -- ⊢ 2 * ↑N < Real.exp x
  refine lt_of_lt_of_le ?_ (Real.pow_div_factorial_le_exp x (Real.rpow_nonneg h_nonneg 3⁻¹) 9)
  -- ⊢ 2 * ↑N < x ^ 9 / ↑(Nat.factorial 9)
  have h2 : x ^ 9 = N * (N * N) := by grind
  rw [h2]
  apply (lt_div_iff₀ (by norm_num)).mpr
  rw [mul_comm 2, mul_assoc]
  refine (mul_lt_mul_iff_of_pos_left h_pos).mpr ?_
  refine lt_of_lt_of_le ?_ (mul_le_mul hN hN (by norm_num) h_nonneg)
  norm_num

[Bbbbbbbbba]

I golfed it a little. Hopefully it does not affect the readability too much.

[Bbbbbbbbba]

I am not sure why by grind worked here but it just did...

[Bbbbbbbbba]

Finding theorems has been a pain throughout. apply? almost always returns a haystack which may or may not contain a needle. Is there any trick to this other than understanding the theorem naming schemes?

[Yan Yablonovskiy 🇺🇦]

Bbbbbbbbba said:

Finding theorems has been a pain throughout. apply? almost always returns a haystack which may or may not contain a needle. Is there any trick to this other than understanding the theorem naming schemes?

Have you been using @loogle ( accidental tag)

[loogle]

:exclamation: The backend process is starting up, please try again later...

[Bbbbbbbbba]

Never heard of it. How does it work?

[Mirek Olšák]

Yeah, I also almost never find apply? useful -- rather exact? when I know exactly the theorem I am looking for. There is

• Syntax-based search Loogle: https://loogle.lean-lang.org/
• Search with natural language (useful when you are less clear what you are searching for): https://leansearch.net/
• rw?? tactic -- when you are searching for a theorem to rewrite with

[Frank Vega]

@Bbbbbbbbba I will copy/paste your suggestion and I put the following comment above of that lean theorem [I hope it is fine in that way: Thanks!]:

-- Credit: `@Bbbbbbbbba` (Zulip thread "Formalizing Goldbach Conjecture Basics - Seeking Feedback", 2026-01-07)

[Frank Vega]

I have adapted PHP and applied the dusart prime theorem to the correct lower bounds explained here: Frank Vega said:

Back to my original account. Sorry for that mess and thanks for the understanding and consideration about it. Mirek Olšák you are right: I only need to remark to your comments that the original math proof does not apply to pigeonhole principle starting for 4 but for 328 to overcome the lower magnitude \ln^2(2n) using a better refinement of Dusart result:

$$\pi(n) > \frac{n}{\ln(n) + 2}$$

for n greater than or equal to 6. I decided to use 2 ^ 10 instead of 328 to simplify more the proof and to use a well-known result instead, that is

$$\pi(n) > \frac{n}{\ln(n)}$$

for n greater than or equal to 18 (I introduced N ≥ 4 by mistake in the lean code and not in the math argument).

[Frank Vega]

I also reduced the broader scope of the import:

import Mathlib

to a little restricted imports lines used by the "ratio_bound":

import Mathlib.Analysis.SpecialFunctions.Pow.Real
import Mathlib.Analysis.SpecialFunctions.Exp
import Mathlib.Data.Nat.Factorial.Basic
import Mathlib.Tactic