Number theory · hard

Statement, exactly as the model and Lean see it

theorem lg_target {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) : ∃ p, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k] := by

Mathlib declaration: Nat.exists_prime_gt_modEq_one
Held-out module: Mathlib.NumberTheory.PrimesCongruentOne
Banned modules (itself + downstream): 1
Reference proof premises (reachable / held-out): 51 / 0

Traces

Each configuration's full record: what was retrieved, what the model wrote, what Lean said back.

Not verified1 model calls · 1 Lean checks · $0.00097

Attempts

sample 0 · round 0Syntax error73.7 s model time

Proof

```lean
let k := k;
let hk0 := hk0;
let n := n;
let k' := k;
let hk0' := hk0;
let n' := n;
let k'' := k;
let hk0'' := hk0;
let n'' := n;
let k''' := k;
let hk0''' := hk0;
let n''' := n;
let k'''' := k;
let hk0'''' := hk0;
let n'''' := n;
let k''''' := k;
let hk0''''' := hk0;
let n''''' := n;
let k'''''' := k;
let hk0'''''' := hk0;
let n'''''' := n;
let k''''''' := k;
let hk0''''''' := hk0;
let n''''''' := n;
let k'''''''' := k;
let hk0'''''''' := hk0;
let n'''''''' := n;
let k''''''''' := k;
let hk0''''''''' := hk0;
let n''''''''' := n;
let k'''''''''' := k;
let hk0'''''''''' := hk0;
let n'''''''''' := n;
let k''''''''''' := k;
let hk0''''''''''' := hk0;
let n''''''''''' := n;
let k'''''''''''' := k;
let hk0'''''''''''' := hk0;
let n'''''''''''' := n;
let k''''''''''''' := k;
let hk0''''''''''''' := hk0;
let n''''''''''''' := n;
let k'''''''''''''' := k;
let hk0'''''''''''''' := hk0;
let n'''''''''''''' := n;
let k''''''''''''''' := k;
let hk0''''''''''''''' := hk0;
let n''''''''''''''' := n;
let k'''''''''''''''' := k;
let hk0'''''''''''''''' := hk0;
let n'''''''''''''''' := n;
let k''''''''''''''''' := k;
let hk0''''''''''''''''' := hk0;
let n''''''''''''''''' := n;
let k'''''''''''''''''' := k;
let hk0'''''''''''''''''' := hk0;
let n'''''''''''''''''' := n;
let k''''''''''''''''''' := k;
let hk0''''''''''''''''''' := hk0;
let n''''''''''''''''''' := n;
let k'''''''''''''''''''' := k;
let hk0'''''''''''''''''''' := hk0;
let n'''''''''''''''''''' := n;
let k''''''''''''''''''''' := k;
let hk0''''''''''''''''''''' := hk0;
let n''''''''''''''''''''' := n;
let k'''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''' := n;
let k''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''''''''''''' := hk0;
let n'''''''''''''''''''''''''''''''''''''''' := n;
let k''''''''''''''''''''''''''''''''''''''''' := k;
let hk0''''''''''''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''''''''''''''''''''' := n;
let k'''''''''''''''''''''''''''''''''''''''''' := k;
let hk0'''''''''''''''''''''''''''''''''''''''''' := hk0;
let n''''''''''''''''''''''

What Lean printed (this is all the model sees on repair)

3:94: error: unsolved goals
k n : ℕ
hk0 : k ≠ 0
⊢ ∃ p, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k]
4:2: error: unexpected token '`'; expected command

Reference proof

Mathlib's own source for this declaration, shown for comparison. It may use lemmas the prover is not allowed to use.

/-- For any positive `k : ℕ` there exists an arbitrarily large prime `p` such that
`p ≡ 1 [MOD k]`. -/
theorem exists_prime_gt_modEq_one {k : ℕ} (n : ℕ) (hk0 : k ≠ 0) :
    ∃ p : ℕ, Nat.Prime p ∧ n < p ∧ p ≡ 1 [MOD k] := by
  rcases (one_le_iff_ne_zero.2 hk0).eq_or_lt with (rfl | hk1)
  · rcases exists_infinite_primes (n + 1) with ⟨p, hnp, hp⟩
    exact ⟨p, hp, hnp, modEq_one⟩
  let b := k * (n !)
  have hgt : 1 < (eval (↑b) (cyclotomic k ℤ)).natAbs := by
    rcases le_iff_exists_add'.1 hk1.le with ⟨k, rfl⟩
    have hb : 2 ≤ b := le_mul_of_le_of_one_le hk1 n.factorial_pos
    calc
      1 ≤ b - 1 := le_tsub_of_add_le_left hb
      _ < (eval (b : ℤ) (cyclotomic (k + 1) ℤ)).natAbs :=
        sub_one_lt_natAbs_cyclotomic_eval hk1 (succ_le_iff.1 hb).ne'
  let p := minFac (eval (↑b) (cyclotomic k ℤ)).natAbs
  have hprime : Fact p.Prime := ⟨minFac_prime (ne_of_lt hgt).symm⟩
  have hroot : IsRoot (cyclotomic k (ZMod p)) (castRingHom (ZMod p) b) := by
    have : ((b : ℤ) : ZMod p) = ↑(Int.castRingHom (ZMod p) b) := by simp
    rw [IsRoot.def, ← map_cyclotomic_int k (ZMod p), eval_map, coe_castRingHom,
      ← Int.cast_natCast, this, eval₂_hom, Int.coe_castRingHom, ZMod.intCast_zmod_eq_zero_iff_dvd]
    apply Int.dvd_natAbs.1
    exact mod_cast minFac_dvd (eval (↑b) (cyclotomic k ℤ)).natAbs
  have hpb : ¬p ∣ b :=
    hprime.1.coprime_iff_not_dvd.1 (coprime_of_root_cyclotomic hk0.bot_lt hroot).symm
  refine ⟨p, hprime.1, not_le.1 fun habs => ?_, ?_⟩
  · exact hpb (dvd_mul_of_dvd_right (dvd_factorial (minFac_pos _) habs) _)
  · have hdiv : orderOf (b : ZMod p) ∣ p - 1 :=
      ZMod.orderOf_dvd_card_sub_one (mt (CharP.cast_eq_zero_iff _ _ _).1 hpb)
    have : NeZero (k : ZMod p) :=
      NeZero.of_not_dvd (ZMod p) fun hpk => hpb (dvd_mul_of_dvd_left hpk _)
    have : k = orderOf (b : ZMod p) := (isRoot_cyclotomic_iff.mp hroot).eq_orderOf
    rw [← this] at hdiv
    exact ((modEq_iff_dvd' hprime.1.pos).2 hdiv).symm