frobenius_problem_conjecture
Provedadditive-combinatoricscombinatoricscomputational-complexitydiophantinegraph-theorynumber-theoryready-to-formalize
Sylvester-Frobenius theorem: The largest integer not representable as ax+by (with a,b coprime and x,y ≥ 0) is ab-a-b. Proved. For 3 or more coin denominations, the problem of finding the Frobenius number exactly is NP-hard.
Preamble
import Mathlib
Formal statement
import Mathlib
theorem frobenius_problem_conjecture (a b : ℕ) (ha : 1 ≤ a) (hb : 1 ≤ b)
(hcop : Nat.Coprime a b) :
∀ n : ℕ, a * b - a - b < n →
∃ x y : ℕ, n = a * x + b * y := by
sorrySource