Skip to content

Formalize Leo Moser's finite distinct-subset-sums inequality - #285

Merged
Vilin97 merged 3 commits into
LeanPool:mainfrom
lyfar:lyfar/erdos-moser-max-bound
Jul 29, 2026
Merged

Vilin97 merged 3 commits into
LeanPool:mainfrom
lyfar:lyfar/erdos-moser-max-bound

Link Erdős-Moser companion repository

437dbd0
Select commit
Loading
Failed to load commit list.
Sign in for the full log view