Claim. There is an absolute constant $C>0$ such that for every finite set $A\subset\mathbb Z$ of size $N$,

Littlewood's conjecture and the exact question of Problem 512. It is the theorem of O. C. McGehee, L. Pigno and B. Smith, Hardy's inequality and the $L^1$ norm of exponential sums, Ann. of Math. (2) 113 (1981), no. 3, 613–618, announced in Hardy's inequality and the Littlewood conjecture, Bull. Amer. Math. Soc. (N.S.) 5 (1981), no. 1, 71–72. Neither paper is held by the library, and the statement is recorded at the level the site's problem page gives it; the method's name, a Hardy-type inequality and a dual construction, is taken from the titles and from the Lean file below.

Acceptance. The Annals paper is a refereed journal publication, the refereed evidence; the publisher's record dates the issue to May 1981 and gives no day, and this page is dated to the first day of that month. The site's curator, Thomas Bloom, labels the problem proved and credits the proof of Littlewood's conjecture independently to this paper and to Konyagin, whose claim page records Konyagin's proof; that curator credit is the reviewed evidence.

Formalization. The linked Lean file in the Jayyhk/erdos-lean repository, pinned at the commit in the link, proves

theorem erdos_512 :
    ∃ K : ℝ, 0 < K ∧ ∀ A : Finset ℤ,
      K * Real.log A.card ≤
        ∫ θ in (0:ℝ)..1,
          ‖∑ n ∈ A, Complex.exp (2 * Real.pi * Complex.I * n * θ)‖

(line breaks reflowed, tokens unchanged) with a docstring crediting the result independently to Konyagin and to McGehee, Pigno and Smith, and its proof cites the Annals paper and builds what its comments call the McGehee–Pigno–Smith dual construction, so the file is recorded here as a formalization of this paper's proof. The proof was produced by the AI system Aristotle (Harmonic): the repository's README states that each proof file imports only Mathlib, lists this problem as complete and points to the sources field of its data/problems.yaml for original sources, and that entry for problem 512 lists an Aristotle request together with the one comment of the site's discussion thread, JoshuaB's post of 22 June 2026, which reports that Aristotle used the paper of McGehee, Pigno and Smith to formalize the problem. The file prints the axioms of erdos_512 and records the output as a comment, [propext, Classical.choice, Quot.sound]; the file contains no sorry, axiom or native_decide token. The statement file in google-deepmind/formal-conjectures names this file as the formal proof and is itself a statement with sorry, so it is not a formalization link. This corpus has not built or kernel-checked the proof, so no formalized evidence is listed. The Lean statement takes the logarithm of the set's size with Lean's convention that the logarithm of $0$ and of $1$ is $0$, which makes the cases $N\le1$ trivial and matches the question's asymptotic form.

Depends on. Nothing beyond the cited paper.