qedbot

Erdős·erdos:1054

Erdős Problem 1054

conjecture formal record: open source: open F2 declared

No independent check recorded yet. A formal artifact, declaration or published object is attached, but no rebuild of it is recorded here.

Fidelity F2: The correspondence is declared through an alignment table and written divergences.

number theory, divisors·Source

AI activity

How grades work
Claude Opus 4.8, GPT-5.5 Pro, Principia Math

23 Jun 2026

Partial result (Lean)

partial A3 V2 F2
Reasoning and sources

Autonomy

AI standalone; human involvement recorded as non-significant

Fidelity

How fidelity is graded

F2 declared. The correspondence is declared through an alignment table and written divergences.

declares divergences from its source reviewed by its authors only

Declared by the projects

1

As each project's formalization.yaml states it.

Erdos 1054: conditional divisor-prefix classificationhs-chae/erdos1054_hyunsik · joined by names · no independent check

Read formalization.yaml

authors
Hyunsik (hschae)
method
agent — GPT-6 (Codex)
review
self-assessed — self-assessed; local build and three-kernel comparator validation passed (Jason (Codex agent))
axioms
Classical.choice, Quot.sound, propext
sorry
0 unproved goals declared
sources
Erdos Problem 1054 verifier — adapts; The ternary Goldbach conjecture is true — background; Approximate formulas for some functions of prime numbers — background
related
pntpp:35fa8a2d09a9aa334f89b8eb67e35ee3cba8e4e5 — builds-on
divergences
Analytic inputs remain conditional. The two imported admitted prime-counting estimates became explicit theorem parameters, with unchanged mathematical content. Finite large and small ranges use new subset-sum dynamic programs, proved sound, rather than the original native certificate search. Fixed real comparisons use rational exponential bounds. The divisor-prefix conclusion is unchanged.
checked by
nobody independent of its authors yet

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/1054
  • https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1054.lean
  • FormalConjectures/ErdosProblems/1054.lean

Cite this record

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

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