Erdős problem 541 · problems.science

Let $a_1, \dots, a_p$ be (not necessarily distinct) residues modulo a prime $p$ , such that there exists some $r$ so that if $S \subseteq [p]$ is non-empty and $\sum_{i \in S} a_i \equiv 0 \pmod{p}$ then $|S| = r$ .

Sources

Browse retained paths and inspect the exact material available for this Problem.

3 retained statements2415f78e850a

Open selected source

FormalConjectures/ErdosProblems/

541.lean

Retained formal statement1 of 3

Must there be at most two distinct residues amongst the $a_i$ ?

This was formalized in Lean by Alexeev using Aristotle and ChatGPT.

FormalConjectures/ErdosProblems/541.leanErdos541.erdos_5415 linesExact file

1True ↔2  ∀ (p : ℕ),3    Fact (Nat.Prime p) →4      ∀ (a : Fin p → ZMod p),5        (∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2

SolvedProof has a holelean4external proof

The proof uses `sorry`: part of the argument is written but not proved. Lean accepts the file; it does not accept the theorem.

Sources

Search problems.science