Status
On this page
Status
Topics
Status
On this page
Status
Topics
Let . Let
Is it true that
Source: erdosproblems.com/476
An accepted solution exists. The statement is true.
Proved. The site's status-defining source is the paper of Dias da
Silva and Hamidoune [dSHa94] (Bull. London Math. Soc. 26 (1994), no. 2,
140--146, refereed), at its Theorem 4.1 (printed p. 144;
result page):
for a finite subset of a field of characteristic and a positive
integer , the sums of the -subsets of number at least
, and the remark after its proof states the case
for , , as the conjecture of
Erdős and Heilbronn; its proof uses linear algebra and the representation
theory of the symmetric group. The general theorem is also stated and proved
in the refereed paper [ANR96], whose Theorem 3.3 (p. 411;
result page)
states it with the label "([4])" and proves it from that paper's own Theorem
3.2 by the polynomial method. The statement itself is also proved in refereed
papers: Theorem 2 of Alon, Nathanson and Ruzsa [ANR95] (Amer. Math. Monthly
102 (1995), 250--255;
result page),
labeled by them "(Dias da Silva--Hamidoune [3])", states
for and derives it in three lines
from their
Theorem 1 (Alon and Ruzsa 1995),
for , proved by the polynomial
method (the Alon--Tarsi lemma with interpolation); and Theorem 1.3 of [ANR96]
(p. 405;
result page),
labeled "([4])", states
for nonempty and derives it from the case of that
paper's Proposition 1.2, and again as the case of its Theorem 3.3. An
external Lean proof following the same method is described under
Formalization. The site's label is PROVED (LEAN); its Lean mark is a catalog
label explained there. The claim pages are
Dias da Silva and Hamidoune
(accepted on the refereed publication and the site's credit) and
Alon, Nathanson and Ruzsa
(the polynomial-method proof; accepted on the refereed publications; the Lean
proof in the lean-proofs repository, which declares itself a formalization of
their argument, is its formalization link, third-party Lean that gives no
formalized evidence).