Skip to content

Erdős problem 541

Start work

Let a1,…,apa_1, \dots, a_p be (not necessarily distinct) residues modulo a prime pp, such that there exists some rr so that if S⊆[p]S \subseteq [p] is non-empty and ∑i∈Sai≡0(modp)\sum_{i \in S} a_i \equiv 0 \pmod{p} then ∣S∣=r|S| = r.

No current result

No reviewed Result is current in Vela Mathematics Program. Retained source material is shown below.

Retained declaration

FormalConjectures/ErdosProblems/541.lean

Formal Conjectures

FormalConjectures/ErdosProblems/541.leanErdos541.erdos_5415 linesExact file
True ↔  ∀ (p : ℕ),    Fact (Nat.Prime p) →      ∀ (a : Fin p → ZMod p),        (∃ 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.

Proof manifests naming this Problem

  • Jayyhk Erdős Leanjayyhk:erdos:541
  • PLBY Lean proofsErdosProblems.Erdos541

Reported activity

Reported by these sources. Not reviewed here.

Continue

Start a contributionBrowse the source filesOpen the collection entry