qedbot

Erdős·erdos:67

Erdős Problem 67

problem formal record: solved source: proved$500 F2 declared

Machine-checked by Palomar.

Fidelity F2: The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

discrepancy·Source

AI activity

How grades work

No AI contribution recorded against this statement.

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through a Comparator challenge, an alignment table and written divergences.

declares divergences from its source reviewed by its authors only source authors not contacted

Checks

1
  • verified·Palomar

    Registered by Palomar at 13853222: Comparator confirmed 1 theorems prove the recorded statement within Palomar's axiom policy, replayed through Lean's kernel and the independent nanoda kernel

    project registered at a pinned commit·2026-09-29·commit 13853222d90d

    PALOMAR-2026-09-29-000002

Declared by the projects

1

As each project's formalization.yaml states it.

A Lean formalization of the Erdős discrepancy theoremProofFleet/prooffleet · joined by anchor · Palomar

Read formalization.yaml

authors
Sean Huver
method
agent — Claude Fable 5, Claude Fable 5.1, Claude Opus 5, gpt-5.6-sol
review
self-assessed
sorry
0 unproved goals declared
sources
The Erdős discrepancy problem — formalizes, authors not-contacted; The logarithmically averaged Chowla and Elliott conjectures for two-point correlations — adapts, authors not-contacted; An averaged form of Chowla's conjecture — adapts, authors not-contacted; Multiplicative functions in short intervals — adapts, authors not-contacted
related
google-deepmind/formal-conjectures/blob/2424bb480c590237ffbb2cc831ae4cb8977e045a/FormalConjectures/ErdosProblems/67.lean — other
divergences
Scope: only ±1 sequences valued in ℤ; Tao's Theorem 1.1 is not formalized. Encoding: the stochastic multiplicative functions of Theorem 1.8 take values in ℂ with almost-sure unimodularity rather than in the unit circle; complete multiplicativity is guarded at 0; the limit in the Fourier reduction is taken through an ultrafilter and Prokhorov's theorem. Intermediate statements that differ from the sources, each recorded as weaker than or different from its source in the repository: Proposition 1.11 with a per-sample existential rather than a measurable selection and its constant fixed before ε; Tao's Theorem 1.3 (companion paper) for completely multiplicative functions, conjugate pairs and natural shifts only; in Section 4, a weaker conclusion than the Vinogradov–Korobov input Tao uses, proved instead from an elementary van der Corput bound for zeta and a character-removing argument (the interface keeps the name VinogradovKorobovAssumption); a zero-free region of Chudakov strength, reached through a weak form of Vinogradov's mean value theorem, in place of the Vinogradov–Korobov region used by Matomäki and Radziwiłł, with Lemma 11's exponent 2/3 + ε replaced by a fixed exponent and
checked by
Palomar

Follow and discuss

All discussion

Discussion and bounties for this problem load here.

Something wrong or missing here? Request a correction or add a claim, with its sources.

Formal material

Formal statements · 1
Cited proofs · 0

No proof artifact cited by the formal record.

Also known as · 3
  • https://www.erdosproblems.com/67
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/67.lean
  • FormalConjectures/ErdosProblems/67.lean

Cite this record

qed.bot, “Erdős Problem 67”, https://qed.bot/s/erdos-67, as of 30 Sep 2026.

This record as plain text, with each claim, its grades and its sources.