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

[lyfar]

This PR formalizes the finite inequality stated as Theorem 2 in Richard K. Guy’s 1982 account and credited there to Leo Moser:

4 ^ |A| - 1 ≤ 3 * ∑ a ∈ A, a ^ 2

for a finite set of natural numbers with distinct subset sums. It also derives direct and square-root lower bounds for the largest element.

This is a known finite result. I am not claiming the stronger historical Erdős–Moser asymptotic bound, and Erdős Problem #1 remains open.

Source: Richard K. Guy, “Sets of Integers Whose Subsets Have Distinct Sums,” Theorem 2, Annals of Discrete Mathematics 12 (1982), 141–154. DOI: https://doi.org/10.1016/S0304-0208(08)73500-X

Local checks:

• lake exe mk_all --check
• lake build LeanPool.ErdosMoser
• lake exe runLinter LeanPool.ErdosMoser
• lake exe lint-style LeanPool.ErdosMoser
• forbidden-token and git diff --check scans
• main theorem axiom footprint: propext, Classical.choice, Quot.sound

AI disclosure: AI agents produced and refactored the Lean proof under my direction. I reviewed the theorem scope, source attribution, and verification results.

[greptile-apps]

Greptile Summary

This PR formalizes Leo Moser's finite distinct-subset-sums inequality (4^|A| - 1 ≤ 3 * ∑ a ∈ A, a²) in Lean 4, credited to Guy's 1982 account, along with derived bounds on the largest element. The formalization is split cleanly into four files covering basic definitions, a discrete variance bound, subset-sum moment identities, and the final bounds.

• New LeanPool/ErdosMoser/ module adds HasDistinctSubsetSums, the variance lower bound for initial intervals (varianceLowerBoundFinsetNat), first/second moment identities for subset sums, the main Moser inequality (leoMoserVarianceBound), and two corollaries bounding max(A).
• LeanPool/projects.yml registers the project with provenance: AI, full source attribution to Guy's DOI, and an external github_repo reference in the source block.
• The axiom footprint reported by the author (propext, Classical.choice, Quot.sound) is consistent with expected pure-Mathlib Lean 4 proofs.

Confidence Score: 5/5

This PR adds a self-contained, sorry-free Lean 4 formalization with no infrastructure changes; it is safe to merge.

All new files are purely additive content under LeanPool/ErdosMoser/. The proof strategy is mathematically correct — the discrete variance lower bound, subset-sum moment identities, and the final Moser inequality chain correctly. The author-reported axiom footprint is consistent with standard Mathlib usage. All four-line file headers are present, no sorry/admit/#eval appear, proof bodies are well within the 200-line limit, and the project card satisfies all required fields with a valid DOI source.

Files Needing Attention: No files require special attention.

Important Files Changed

Filename	Overview
LeanPool/ErdosMoser.lean	Top-level entry module with module docstring and single import; correctly structured.
LeanPool/ErdosMoser/Basic.lean	Defines HasDistinctSubsetSums and proves sumSquaresLeCardMulMaxSquare; straightforward and correct.
LeanPool/ErdosMoser/DiscreteVariance.lean	Proves the discrete variance lower bound for finite sets of naturals via orderEmbOfFin and pairwise-difference identity; mathematically correct, no Lean core imports.
LeanPool/ErdosMoser/SubsetSums.lean	Establishes first/second moment identities for subset sums and combines them with the variance bound to prove the main Moser inequality; logic is sound.
LeanPool/ErdosMoser/Bounds.lean	Derives erdosMoserMaxBound and erdosMoserMaxSqrt from the main inequality; correctly uses Real.sqrt_le_left for the square-root form.
LeanPool/projects.yml	Project card is well-formed with required fields, valid DOI source, provenance: AI, and github_repo now correctly pointing to an external formalization repository.
LeanPool.lean	Adds the five new ErdosMoser imports in alphabetical position; no issues.

Flowchart

%%{init: {'theme': 'neutral'}}%%
flowchart TD
    A["HasDistinctSubsetSums\n(Basic.lean)"]
    B["sumSquaresLeCardMulMaxSquare\n(Basic.lean)"]
    C["varianceLowerBoundFinsetNat\n(DiscreteVariance.lean)\nm²(m²-1)/12 ≤ m·Σt² - (Σt)²"]
    D["sumSubsetSums / secondMomentSubsetSums\n(SubsetSums.lean)\n1st & 2nd moment identities"]
    E["leoMoserVarianceBound\n(SubsetSums.lean)\n4^|A| - 1 ≤ 3·Σa²"]
    F["erdosMoserMaxBound\n(Bounds.lean)\n4^|A| - 1 ≤ 3|A|·max(A)²"]
    G["erdosMoserMaxSqrt\n(Bounds.lean)\n√((4^|A|-1)/(3|A|)) ≤ max(A)"]

    A --> E
    C --> E
    D --> E
    E --> F
    B --> F
    F --> G

Loading

_{Reviews (3): Last reviewed commit: "Link Erdős-Moser companion repository" | Re-trigger Greptile}

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 26.43 s (= 0.44 min) — user 13.64 s, sys 2.51 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 45 maxHeartbeats units across 5 files (649 added LOC).

Sum of lean --profile: 10897.7 ms (= 10.90 s). Import-excluded time: 7855.7 ms (= 7.86 s).

Count-heartbeats wall-clock total: 13.62 s. Repeated import cost inside lean --profile: 3042.0 ms (= 3.04 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/ErdosMoser/DiscreteVariance.lean	294	15	2.78	3.01	2.44	0.57	5	0
LeanPool/ErdosMoser/SubsetSums.lean	205	15	5.39	5.19	4.62	0.56	5	0
LeanPool/ErdosMoser/Basic.lean	56	9	1.76	0.80	0.24	0.56	3	0
LeanPool/ErdosMoser/Bounds.lean	66	6	1.87	1.06	0.39	0.67	2	0
LeanPool/ErdosMoser.lean	28	0	1.82	0.83	0.16	0.67	0	0
Total	649	45	13.62	10.90	7.86	3.04	15	0

Aggregate phase totals

Phase	Time
interpretation	4461.0 ms (= 4.46 s)
import	3042.0 ms (= 3.04 s)
typeclass inference	1355.5 ms (= 1.36 s)
tactic execution	530.0 ms (= 0.53 s)
simp	294.1 ms (= 0.29 s)
norm_num	226.2 ms (= 0.23 s)
ring	220.0 ms (= 0.22 s)
type checking	218.0 ms (= 0.22 s)
initialization	157.4 ms (= 0.16 s)
elaboration	97.8 ms (= 0.10 s)
tacticAnalysis	87.7 ms (= 0.09 s)
share common exprs	57.1 ms (= 0.06 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.ErdosMoser.SubsetSums	5.00 s
LeanPool.ErdosMoser.Basic	2.90 s
LeanPool.ErdosMoser.DiscreteVariance	2.50 s
LeanPool.ErdosMoser.Bounds	1.10 s
LeanPool.ErdosMoser	0.87 s

Per-file `lean --profile` output

LeanPool/ErdosMoser.lean

import took 670ms
cumulative profiling times:
	elaboration 0.155ms
	import 670ms
	initialization 37.6ms
	interpretation 121ms
	linting 0.39ms
	module linting 0.0011ms
	overlappingInstancesLinter 0.679ms
	parsing 0.0415ms
	tacticAnalysis 2.27ms
real 1.64
user 0.79
sys 0.48

LeanPool/ErdosMoser/Basic.lean

import took 563ms
cumulative profiling times:
	attribute application 0.0324ms
	congr simp thm 0.519ms
	elaboration 9.22ms
	fix level params 0.0458ms
	import 563ms
	initialization 34.7ms
	instantiate metavars 0.101ms
	interpretation 124ms
	let-to-have transformation 0.0301ms
	linting 2.11ms
	module linting 0.00152ms
	overlappingInstancesLinter 1.13ms
	parsing 2.38ms
	process pre-definitions 0.942ms
	share common exprs 0.272ms
	simp 12.3ms
	tactic execution 15.5ms
	tacticAnalysis 7.4ms
	type checking 2.46ms
	typeclass inference 26.8ms
real 1.15
user 0.80
sys 0.39

LeanPool/ErdosMoser/Bounds.lean

import took 669ms
cumulative profiling times:
	attribute application 0.0216ms
	congr simp thm 0.588ms
	elaboration 9.75ms
	fix level params 0.225ms
	import 669ms
	initialization 28.2ms
	instantiate metavars 0.326ms
	interpretation 186ms
	let-to-have transformation 0.0368ms
	linting 4.36ms
	module linting 0.00142ms
	norm_num 3.89ms
	overlappingInstancesLinter 1.33ms
	parsing 2.33ms
	process pre-definitions 2.27ms
	ring 16ms
	share common exprs 2.74ms
	simp 0.43ms
	tactic execution 33.5ms
	tacticAnalysis 9.62ms
	type checking 15.2ms
	typeclass inference 75.7ms
real 1.33
user 1.04
sys 0.41

LeanPool/ErdosMoser/DiscreteVariance.lean

import took 575ms
cumulative profiling times:
	attribute application 0.0645ms
	congr simp thm 3.1ms
	elaboration 40.8ms
	fix level params 2.02ms
	import 575ms
	initialization 28.7ms
	instantiate metavars 8.23ms
	interpretation 670ms
	let-to-have transformation 0.0937ms
	linting 18.1ms
	module linting 0.00141ms
	norm_num 135ms
	overlappingInstancesLinter 3.24ms
	parsing 17.4ms
	process pre-definitions 16.5ms
	ring 95ms
	share common exprs 27.5ms
	simp 214ms
	tactic execution 307ms
	tacticAnalysis 38.2ms
	type checking 130ms
	typeclass inference 682ms
real 2.45
user 2.96
sys 0.41

LeanPool/ErdosMoser/SubsetSums.lean

import took 565ms
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.14s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 1.17s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 630ms
cumulative profiling times:
	attribute application 0.0537ms
	congr simp thm 1.29ms
	elaboration 37.9ms
	fix level params 1.24ms
	import 565ms
	initialization 28.2ms
	instantiate metavars 4.85ms
	interpretation 3.36s
	let-to-have transformation 0.0928ms
	linting 27.8ms
	module linting 0.00153ms
	norm_num 87.3ms
	overlappingInstancesLinter 3.35ms
	parsing 9.63ms
	process pre-definitions 13.9ms
	ring 109ms
	share common exprs 26.6ms
	simp 67.4ms
	tactic execution 174ms
	tacticAnalysis 30.2ms
	type checking 70.3ms
	typeclass inference 571ms
real 5.03
user 5.16
sys 0.39

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[github-actions]

🤖 LLM review (gpt-5.6-sol, 5 rubrics)

Reviewed head: 437dbd08e4500bc912cb0606d208e385fadb77ae

Verdict: ✅ approve — computed from the rubric verdicts below, not chosen by a model.

Rubric	Verdict	Bottom line
Faithfulness	✅ pass	Each listed declaration matches its informal statement, with all hypotheses disclosed.
Novelty	✅ pass	The Mathlib searches and pool inventory contain no declaration proving any of the three headline bounds.
Significance	✅ pass	The named finite distinct-subset-sums inequality, supported by a reusable variance and subset-moment development, is a good-fit graduate-level additive-combinatorics project.
Sources	✅ pass	The citation metadata is internally consistent, but the diff does not reproduce Guy’s Theorem 2, so the claimed theorem number and attribution are unverifiable here.
Code quality (advisory)	✅ pass	The proof is competently decomposed into reusable combinatorial, variance, and bound lemmas; the long algebraic blocks remain structured and create no material maintenance debt.

Aspect	Value
Proves the claim	✅ proves_it
Assumed, not proved	The main inequality assumes HasDistinctSubsetSums A; the maximum bounds additionally assume A.Nonempty, and both conditions are stated in the card.
Matches cited source	🟡 unverifiable
Fit	✅ good_fit
Level	graduate
Branch	additive combinatorics
Mode	theory_building
Code quality	3 / 5

Statement check: The Lean proves the real-valued finite sum-of-squares inequality and, for nonempty A, the stated direct and square-root bounds on A.max'.

The contribution derives (4 : ℝ) ^ A.card - 1 ≤ 3 * ∑ a ∈ A, (a : ℝ) ^ 2 from a sharp discrete-variance bound and exact subset-sum moment identities, then obtains largest-element lower bounds.

---

Tokens: 74,742 in / 6,512 out across 5 rubric calls · Tier: flex · Effort: xhigh · Cost: $0.2845
Each rubric is an independent review against .github/review-rubrics/ on top of .github/REVIEW_RULES.md. Disagree? Reply on the PR; rules can be updated in a PR of their own.

[Vilin97]

/review — re-run to live-test the gpt-5.6-sol @ xhigh upgrade (752d7bf); comparing cost against the gpt-5.5 baseline on the same head.

[Vilin97]

/review — first run of the audited rules (#293) now that they are on main.

[Vilin97]

/review — confirming the prior-art rendering fix (#303).

[Vilin97]

/review — first run with the Mathlib prior-art search (#306).

[Vilin97]

/review — first run of the five-rubric review (#313).