Erdős Problem #106
Erdős problem #106 · erdosproblems.com/106
If is the maximum total side length of interior-disjoint squares packed in the unit square, is ? An exact rational configuration packs squares with total side length greater than , refuting the identity at .
- Result
- Disproved
- Status
- Candidate (review pending)
- 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
- OpenAI Codex
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 10 / 100
- Disclosed cost
- —
- Wikipedia
- No dedicated article
What the AI did
The public Lean source credits Codex as formal author; the available record does not establish that Codex discovered the packing, so this entry tracks the AI formalization rather than assigning mathematical priority.
Verification
A 613-line, placeholder-free Lean proof of the counterexample; the erdosproblems.com page had not yet incorporated the result at audit time.