VibeMathedMath problems solved with AI
Sign in

Erdős Problem #106

Erdős problem #106 · erdosproblems.com/106

If f(n)f(n) is the maximum total side length of nn interior-disjoint squares packed in the unit square, is f(k2+1)=kf(k^2 + 1) = k? An exact rational configuration packs 1717 squares with total side length greater than 44, refuting the identity at k=4k = 4.

Result
Disproved
Status
Resolved
AI contribution
AI-assisted
Method
Computation
Field
Discrete Geometry, Packing
Posed by
Paul Erdős
Year posed
1932
Years open
94y
Solved
2026-07-29
Model
Claude Opus 5
Vendor
Anthropic
Collaborators
—
Verification
Lean-verified
Publication
Announced
Significance
11 / 100
Disclosed cost
—
Wikipedia
No dedicated article

What the AI did

The public Lean source credits Codex as formal author; The packing was discovered by Claude Opus 5 (Anthropic) against search infrastructure built and run by the submitter, and verified independently in exact rational arithmetic via separating-axis certificates.

Verification

A 613-line, placeholder-free Lean proof of the counterexample; the erdosproblems.com page has now the result and is showing the conjecture as disproved.

Sources

Changelog3 changes
  • FrostyOsprey245changed Status from “candidate” to “resolved”, also Verification note
  • FrostyOsprey245changed What the AI did from “The public Lean source credits Codex as formal author; the available record does not estab…” to “The public Lean source credits Codex as formal author; The packing was discovered by Claud…”, also Model, Vendor
  • FrostyOsprey245set Age footnote to “Dated to 1932 by Soifer, who heard it from Erdős directly ("In 1932, the 19-year old Paul …”, also Year posed, More links, Posed by

Discussion