---

The claim. The file ErdosProblems/Erdos541.lean of Boris Alexeev's public repository plby/lean-proofs proves erdos_541 : ∀ p, Fact p.Prime → ∀ (a : Fin p → ZMod p), (∃ r, ∀ (S : Finset (Fin p)), S ≠ ∅ → ∑ i ∈ S, a i = 0 → S.card = r) → (Set.range a).ncard ≤ 2, the formal-conjectures statement of Problem 541: for every prime $p$ and every sequence $a_1,\ldots,a_p$ of residues modulo $p$ in which every nonempty zero-sum index set has one size $r$, at most two distinct residues occur. This is the site's statement for all primes, the residue $0$ admitted; it is weaker than the all-moduli theorem of Gao, Hamidoune and Wang 2009 and stronger than the large-prime theorem of Erdős and Szemerédi 1976, as the site's curator, Thomas Bloom, noted in the thread.

Provenance. The claimant is Boris Alexeev, who published the file in their repository and reported it in a thread comment of 31 December 2025: the proof was produced with the prover Aristotle (from Harmonic) and with ChatGPT after many runs, connected to the formal-conjectures statement and type-checked by Alexeev (a file of about 3,000 lines taking twenty minutes to check); asked by the curator whether the composite case was tried, Alexeev answered that ChatGPT had read $p$ as a prime. The file's header calls it a formalization of a solution to the problem: it cites Erdős and Szemerédi and Gao, Hamidoune and Wang, says that the argument ChatGPT explained is closer to Grynkiewicz's (the accepted claim Grynkiewicz 2009), and records that Aristotle formalized it except for one lemma proved by ChatGPT. The copy for Lean v4.24.0, the posting's toolchain, names no informal author; the later revision lists as informal authors the authors of those three papers and ChatGPT, and as formal authors Aristotle, ChatGPT and Alexeev. The file formalizes the argument ChatGPT produced, not one claimant's manuscript, so it is recorded as an independent proof with its own page, not as a formalization link on another claimant's page. The formal-conjectures file ErdosProblems/541.lean, at the head of its main branch on 2026-09-18, carries a formal_proof attribute naming the v4.24.0 copy on the repository's main branch, not a fixed commit; the links above pin the repository head of 15 September 2026, where the repository's index page for the problem lists copies for five toolchains (v4.24.0 to v4.33.0). The v4.24.0 copy there (189,988 bytes, 3,072 lines) contains no sorry, no axiom declaration and no native_decide; its closing comment records #print axioms as propext, Classical.choice and Quot.sound. The site's (LEAN) suffix refers to this proof; the community database lists the problem as "proved (Lean)", as of its last update on 30 December 2025, with no formal-proof URL.

Acceptance. Formalized. This corpus's verification built the repository's src/latest project at the commit the links above pin (committed 15 September 2026; Lean v4.33.0, Mathlib v4.33.0) and checked the axioms of Erdos541.erdos_541 in its module ErdosProblems.Erdos541, the first link above; they are exactly propext, Classical.choice and Quot.sound. The built file is a later revision of the posted proof, carried by the repository through toolchain upgrades and clean-ups; the v4.24.0 copy, the version of the posting, was not built, and the acceptance rests on the revision, whose theorem statement is the same text. The repository's comparator challenge ComparatorChallenges/ErdosProblems/Erdos541.lean pins that declaration, and its fingerprint was found identical to the challenge's. The statement was audited clause by clause against the problem's Statement under its Formulation ($p$ prime, repeated residues and the residue $0$ allowed): it takes every a : Fin p → ZMod p and every natural number $r$ such that every nonempty zero-sum index set has size $r$, and concludes that the range of a has at most two elements; Set.ncard is exact because the range is finite, the theorem asserts the answer yes outright, and the file's open declarations and local classical instance do not touch the statement. Not reviewed: the site's curator labels the problem PROVED (LEAN), but the curator's commentary credits the proof to Erdős and Szemerédi and to Gao, Hamidoune and Wang, and the curator's thread remark on this file places its scope without examining it; no outside reviewer has published an examination. Not refereed: the proof is published only in the repository and the site's thread.

Depends on. No page of this wiki.