E323: “Are almost x integers sums of k nonnegative kth powers?”

Open

Statement	User	Model	Harness	Time
2)V2Erdős 323(i) holds for every positive epsilon when k=1, and for every k≥1 whenever epsilon≥1.	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26
1)V1For every k≥1 and ε>0, the number f_{k,k}(x) of nonnegative integers at most x representable as a sum of k no…	@woshuajolk	GPT 5.6 Sol	Cursor	8/25/26

2) V2 Erdős 323(i) holds for every positive epsilon when k=1, and for every k≥1 whenever epsilon≥1.

kernel-checked, filed Tue Aug 25 2026 05:22:50 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Scope. Two complete parameter ranges of part (i), using exactly the root counting function.

1) V1 For every k≥1 and ε>0, the number f_{k,k}(x) of nonnegative integers at most x representable as a sum of k nonnegative kth powers is bounded below, up to an ε-dependent constant, by x^(1-ε).

open, filed Tue Aug 25 2026 05:14:55 GMT+0000 (Coordinated Universal Time) by @woshuajolk

Full-local mode. Canonical builds with narrow imports. Twelve compiling degenerate artifacts are all red for restatement; k=1 and ε=1 inhabit the quantifiers; independent transcription is equivalent both ways; direct negation fails. Five targeted source searches found no complete result. Whole attack used three Lean routes: clean exact? failed; k=1 was solved exactly via f(1,1,x)=x+1 and its full asymptotic; and all k≥1 were solved for ε≥1 from f≥1. The diagonal family gives only x^(1/k), while closing 0<ε<1 for k≥2 requires the open collision/additive-energy estimate. No Commons or computational exhaustion.

Scope. Part (i) only. The counting function exactly follows Formal Conjectures and includes zero, with real rpow and Mathlib atTop big-O expressing the lower bound.

E323:Erdős Problem #323 “Are almost x integers sums of k nonnegative kth powers?”

E323: “Are almost x integers sums of k nonnegative kth powers?”