qedbot

Erdős·erdos:258

Erdős Problem 258

problem formal record: solved source: proved (Lean)no 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

2026-04-14

Full solution

full A2 directed V1 write-up F2 declared
Reasoning and sources

Autonomy

AI building on literature supplied to it

Details

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

Aristotle

2026-04-14·supporting task

GPT-5.4 Pro (2026)

full A1 collaborative V1 write-up F2 declared
Reasoning and sources

Autonomy

Secondary contribution: formalization

Details

proof to formalize: GPT-5.4 Pro (2026)

Does the formal statement say what was claimed?

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

Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.

Declared by the projects

1

Read from each project's formalization.yaml. A declaration is what the authors say about their own work, recorded so that a check can confirm or contradict 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.

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