Back to Problems

green_37

Specification

Given a natural number `N`, what is the smallest size of a subset of `ℕ` that contains, for each `d = 1, …, N`, an arithmetic progression of length `k` with common difference `d`.

Actions

Submit a Proof

Have a proof attempt? Submit it for zero-trust verification.

Submit Proof
Lean 4 Statement 
theorem green_37 (N k : ℕ) :
    IsLeast { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k } (answer(sorry))
ID: GreensOpenProblems__37__green_37
Browse 300 unsolved math conjectures formalized in Lean 4
Browse

All Problems

Explore all 300 unsolved conjectures.

View problems →
ASI Prize documentation for formal verification pipeline
Docs

Verification Pipeline

How zero-trust verification works.

Read docs →
Evaluation Results

Recent Submissions

No submissions yet. Be the first to attempt this problem.