/-
Copyright 2026 The Formal Conjectures Authors.
Licensed under the Apache License, Version 2.0 (the "License");
you may not use this file except in compliance with the License.
You may obtain a copy of the License at
https://www.apache.org/licenses/LICENSE-2.0
Unless required by applicable law or agreed to in writing, software
distributed under the License is distributed on an "AS IS" BASIS,
WITHOUT WARRANTIES OR CONDITIONS OF ANY KIND, either express or implied.
See the License for the specific language governing permissions and
limitations under the License.
-/
import FormalConjecturesUtilBen Green's Open Problem 37
What is the smallest subset of ℕ containing, for each d = 1, …, N,
an arithmetic progression of length k with common difference d?
namespace Green37
open Set Filteropen scoped Asymptotics
A contains an arithmetic progression of length k and common difference d for every d ∈ {1, …, N}.
def IsAPCover (A : Set ℕ) (N k : ℕ) : Prop := ∀ d, 1 ≤ d ∧ d ≤ N → Set.ContainsAP A k d
The minimum size of a subset of ℕ that contains, for each d = 1, …, N,
an arithmetic progression of length k with common difference d.
noncomputable def m (N k : ℕ) : ℕ :=
sInf { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k }
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.
@[category research open, AMS 5 11]
theorem green_37 (N k : ℕ) :
IsLeast { m | ∃ A : Finset ℕ, A.card = m ∧ IsAPCover (A : Set ℕ) N k } (answer(sorry)) := N:ℕk:ℕ⊢ IsLeast {m | ∃ A, A.card = m ∧ IsAPCover (↑A) N k} sorry
All goals completed! 🐙
Asymptotic version: determine the asymptotic behavior of m(N, k) as N grows.
The solver should determine what function f : ℕ → ℝ eventually equals (fun N ↦ (m N k : ℝ)).
@[category research open, AMS 5 11]
theorem green_37_asymptotic (k : ℕ) :
∀ᶠ N in atTop, (m N k : ℝ) = (answer(sorry) : ℕ → ℝ) N := k:ℕ⊢ ∀ᶠ (N : ℕ) in atTop, ↑(m N k) = sorry N
All goals completed! 🐙
Determine the asymptotic equivalence class (theta) of m(N, k).
@[category research open, AMS 5 11]
theorem green_37_theta (k : ℕ) :
(fun N ↦ (m N k : ℝ)) =Θ[atTop] (answer(sorry) : ℕ → ℝ) := k:ℕ⊢ (fun N => ↑(m N k)) =Θ[atTop] sorry
All goals completed! 🐙
Determine an upper bound (big O) for m(N, k).
@[category research open, AMS 5 11]
theorem green_37_bigO (k : ℕ) :
(fun N ↦ (m N k : ℝ)) =O[atTop] (answer(sorry) : ℕ → ℝ) := k:ℕ⊢ (fun N => ↑(m N k)) =O[atTop] sorry
All goals completed! 🐙
Determine a strict upper bound (little o) for m(N, k).
@[category research open, AMS 5 11]
theorem green_37_littleO (k : ℕ) :
(fun N ↦ (m N k : ℝ)) =o[atTop] (answer(sorry) : ℕ → ℝ) := k:ℕ⊢ (fun N => ↑(m N k)) =o[atTop] sorry
All goals completed! 🐙
end Green37