proof fail? when the goal pops up as a condition

Stream: maths

[Ralf Stephan]

Something funny happened in my formalization of the infinitude of primes by Euler (proof 4 in chapter 1 of Aigner & Ziegler's "Proofs from THE BOOK", 6th ed.): The infinitude itself is needed by the proof. Before jumping to the conclusion that the proof is defect, I'll assume that my formalization is incorrect.

image.png
The appended page from the book is marked at the critical point, where it says "Now clearly, $p_k \ge k+1$". Yes, clearly this holds for all primes, but to show it, have a look at what's needed to prove it in Lean:

import Mathlib

set_option autoImplicit false
open Set Finset Nat BigOperators Filter
variable {a b n: ℕ}

theorem zeroth_prime_eq_two : nth Nat.Prime 0 = 2 := nth_count prime_two

theorem nth_prime_ge_add_two : nth Nat.Prime n ≥ n + 2 := by
  induction' n with n ih
  . norm_num
    rw [le_iff_eq_or_lt]
    exact Or.inl zeroth_prime_eq_two.symm
  . rw [succ_eq_add_one]
    rw [ge_iff_le, ← add_le_add_iff_right 1, add_assoc] at ih
    norm_num at ih
    simp_arith
    have h : nth Nat.Prime n + 1 ≤ nth Nat.Prime (n + 1) := by
      rw [succ_le_iff, nth_lt_nth]
      exact lt_add_one n
      sorry
    exact LE.le.trans ih h

The state at the sorry:

      case hf
      a b n✝ n : ℕ
      ih : n + 3 ≤ nth Nat.Prime n + 1
      ⊢ Set.Infinite (setOf Nat.Prime)

The only idea I have is that, in the proof, the statement can be constructed to not be about $p_k$ in general, but those with $k \le \pi(x)$, but then, $x$ is not bounded, either. What is my misconception here?

[Moritz Firsching]

Isn't exact infinite_setOf_prime what you need to fill the sorry here?

[Ralf Stephan]

A workaround seems possible if there was a version of nth_lt_nth that does not depend on Set.Infinite?

[Ralf Stephan]

Moritz Firsching said:

Isn't exact infinite_setOf_prime what you need to fill the sorry here?

Yeah but use the fact to prove it---wouldn't that be cheating?

[Moritz Firsching]

Ah, I see the problem now.

[Richard Copley]

Ralf Stephan said:

The only idea I have is that, in the proof, the statement can be constructed to not be about pk​ in general, but those with k≤π(x), but then, x is not bounded, either. What is my misconception here?

You will have introduced $x$, so you will be in a context where it is a constant.

[Ruben Van de Velde]

I think the problem here is with your use of Nat.nth

[A.]

Ralf Stephan said:

A workaround seems possible if there was a version of nth_lt_nth that does not depend on Set.Infinite?

#check Nat.nth_lt_nth'

Nat.nth_lt_nth' {p : ℕ → Prop} {m n : ℕ} (hlt : m < n) (h : ∀ (hf : (setOf p).Finite), n < hf.toFinset.card) :
  nth p m < nth p n

[Ralf Stephan]

Thanks. I think now, it should work to assume a finite set of primes of suitable cardinality and work with that.

[Ralf Stephan]

And probably it's time to start a blueprint of that proof :working_on_it: , even if it's trivial for most of you.