feat(ErdosProblems): 708

[JuanMarchetto]

Closes #908

Formalizes https://www.erdosproblems.com/708

Summary

Adds FormalConjectures/ErdosProblems/708.lean with the Erdős–Surányi covering problem:

• HasCoveringSize n k / IsMinCoveringSize g: $g(n)$ is the least $k$ such that for every $A \subseteq [2,\infty) \cap \mathbb{N}$ with $|A| = n$ and every window of $\max(A)$ consecutive positive integers there is some $B$ inside the window with $|B| \le k$ and $\prod_{a\in A} a \mid \prod_{b \in B} b$. The statements take IsMinCoveringSize g as a hypothesis (that some finite $k$ works for every $A$ is itself a theorem of [ErSu59]), following the hypothesis-function pattern of 126.lean.
• erdos_708.parts.i (research open): is $g(n) \le (2+o(1))n$?
• erdos_708.parts.ii (research open): or perhaps even $g(n) \le 2n$?
• erdos_708.variants.lower_bound (research solved): $g(n) \ge (2-o(1))n$ [ErSu59].
• erdos_708.variants.g_two (research solved): $g(2) = 2$ (Gallai).
• erdos_708.variants.g_three (research solved): $g(3) = 4$ [ErSu59].
• erdos_708.variants.g_one (test): $g(1) = 1$, a sanity check for the definitions.

Implementation notes (also documented in the docstrings):

• The source states $|B| = g(n)$, but the formalization uses $|B| \le k$ so that {k | HasCoveringSize n k} is upward closed and IsLeast is the right minimum: with equality no single $k$ can serve all $A$, since e.g. $A = {2, \dots, n+1}$ forces windows of length $n + 1 < (2-o(1))n$, too short for a $B$ of the size required by the Erdős–Surányi lower bound. Padding $B$ with extra window elements preserves divisibility, so the two readings agree whenever the window is long enough.
• Windows consist of consecutive positive integers (0 < m), matching the primary formulation in [Er92c] ("for every $x \ge 0$ ... among $x+1, \dots, x+a_n$"). Allowing windows in $\mathbb{Z}$ does not change $g$: a window containing $0$ is trivially satisfiable, and a window of negative integers reduces to a positive one via $b \mapsto -b$.

Verification

The full lake --wfail build (the CI command, including the repository's linters) passes with this file included, after regenerating the import index with lake exe mk_all --lib FormalConjectures.

Drafted with AI assistance (Claude) and checked against the primary sources listed in the module docstring.

🤖 Generated with Claude Code

[github-actions]

👋 This is an automated welcome message. 🤖
Thanks for the contributions!

A few friendly reminders while the review gets started:

• Please take a look at the style guidelines,
  especially the conventions for references, categories, AMS tags, and answer(sorry).
• You can manage some PR labels by leaving a comment with +label-name or -label-name; for example, +awaiting-author or -awaiting-author.
• This repository is mainly for formalised statements. Proofs longer than about 25-50 lines are usually out of scope; longer proofs are welcome to be included/linked via the formal_proof mechanism.

Thanks again for helping improve Formal Conjectures.

[google-cla]

Thanks for your pull request! It looks like this may be your first contribution to a Google open source project. Before we can look at your pull request, you'll need to sign a Contributor License Agreement (CLA).

View this failed invocation of the CLA check for more information.

For the most up to date status, view the checks section at the bottom of the pull request.

[JuanMarchetto]

@googlebot I signed it!