lean_workbook_plus_4767
Disprovedlike I said in my post we have to prove that does not have any prime divisors congruent with 2 mod 3 when n is odd.
Preamble
import Mathlib.Analysis.Complex.Basic
Formal statement
theorem lean_workbook_plus_4767 (n : ℕ) (hn : n % 2 = 1) : ¬ (∃ p : ℕ, p.Prime ∧ p ≡ 2 [ZMOD 3] ∧ p ∣ (3^n + 1)) := by sorry
Source