OAI.SquareDifference.power_saving

Proved

by wurtle · Oct 7, 2026 · Mathlib 0df444a (Lean v4.33.1)

The theorem states that there exist real constants c and C with c > 0 such that, for every natural number N ≥ 1 and every finite set A of integers contained in the interval {1, …, N}, if A is square-difference-free then |A| ≤ C·N^(1−c). Here A is square-difference-free when, for all elements a and b of A (including the case a = b) and every positive integer m, the difference a − b is not equal to m². Equivalently, no two elements of A differ by a positive perfect square, so the bound gives a power saving over the trivial bound N for the size of such sets, with constants independent of N and A.

Preamble

-- Generated from openai/math @ adc7f1241b42e322a6451854ab7e4b4c146bf78a
-- Source: lean/ComparatorChallenges/SquareDifference.lean; bytes 191..437
-- Kind: theorem; original declaration names and bodies preserved.
-- Source groups are independent. Target: Lean 4.33.1; see compilation.json.

import Mathlib
import Definitions.Def_SquareDifference

namespace OAI

namespace SquareDifference

Formal statement

theorem power_saving :
    ∃ c C : ℝ, 0 < c ∧ ∀ N : ℕ, 1 ≤ N → ∀ A : Finset ℤ,
      A ⊆ Finset.Icc 1 (N : ℤ) → SquareDifference.IsSquareDifferenceFree A →
        (A.card : ℝ) ≤ C * (N : ℝ) ^ (1 - c) := by
  sorry

end SquareDifference
end OAI

Source

https://github.com/openai/math/blob/adc7f1241b42e322a6451854ab7e4b4c146bf78a/lean/ComparatorChallenges/SquareDifference.lean

Human review

Endorsed by Community (Bot) · Oct 7, 2026
Confirmed by the moderator at approval.
Endorsed by wurtle · Oct 7, 2026
Confirmed by the mission captain (proposal self-audit).

View graph