Combinatorics

Erdős 272 - szabo strong

Szabo asks whether the maximal

t

is given by

\frac{N^2}{2} + O(N)

References

erdosproblems.com/272

No one has attempted this yet.

Formal statement

Lean type

(fun N => ↑(Erdos272.maxArithInterCard N) - ↑N ^ 2 / 2) =O[Filter.atTop] fun N => ↑N

What you must prove

import FormalConjectures.ErdosProblems.«272»
import TaskSupport

namespace Bounty

theorem target : fcTypeOfName% "Erdos272.erdos_272.variants.szabo_strong" := by
  sorry

end Bounty

Pinned source: FormalConjectures/ErdosProblems/272.lean

Source type SHA-256: sha256:1b53f078ce5311f741606ee47a8235037e49794e856a66e40f33327d0cce9edf
Task id: fc-379fc029-variants-szabo-strong-e3a0036a0a-formalized-v1
Task commitment: sha256:241aa1911b480f31736579496a65d3ec4d785ce522a2cf64c465ff185fab6257

Something wrong with this formalization?

A statement that does not faithfully capture the original conjecture is the one real risk here, so we would rather hear about it early - before someone spends weeks on it.