Erdős·erdos:1041
Erdős Problem 1041
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 statement corpus cites this proof against its own statement.
analysis, polynomials·Source
AI activity
How grades workArgument with major gaps made
Reasoning and sources
Autonomy
AI standalone; human involvement recorded as non-significant
Sources
Argument with major gaps made
Reasoning and sources
Autonomy
AI collaborating with humans
Sources
Does the formal statement say what was claimed?
F2 declared The statement corpus cites this proof against its own statement.
Computed from what the project declares and what the register holds, never from reading the mathematics. How fidelity is graded.
Declared by the projects
1Read 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 mathematics
- 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 discussionGet an email when this problem moves
A new claim, a check, a bounty or a discussion. One link to confirm, one click to stop.
Discussion and bounties for this problem load here.
Formal material
Formal statements · 1
Also known as · 3
- https://www.erdosproblems.com/1041
- https://github.com/google-deepmind/formal-conjectures/blob/main/FormalConjectures/ErdosProblems/1041.lean
- FormalConjectures/ErdosProblems/1041.lean