IMO 2025 Problem 1: sunny lines
Follow the latest progress by email.
For a fixed integer n≥3, cover all positive lattice points (a,b) with a+b≤n+1 using n distinct lines. A line is sunny if it is parallel to neither coordinate axis nor x+y=0. Determine every possible number of sunny lines in such a covering.
Why it matters and what counts as progress
Why it matters: It asks how a finite triangular point pattern constrains the directions of an exact-size line covering.
What counts as progress: A complete classification of feasible sunny-line counts, including constructions and an impossibility proof for the excluded counts.
How the problem developed
- 15 Jul 2025 · Contest problem [1]
IMO jury The problem was set on this day of the official IMO 2025 contest.
Google DeepMind and Gemini Deep Think DeepMind reported an officially graded five-of-six result (35/42); its published solution collection includes a proof for this problem.
AI contributions 2
Aristotle formalizes five IMO 2025 solutions
Harmonic reports that Aristotle generated machine-verified solutions for 2025 IMO Problems 1–5 from human-formalized problem statements, with the Lean proofs published.
Gemini Deep Think solves five IMO 2025 problems
An advanced Gemini Deep Think model produced natural-language solutions to five of the six 2025 International Mathematical Olympiad problems, earning 35 of 42 points under the official coordinators’ grading.
Sources
Website timeline
Publication dates and editorial changes.