Research notes on every problem, and a library of the papers behind them. Built from the open erdos repository.
Updated
This proves the entire statement of
L20
by machine-checked Lean, at tier 2 for the Lean sources of 2026-09-28 that
the card's standing names; the prose route it formalizes is the
prime tensor extraction route,
and the Lean proof map lists the
modules stage by stage. The formal entry point is
Erdos.Research.Problem774.rootsOfUnity_analyticSidon in
lean/Erdos/RootsOfUnitySidon/RootsOfUnitySidonAnalytic.lean: a cutoff prime
with a uniform half parameter on every finite tail stage
(exists_cutoff_uniform_stage_half_parameter) feeds
analyticSidon_of_uniform_tail_parameter, which absorbs the finitely many
small primes (SmallPrimeAssembly.lean) and passes from odd squarefree
orders to all root orders (OddSquarefreeReduction.lean,
RootsOfUnitySidon.lean, AntipodalSidon.lean). The definitions
rootsOfUnity and AnalyticSidon live in RootsOfUnitySidon.lean.