qedbot

Erdős·erdos:258

Erdős Problem 258

problem formal record: solved source: proved (Lean) 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 a Comparator challenge, an alignment table and written divergences.

irrationality·Source

AI activity

How grades work
GPT-5.4 Pro

14 Apr 2026

Full solution

full A2 V1 F2
Reasoning and sources

Autonomy

AI building on literature supplied to it

Details

literature: 🟡 Tao and Teräväinen (2025)

Aristotle

14 Apr 2026·supporting task

GPT-5.4 Pro (2026)

full A1 V1 F2
Reasoning and sources

Autonomy

Secondary contribution: formalization

Details

proof to formalize: GPT-5.4 Pro (2026)

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 declares 8 unproved goals reviewed by its authors only

Declared by the projects

1

As each project's formalization.yaml states it.

Eight Erdős problem programmes: checked mathematicswcook04/plectis-lean-erdos249-257 · joined by artifact · no independent check

Read formalization.yaml

authors
Will Cook
method
agent — OpenAI Codex and other disclosed agent systems
review
self-assessed
axioms
Classical.choice, Quot.sound, propext
sorry
8 unproved goals declared
results
49 main results named, checked with Comparator, with an alignment table
sources
Erdős Problems 68, 243, 249, 251, 257, 269, 1041, and 1049 — background, authors n/a; Repository problem notes and cited-source registry — adapts, authors n/a
divergences
Using the degree-seven polynomial constructed by the erdosproblems.com contributor ani, Lean proves that every preconnected strict-lemniscate set containing two distinct roots has one-dimensional Hausdorff measure greater than two. This refutes the exact Formal Conjectures path-image-length statement; the separate total-variation bound is also checked. The other seven targets remain open. Independent human review of correspondence with the 1958 wording has not been recorded. Comparator checks only selected exact statements, axioms and kernel acceptance; it does not assess novelty or historical correspondence.
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 · 2

Recorded elsewhere

Compare the registries
  • vibemathed — Erdős Problem #258

    checked·machine-led·their labels: lean-verified, ai-discovered

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

Cite this record

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

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