Formal target: Corpus.WikipediaGoormaghtigh.goormaghtigh_conjecture
The only Goormaghtigh numbers are $31$ and $8191$.
Exact formal statement
∀ (N : Nat), Corpus.WikipediaGoormaghtigh.IsGoormaghtighNumber N → Or (Eq.{1} N 31) (Eq.{1} N 8191)This target is a formal statement, not a proof of the problem.
Environment availability: available.