Erdős Problem #183 — Multicolor Triangle Ramsey
Erdős problem #183 · erdosproblems.com/183
Let be the least such that every -colouring of the edges of contains a monochromatic triangle. Determine (a \$250 Erdős prize problem). A superexponential lower bound resolves the problem: the limit is infinite.
- Result
- Proved
- Status
- Candidate (review pending)
- AI contribution
- AI-discovered
- Method
- Construction
- Field
- Ramsey theory
- Posed by
- Paul Erdős
- Year posed
- 1961
- Years open
- 65y
- Solved
- 2026-08-01
- Model
- Astra (internal preview)
- Vendor
- OpenAI
- Collaborators
- —
- Verification
- Lean-verified
- Publication
- Announced
- Significance
- 20 / 100
- Disclosed cost
- $182
- Wikipedia
- No dedicated article
What the AI did
Generated by an internal version of OpenAI's Astra: per the announcement, the mathematical arguments were produced by the system (roughly 2,000 dollars of compute at Sol API rates across all ten results), humans prepared the manuscripts with the same model, and the model then formalized the argument in Lean. A narrated reasoning walkthrough is published for each result.
Verification
Kernel-checked Lean 4 certificate in OpenAI's public ten-proofs repository (Lean 4.32, mathlib, `lake build All`), with an independent Comparator checking route. Statement fidelity and community review of the day-old company announcement remain pending, hence candidate status.
Sources
OpenAI: Ten advances in mathematics and theoretical computer science