feat(ErdosProblems): All 1179 Erdős conjectures formalized

FIX_REVIEW_ISSUES.md

@@ -0,0 +1,120 @@
+# Fix Review Issues
+
+You are a PhD-level mathematician and Lean 4 expert. Your task is to fix all issues identified in a review for Erdős Problem **NUM**.
+
+## Inputs
+
+- **Review:** `ai-review/NUM.md`
+- **Lean file:** `FormalConjectures/ErdosProblems/NUM.lean`
+- **Library:** `FormalConjecturesForMathlib/` (shared definitions to reuse)
+- **Website:** `https://www.erdosproblems.com/NUM` (detailed problem info — variants, context, related problems)
+- **LaTeX source:** `https://www.erdosproblems.com/latex/NUM` (authoritative source for citations — most complete bibliographic data)
+
+## Instructions
+
+Read the review at `ai-review/NUM.md` in full. Then implement **all** fixes described below, working through each section in order. After completing all sections, run the verification checklist.
+
+---
+
+### Section 1: Code Reuse
+
+If the review identifies local definitions that duplicate library code:
+
+1. Find the library equivalent mentioned in the review (search Mathlib and `FormalConjecturesForMathlib/` only — do **not** look at other Erdős problem files).
+2. Read both the local definition and the library version. Confirm they are semantically equivalent or that the library version is strictly better.
+3. Delete the local definition(s).
+4. Add the necessary `import` statement(s) and `open` declarations.
+5. Rewrite the theorem statement(s) to use the library definitions.
+6. Ensure the file still compiles (`sorry` proofs are fine — the goal is correct *statements*, not proofs).
+
+If the review says "No issues" or the section has no actionable recommendations, skip this section.
+
+**Important constraints:**
+- Only import definitions that already exist in Mathlib or `FormalConjecturesForMathlib/`. Do **not** look at other Erdős problem files for code to reuse, and do **not** create new definitions in the library.
+- Preserve the existing `ErdosNUM` namespace. Every problem file uses a `namespace ErdosNUM` / `end ErdosNUM` block — do not remove or rename it, even if the local definitions it originally scoped are deleted.
+
+---
+
+### Section 2: Citations
+
+If the review identifies citation issues:
+
+1. Fetch `https://www.erdosproblems.com/latex/NUM` to get the LaTeX source with exact citations. This is the **most complete source** for bibliographic data (titles, journals, volumes, pages). You may also fetch `https://www.erdosproblems.com/NUM` for additional context, but the LaTeX endpoint has the most complete citation details. Do not search the web or use any other sources.
+2. When extracting citations from the LaTeX source, convert LaTeX-encoded names to plain text (e.g., `Erd\H{o}s` → `Erdős`, `Szemer\'edi` → `Szemerédi`, `Tur\'an` → `Turán`).
+3. For each citation issue flagged in the review:
+   - **Missing reference:** Add it to the module docstring in the standard format: `[TAG] Last, F., Last, F., _Title_. Journal **vol** (year), pages.`
+   - **Incomplete reference:** Expand it with title, journal, volume, and page numbers from the LaTeX source.
+   - **Tag mismatch:** Standardize the tag to match other files that cite the same paper. Search the codebase for the same author/year to find the canonical tag.
+4. If the review mentions missing OEIS sequences or other cross-references from the website, add them to the docstring.
+
+If the review says "No issues" or the section has no actionable recommendations, skip this section.
+
+---
+
+### Section 3: Variants
+
+If the review identifies missing variants that should be formalized:
+
+1. For each variant the review recommends adding:
+   - Write a new theorem statement with an appropriate name (e.g., `erdos_NUM_upper`, `erdos_NUM_variant`).
+   - Include a docstring explaining what the variant captures and its relationship to the main problem.
+   - Use `sorry` for the proof.
+   - Reuse existing definitions (library or local) — do not introduce new definitions unless necessary.
+2. Only add variants that the review **explicitly recommends** formalizing. Do not invent new variants.
+
+If the review says "No issues", the section has no actionable recommendations, or variants are described as "optional", skip this section.
+
+---
+
+### Section 4: Readability
+
+If the review identifies readability improvements:
+
+1. Apply each specific recommendation (e.g., renaming variables, using standard Lean/Mathlib idioms like `Odd k` instead of `k % 2 = 1`, replacing `p.1`/`p.2` with named projections).
+2. Do **not** make readability changes that conflict with Section 1 fixes (e.g., don't improve a local definition that you already deleted and replaced with a library version).
+3. Improve docstrings only if the review specifically requests it.
+
+If the review says "No issues" or the section has no actionable recommendations, skip this section.
+
+---
+
+### Section 5: Formalizability
+
+This section is informational. **No code changes needed** unless the review explicitly identifies an encoding issue that should be fixed (e.g., "the formalization encodes X but should encode Y"). In that case, fix the encoding in the theorem statement.
+
+---
+
+### Section 6: Correctness
+
+If the review identifies correctness issues:
+
+1. **This is the highest priority section.** Correctness fixes take precedence over all other changes.
+2. For each issue flagged:
+   - Read the review's explanation of why the current formalization is incorrect.
+   - Identify the correct mathematical formulation (the review will typically describe it).
+   - Rewrite the affected definition(s) and/or theorem statement(s).
+   - If the fix involves switching to a library definition (overlapping with Section 1), ensure the library version is mathematically correct per the review's analysis.
+3. If the review says "Correct and complete" or equivalent, no changes needed.
+
+---
+
+## Verification Checklist
+
+After implementing all fixes, verify each item:
+
+1. **Compiles:** Run `lake build FormalConjectures/ErdosProblems/NUM.lean` and confirm it compiles (with `sorry` proofs — warnings are OK, errors are not).
+2. **Code reuse:** Grep the file for any local definitions the review said to remove. Confirm they are gone.
+3. **Citations:** Re-read the module docstring. Confirm all references from the website are present with full bibliographic details.
+4. **Variants:** If variants were added, confirm each has a docstring and compiles.
+5. **Correctness:** If correctness issues were flagged, re-read the rewritten theorem statement and confirm it matches the review's recommended fix.
+6. **No regressions:** Ensure no other files that import this one are broken. Search for `import FormalConjectures.ErdosProblems.NUM` across the codebase.
+
+If compilation fails, diagnose and fix the error. Common issues:
+- Missing imports (add `import` statements)
+- Missing `open` declarations (add `open` for namespaces used)
+- Type mismatches from switching definitions (adjust the theorem statement to match library types)
+- Name clashes (use fully qualified names or adjust `open`/`namespace`)
+
+## Output
+
+When done, report a summary of changes made per section (1-6) and the result of each verification checklist item.

FormalConjectures/ErdosProblems/1000.lean

@@ -0,0 +1,68 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 1000
+
+*Reference:* [erdosproblems.com/1000](https://www.erdosproblems.com/1000)
+
+Let $A = \{n_1 < n_2 < \cdots\}$ be an infinite sequence of integers, and let $\varphi_A(k)$
+count the number of $1 \leq m \leq n_k$ such that the fraction $m/n_k$ does not have
+denominator $n_j$ for $j < k$ when written in lowest form; equivalently,
+$n_k / \gcd(m, n_k) \neq n_j$ for all $1 \leq j < k$.
+
+Is there a sequence $A$ such that
+$$\lim_{N \to \infty} \frac{1}{N} \sum_{k \leq N} \frac{\varphi_A(k)}{n_k} = 0?$$
+
+Erdős believed no such sequence exists. This was solved by Haight [Ha] who
+proved that such a sequence does exist (contrary to Erdős' expectations).
+
+[Er64b] Erdős, P., _Some problems in number theory_. 1964.
+
+[Ha] Haight, J. A., _A linear programming problem_. 1979.
+-/
+
+open Finset Filter
+
+namespace Erdos1000
+
+/-- For a strictly increasing sequence $a : \mathbb{N} \to \mathbb{N}$ of positive integers,
+$\varphi_A(k)$ counts the number of $1 \leq m \leq a(k)$ such that
+$a(k) / \gcd(m, a(k)) \neq a(j)$ for all $j < k$. -/
+noncomputable def phiA (a : ℕ → ℕ) (k : ℕ) : ℕ :=
+  ((Finset.Icc 1 (a k)).filter (fun m =>
+    ∀ j < k, (a k) / Nat.gcd m (a k) ≠ a j)).card
+
+/--
+Erdős Problem 1000 [Er64b]:
+
+There exists a strictly increasing sequence $A = \{n_1 < n_2 < \cdots\}$ of positive
+integers such that the Cesàro mean of $\varphi_A(k)/n_k$ tends to $0$:
+$$\lim_{N \to \infty} \frac{1}{N} \sum_{k \leq N} \frac{\varphi_A(k)}{n_k} = 0.$$
+
+Proved by Haight [Ha].
+-/
+@[category research solved, AMS 11]
+theorem erdos_1000 : answer(True) ↔
+    ∃ a : ℕ → ℕ, StrictMono a ∧ (∀ i, 0 < a i) ∧
+    Filter.Tendsto
+      (fun N : ℕ => (∑ k ∈ Finset.range N, (phiA a k : ℝ) / (a k : ℝ)) / (N : ℝ))
+      Filter.atTop (nhds 0) := by
+  sorry
+
+end Erdos1000

FormalConjectures/ErdosProblems/1001.lean

@@ -0,0 +1,97 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 1001
+
+*Reference:* [erdosproblems.com/1001](https://www.erdosproblems.com/1001)
+
+Let $S(N, A, c)$ be the Lebesgue measure of the set of $\alpha \in (0,1)$ such that
+$|\alpha - x/y| < A/y^2$
+for some $N \leq y \leq cN$ and $\gcd(x,y) = 1$. Does
+$\lim_{N \to \infty} S(N, A, c) = f(A, c)$
+exist? What is its explicit form?
+
+A problem of Erdős, Szüsz, and Turán [EST58], who proved the formula
+$f(A, c) = 12A \log c / \pi^2$
+when $0 < A < c/(1 + c^2)$.
+
+The existence of the limit was proved by Kesten and Sós [KeSo66].
+Alternative, more explicit proofs were given by Boca [Bo08] and
+Xiong–Zaharescu [XiZa06].
+
+[Er64b] Erdős, P., _Problems and results on diophantine approximations_.
+Compositio Math. (1964), 52–65.
+
+[EST58] Erdős, P., Szüsz, P., and Turán, P., _Remarks on the theory of
+diophantine approximation_. Colloq. Math. (1958), 119–126.
+
+[KeSo66] Kesten, H. and Sós, V. T., _On two problems of Erdős, Szüsz and
+Turán concerning diophantine approximations_. Acta Arith. (1966/67), 183–192.
+
+[Bo08] Boca, F. P., _A problem of Erdős, Szüsz and Turán concerning
+Diophantine approximations_. Int. J. Number Theory (2008), 691–708.
+
+[XiZa06] Xiong, M. and Zaharescu, A., _A problem of Erdős-Szüsz-Turán on
+Diophantine approximation_. Acta Arith. (2006), 163–177.
+-/
+
+open MeasureTheory Set Filter
+
+namespace Erdos1001
+
+/-- The set of $\alpha \in (0,1)$ approximable by a coprime fraction $x/y$
+    with $N \leq y \leq cN$ to within $A/y^2$. -/
+noncomputable def approxSet (N : ℕ) (A c : ℝ) : Set ℝ :=
+  {α : ℝ | α ∈ Ioo 0 1 ∧
+    ∃ (x : ℤ) (y : ℕ), N ≤ y ∧ (y : ℝ) ≤ c * N ∧
+      Nat.Coprime (Int.natAbs x) y ∧
+      |α - (x : ℝ) / (y : ℝ)| < A / ((y : ℝ) ^ 2)}
+
+/-- $S(N, A, c)$ is the Lebesgue measure of the approximation set. -/
+noncomputable def sMeasure (N : ℕ) (A c : ℝ) : ℝ :=
+  (volume (approxSet N A c)).toReal
+
+/--
+Erdős Problem 1001 [Er64b]:
+
+For all $A > 0$ and $c > 1$, the limit $\lim_{N \to \infty} S(N, A, c)$ exists.
+
+Proved by Kesten and Sós [KeSo66].
+-/
+@[category research solved, AMS 11 28]
+theorem erdos_1001 : answer(True) ↔
+    ∀ (A c : ℝ), 0 < A → 1 < c →
+      ∃ L : ℝ, Tendsto (fun N : ℕ => sMeasure N A c) atTop (nhds L) := by
+  sorry
+
+/--
+Erdős Problem 1001 — EST58 explicit formula [EST58]:
+
+When $0 < A < c/(1 + c^2)$, the limit $f(A, c) = 12A \log c / \pi^2$.
+
+Proved by Erdős, Szüsz, and Turán.
+-/
+@[category research solved, AMS 11 28]
+theorem erdos_1001_explicit_formula :
+    ∀ (A c : ℝ), 0 < A → 1 < c → A < c / (1 + c ^ 2) →
+      Tendsto (fun N : ℕ => sMeasure N A c) atTop
+        (nhds (12 * A * Real.log c / Real.pi ^ 2)) := by
+  sorry
+
+end Erdos1001

FormalConjectures/ErdosProblems/1002.lean

@@ -0,0 +1,70 @@
+/-
+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 FormalConjectures.Util.ProblemImports
+
+/-!
+# Erdős Problem 1002
+
+*Reference:* [erdosproblems.com/1002](https://www.erdosproblems.com/1002)
+
+For any $0 < \alpha < 1$, let
+$$f(\alpha, n) = \frac{1}{\log n} \sum_{1 \le k \le n} \left(\frac{1}{2} - \{\alpha k\}\right)$$
+where $\{\cdot\}$ denotes the fractional part.
+
+Does $f(\alpha, n)$ have an asymptotic distribution function? In other words, is there
+a non-decreasing function $g$ such that $g(-\infty) = 0$, $g(\infty) = 1$, and
+$$\lim_{n \to \infty} |\{\alpha \in (0,1) : f(\alpha,n) \le c\}| = g(c)$$
+where $|\cdot|$ denotes Lebesgue measure?
+
+Kesten [Ke60] proved the analogous result with an additional shift $\beta$:
+if $f(\alpha, \beta, n) = \frac{1}{\log n} \sum_{k=1}^n \left(\frac{1}{2} - \{\beta + \alpha k\}\right)$,
+then $f(\alpha, \beta, n)$ has asymptotic distribution function
+$g(c) = \frac{1}{\pi} \int_{-\infty}^{\rho c} \frac{1}{1+t^2} \, dt$
+where $\rho > 0$ is an explicit constant.
+-/
+
+open Finset Filter MeasureTheory
+
+namespace Erdos1002
+
+/-- The function $f(\alpha, n) = \frac{1}{\log n} \sum_{k=1}^{n} \left(\frac{1}{2} - \{\alpha k\}\right)$,
+where $\{\cdot\}$ denotes the fractional part. -/
+noncomputable def erdosF (α : ℝ) (n : ℕ) : ℝ :=
+  (∑ k ∈ Finset.Icc 1 n, ((1 : ℝ) / 2 - Int.fract (α * ↑k))) / Real.log ↑n
+
+/--
+Erdős Problem 1002 [Er64b]:
+
+Does the function $f(\alpha, n) = \frac{1}{\log n} \sum_{k=1}^n \left(\frac{1}{2} - \{\alpha k\}\right)$
+have an asymptotic distribution function? That is, is there a non-decreasing function
+$g : \mathbb{R} \to \mathbb{R}$ with $g(-\infty) = 0$ and $g(\infty) = 1$ such that for every
+$c \in \mathbb{R}$,
+$$\lim_{n \to \infty} \mu(\{\alpha \in (0,1) : f(\alpha,n) \le c\}) = g(c)$$
+where $\mu$ is Lebesgue measure.
+-/
+@[category research open, AMS 11 28]
+theorem erdos_1002 : answer(sorry) ↔
+    ∃ g : ℝ → ℝ, Monotone g ∧
+    Filter.Tendsto g Filter.atBot (nhds 0) ∧
+    Filter.Tendsto g Filter.atTop (nhds 1) ∧
+    ∀ c : ℝ, Filter.Tendsto
+      (fun n : ℕ =>
+        (volume (Set.Ioo (0 : ℝ) 1 ∩ {α : ℝ | erdosF α n ≤ c})).toReal)
+      Filter.atTop (nhds (g c)) := by
+  sorry
+
+end Erdos1002