Erdős problem 1212
Let be the graph with vertex set those pairs with , in which we join two vertices if the differ in only one coordinate, and there by .
No current result
No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.
Retained declaration
FormalConjectures/ErdosProblems/1212.lean∀ {a s : ℕ}, a < s → (∀ (p : ℕ), Nat.Prime p → p ∣ a → s < a + p) → a.gcd s = 1APIStatement only, no proof