diff --git a/FormalConjectures/ErdosProblems/7.lean b/FormalConjectures/ErdosProblems/7.lean index a946ad49d8..03622d6cdb 100644 --- a/FormalConjectures/ErdosProblems/7.lean +++ b/FormalConjectures/ErdosProblems/7.lean @@ -15,56 +15,55 @@ limitations under the License. -/ import FormalConjectures.Util.ProblemImports +import FormalConjecturesForMathlib.NumberTheory.CoveringSystem /-! # Erdős Problem 7 *Reference:* [erdosproblems.com/7](https://www.erdosproblems.com/7) -Erdős asked whether there exists a distinct covering system all of whose moduli are odd. +Erdős and Selfridge asked whether there exists a distinct covering system all of whose +moduli are odd. -[HN19] Hough, B. and Nielsen, N., _Solution of the minimum modulus problem for covering +[HoNi19] Hough, B. and Nielsen, N., _Solution of the minimum modulus problem for covering systems_. Ann. of Math. (2019). -[Ba22] Balister, P., Bollobás, B., Morris, R., Sahasrabudhe, J. and Tiba, M., _Covering +[BBMST22] Balister, P., Bollobás, B., Morris, R., Sahasrabudhe, J. and Tiba, M., _Covering systems, matchings, and odd covering systems_. (2022). --/ - -namespace Erdos7 - -/-- -A finite system of congruences $\{(a_i, m_i)\}$ is a **covering system** if every -modulus is positive and every integer satisfies at least one congruence $n \equiv a_i \pmod{m_i}$. --/ -def IsCoveringSystem (S : Finset (ℤ × ℕ)) : Prop := - S.Nonempty ∧ - (∀ p ∈ S, 0 < p.2) ∧ - (∀ n : ℤ, ∃ p ∈ S, (p.2 : ℤ) ∣ (n - p.1)) -/-- -A covering system has **distinct moduli** if no two congruences share the same modulus. +Selfridge showed that this problem would have a positive answer if a covering system with +pairwise non-divisible moduli existed (see Problem 586). -/ -def HasDistinctModuli (S : Finset (ℤ × ℕ)) : Prop := - ∀ p ∈ S, ∀ q ∈ S, p.2 = q.2 → p = q /-- Is there a distinct covering system all of whose moduli are odd? -A **distinct covering system** is a finite collection of congruences -$\{n \equiv a_i \pmod{m_i}\}$ where all moduli $m_i$ are pairwise distinct, +A **distinct covering system** (`StrictCoveringSystem`) is a finite collection of +congruences $\{n \equiv a_i \pmod{m_i}\}$ where all moduli $m_i$ are pairwise distinct, covering every integer. The question asks whether such a system can exist with all -moduli odd. +moduli odd and at least 2. Known results: -- [HN19] proved that in any distinct covering system, at least one modulus must be - divisible by 2 or 3. A simpler proof was given by [Ba22], who also showed that the +- [HoNi19] proved that in any distinct covering system, at least one modulus must be + divisible by 2 or 3. A simpler proof was given by [BBMST22], who also showed that the lcm of any odd covering system's moduli must be divisible by 9 or 15. -- [Ba22] proved no odd distinct covering system exists if the moduli are additionally +- [BBMST22] proved no odd distinct covering system exists if the moduli are additionally required to be squarefree. The general odd case remains open. -/ @[category research open, AMS 11] theorem erdos_7 : answer(sorry) ↔ - ∃ S : Finset (ℤ × ℕ), IsCoveringSystem S ∧ HasDistinctModuli S ∧ ∀ p ∈ S, Odd p.2 := by + ∃ c : StrictCoveringSystem ℤ, + ∀ i, ∃ (m : ℕ), Odd m ∧ 1 < m ∧ c.moduli i = Ideal.span {(m : ℤ)} := by sorry -end Erdos7 +/-- +There is no distinct covering system with all moduli odd and squarefree. + +This is a stronger variant of `erdos_7` where the moduli are additionally required to be +squarefree. It was disproved by [BBMST22] Balister, Bollobás, Morris, Sahasrabudhe, and Tiba. +-/ +@[category research solved, AMS 11] +theorem erdos_7_squarefree : ¬ ∃ c : StrictCoveringSystem ℤ, + ∀ i, ∃ (m : ℕ), Odd m ∧ Squarefree m ∧ 1 < m ∧ + c.moduli i = Ideal.span {(m : ℤ)} := by + sorry diff --git a/ai-review/7.md b/ai-review/7.md new file mode 100644 index 0000000000..3a3463f234 --- /dev/null +++ b/ai-review/7.md @@ -0,0 +1,151 @@ +# Review: Erdos Problem 7 + +**File:** `FormalConjectures/ErdosProblems/7.lean` +**Reviewer:** Claude (automated) +**Date:** 2026-03-09 + +--- + +## 1. Code Reuse + +**Rating: Significant reuse opportunity missed.** + +The file defines `IsCoveringSystem` and `HasDistinctModuli` locally in the `Erdos7` namespace. However, `FormalConjecturesForMathlib/NumberTheory/CoveringSystem.lean` already provides: + +- `CoveringSystem R` — a structure over a general `CommSemiring R` with a finite index type, residues, ideals as moduli, a union-covers proof, and non-triviality. +- `StrictCoveringSystem R` — extends `CoveringSystem R` with `injective_moduli`, which encodes the "distinct moduli" constraint. + +A `StrictCoveringSystem ℤ` is mathematically equivalent to `IsCoveringSystem S ∧ HasDistinctModuli S` as defined in Problem 7. Problem 273 already demonstrates using `StrictCoveringSystem` directly in a theorem statement. + +Furthermore, Problems 2 and 8 define literally identical copies of `IsCoveringSystem` in their own namespaces. This is a codebase-wide consistency issue — at minimum, these definitions should be consolidated. + +**Recommendation:** Restate `erdos_7` using `StrictCoveringSystem ℤ` with an additional constraint that each `moduli i` is a principal ideal generated by an odd number. This would align with the shared library and Problem 273's approach. If the `Finset`-based formulation is preferred for concreteness, it should be factored into a shared file and reused across Problems 2, 7, 8, 27, etc. + +--- + +## 2. Citations + +**Rating: Mostly accurate, minor gaps.** + +The docstring cites: +- **[HN19]** Hough, B. and Nielsen, N. — cited as "Solution of the minimum modulus problem for covering systems", Ann. of Math. (2019). +- **[Ba22]** Balister, P., Bollobás, B., Morris, R., Sahasrabudhe, J. and Tiba, M. — cited as "Covering systems, matchings, and odd covering systems" (2022). + +Per erdosproblems.com/7: +- The [HN19] citation matches (listed as `HoNi19` on the website). +- The [Ba22] citation matches (listed as `BBMST22` on the website, with all five authors). The docstring correctly lists all five authors. + +**Missing from the docstring:** +- The website notes that Selfridge showed the problem would have a positive answer if a covering system with pairwise non-divisible moduli existed, connecting this to Problem #586. This context is not mentioned. +- The website notes a $25 prize offered by Erdos and a separate $2000 prize by Selfridge for an explicit example. Prize information is not expected in formalizations but adds useful context. +- The problem is attributed to both Erdos and Selfridge (sometimes with Schinzel). The docstring attributes it only to Erdos. + +**Recommendation:** Add a brief note mentioning the Selfridge connection and Problem 586. Consider using the website's citation keys (HoNi19, BBMST22) for consistency with the source. + +--- + +## 3. Variants + +**Rating: Incomplete — one important variant missing.** + +The docstring mentions two results: +1. [HN19]'s result that at least one modulus must be divisible by 2 or 3. +2. [Ba22]'s result that no odd distinct covering system exists if moduli are squarefree. + +The website identifies a **stronger variant**: "Is there a distinct covering system with all moduli odd **and squarefree**?" This was disproved by BBMST22. + +While the docstring mentions the squarefree result in passing as a "known result," it is not formalized as a separate theorem. Given that this is a resolved variant (answered negatively), it would be a natural candidate for a companion theorem: + +```lean +theorem erdos_7_squarefree : ¬ ∃ S : Finset (ℤ × ℕ), + IsCoveringSystem S ∧ HasDistinctModuli S ∧ + (∀ p ∈ S, Odd p.2) ∧ (∀ p ∈ S, Squarefree p.2) := by + sorry +``` + +Additionally, the Selfridge conditional result (connection to Problem 586 — pairwise non-divisible moduli) is another variant worth noting. + +--- + +## 4. Readability + +**Rating: Good, with minor suggestions.** + +**Strengths:** +- Clean, minimal definitions with clear docstrings. +- The `IsCoveringSystem` definition is straightforward and easy to parse. +- Good use of LaTeX in docstrings. + +**Suggestions:** +- The `HasDistinctModuli` name is slightly ambiguous — it could also mean "the set of moduli is non-trivial" in casual reading. A name like `HasPairwiseDistinctModuli` or `HasInjectiveModuli` would be more precise, though this is minor. +- The covering condition `(p.2 : ℤ) ∣ (n - p.1)` is equivalent to `n ≡ p.1 [ZMOD p.2]` but less immediately recognizable. Problems 204 and 277 use `Int.ModEq` notation (`z ≡ s.1 [ZMOD s.2]`), which is arguably more readable. However, the divisibility formulation is more direct for Lean proofs, so this is a stylistic choice. +- The theorem `erdos_7` uses `answer(sorry)`, which is the standard pattern for open problems with unknown truth values. This is correct and readable. + +--- + +## 5. Formalizability + +**Rating: High — the statement is precise and unambiguous.** + +The mathematical statement "Is there a distinct covering system all of whose moduli are odd?" is fully precise: +- "Covering system" has a standard definition in combinatorial number theory. +- "Distinct" (meaning distinct moduli) is standard. +- "Odd moduli" is unambiguous. + +There is **no meaningful ambiguity** in this problem statement. The only design choice is representational: how to encode covering systems in Lean (Finset-based, function-based, or structure-based). The chosen `Finset (ℤ × ℕ)` representation is concrete and natural. + +One minor subtlety: the formalization allows a modulus of 1 (since `0 < p.2` permits `p.2 = 1`, and `1` is odd). A single congruence with modulus 1 trivially covers all integers, but the `HasDistinctModuli` constraint means at most one modulus-1 congruence can appear. Since modulus 1 is odd, the existence claim would be trivially true if the distinct-moduli constraint allowed it. However, `HasDistinctModuli` as defined only requires that elements with the same modulus are equal — it does not forbid modulus 1. So the set `{(0, 1)}` satisfies all three conditions (`IsCoveringSystem`, `HasDistinctModuli`, and all moduli odd). **This means `erdos_7` as formalized is trivially true**, which is almost certainly not the intended formalization. + +The standard definition of a covering system in this context requires all moduli to be **greater than 1** (or equivalently ≥ 2). Problem 586 uses `2 ≤ n i` for exactly this reason. The website's description and the mathematical literature uniformly assume moduli ≥ 2 in covering system problems. + +**This is a critical correctness issue** — see Section 6 below. + +--- + +## 6. Correctness + +**Rating: Incorrect — admits trivial solution.** + +### Critical Issue: Modulus 1 is permitted + +As analyzed in Section 5, the set `S = {(0, 1)}` satisfies: +- `IsCoveringSystem S`: S is nonempty, `0 < 1`, and every integer `n` satisfies `1 ∣ (n - 0)`. +- `HasDistinctModuli S`: vacuously, the single element has a unique modulus. +- `∀ p ∈ S, Odd p.2`: `Odd 1` is true. + +Therefore `erdos_7` is trivially provable with `answer(sorry) = True`, which contradicts the problem's open status. + +**Fix:** Add the constraint `1 < p.2` (or equivalently `2 ≤ p.2`) to either `IsCoveringSystem` or the theorem statement: + +```lean +theorem erdos_7 : answer(sorry) ↔ + ∃ S : Finset (ℤ × ℕ), IsCoveringSystem S ∧ HasDistinctModuli S ∧ + ∀ p ∈ S, Odd p.2 ∧ 1 < p.2 := by + sorry +``` + +Alternatively, modify `IsCoveringSystem` to require `1 < p.2` instead of `0 < p.2`. + +### Secondary Issue: `HasDistinctModuli` is stronger than necessary + +The definition `∀ p ∈ S, ∀ q ∈ S, p.2 = q.2 → p = q` says that elements of `S` are uniquely determined by their modulus. This means not only are the moduli distinct, but **there is at most one residue per modulus**. This is indeed the standard meaning of "distinct covering system" (each modulus appears exactly once), so this is correct. However, it's worth noting that this rules out systems like `{(0, 3), (1, 3)}` which have the same modulus but different residues — which is the intended behavior. + +### Note on `IsCoveringSystem` requiring `Nonempty` + +The `S.Nonempty` condition is redundant given the covering property (if `S` were empty, no integer would be covered). This is not a correctness issue but a minor redundancy. + +--- + +## Summary + +| Criterion | Rating | Key Issue | +|-----------|--------|-----------| +| Code Reuse | Needs improvement | Should use `StrictCoveringSystem` or shared definitions | +| Citations | Good | Minor gaps (Selfridge attribution, Problem 586 connection) | +| Variants | Incomplete | Squarefree variant should be formalized separately | +| Readability | Good | Minor naming suggestions | +| Formalizability | High | Statement is mathematically precise | +| Correctness | **Incorrect** | **Modulus 1 makes the problem trivially true** | + +### Priority Fix +The modulus-1 issue must be resolved. The covering system definition should require `1 < p.2` (moduli ≥ 2) to match the standard mathematical definition and the problem's open status. diff --git a/ai-review/REVIEW_MATH.md b/ai-review/REVIEW_MATH.md new file mode 100644 index 0000000000..d34c053c43 --- /dev/null +++ b/ai-review/REVIEW_MATH.md @@ -0,0 +1,12 @@ +# Review Math + +Assume the role of a PhD-level mathematician. + +The goal is to review a particular Erdos Problem formalization (problem number NUM) to answer the following questions. Produce a review document called ai-review/NUM.md. + +1. Code reuse - Can any code from the existing codebase be repurposed? Look in FormalConjecturesForMathlib to determine if an existing implementation would work just as well. +2. Citations - Fetch data from https://www.erdosproblems.com/NUM to ensure any citations included in docstrings are documented as they exist on the website as opposed to shorthand references. +3. Variants - Are all variants of the problem captured by the formalization? +4. Readability - Could the code be made more readable? +5. Formalizability - Is the problem as stated precise enough to be obviously formalizable? Provide an assessment of the ambiguity of the statement. +6. Correctness - Is the formalization as-implemented correct and complete from a mathematical perspective? Would an experienced mathematician identify any obvious flaws? Is any incompleteness or incorrectness attributable to ambiguity in the statement itself?