Complete formalization and solutions for all IMO (1959–2026) and USAMO problems by Imbernoulli · Pull Request #234 · dwrensha/compfiles

Imbernoulli · 2026-07-27T12:05:57Z

Complete formalization and solutions for all IMO (1959–2026) and USAMO problems

This PR adds 443 fully-proved problem files, bringing compfiles' coverage of IMO and USAMO to 100%:

IMO 1959–2026: all 404 problems formalized and solved (404/404/404 on the dashboard)
USAMO 1972–2026: all 306 problems formalized and solved (306/306/306)

Every file:

has a complete, sorry-free proof of the problem statement;
depends only on the standard axioms [propext, Classical.choice, Quot.sound] (verified per file with #print axioms);
is in the module-system format introduced in migrate to Lean's module system #235;
carries attribution in the header (Kimi K3, with joint credit where earlier contributors' work was continued; the IMO 2026 solutions cite the humanfia/imo2026 write-ups they were cross-checked against).

Stock CI passes — memory and speed work

All 740 problem files were profiled for peak elaboration memory (ru_maxrss) and wall time, and the heavy ones were optimized so the unmodified upstream CI (plain lake build) passes — verified on our fork (build + dashboard deploy green):

narrowed public import sets across 380+ files (import Mathlib costs ~3.4 GB + ~20 s per file; targeted imports ~1–1.6 GB + ~5 s);
decomposed brute-force computations into small verified steps in the worst offenders, e.g. Usa1981P2 11.5 → 2.3 GB, Imo1964P5 12.1 → 2.3 GB, Imo2018P4 7.6 → 1.2 GB, Usa2008P2 8.3 → 2.1 GB, Imo2023P6 12.6 → 2.5 GB, Usa2014P4 wall 187 s → 9 s;
CAS-factored the giant literal linear_combination certificates in Imo2015P4 (resultants of the coordinate elimination): elaboration peak 23.2 → 7.9 GB, wall 261 s → 70 s;
set_option Elab.async false on the four heaviest files (Usa2023P3 11.9 → 7.1 GB);
22 small module-system compatibility fixes on top of migrate to Lean's module system #235 (missing public imports that were transitively visible in legacy mode, private definitions referenced by exposed declarations, definitional-unfolding steps rewritten via equational lemmas, one delayOnMVars deadlock in Imo2022P6, attribute [local irreducible] for elaboration blowups in Imo2018P3/Imo2015P4).

A full local build of all 740 modules plus the dashboard also passes on a 4-core machine.

Notes

Compfiles/Usa2026P1.lean and Compfiles/Usa2026P4.lean overlap with upstream's own 2026 additions by Daniel Liao — our independently-written versions are included for completeness; feel free to drop either version.
Compfiles.lean is regenerated with scripts/mk_toplevel_file.bash (includes the new files).
Live dashboard of the result: https://bohanlyu.com/compfiles/

dwrensha · 2026-07-27T12:36:16Z

@@ -0,0 +1,16537 @@
+/-


Wow, that's a big file!

dwrensha · 2026-07-27T12:45:15Z


+      - name: add swap space
+        run: |
+          # Some problem files need >16GB RAM to elaborate. The runner image


I suspect that adding swap like this will make the build take a very long time. Instead, I think it would be better to omit any of the solutions that require high memory usage. They can be added back once more efficient proofs are found.

I agree. We can disable online compilation for specific problems.

By "omit" I mean: let's not include those files in this PR.

dwrensha · 2026-07-28T15:25:11Z

Since we're worrying about memory usage on this PR, I went ahead and migrated the project to Lean's module system in #235. This significantly decreased memory usage, and should give you some more headroom.

Imbernoulli · 2026-07-28T15:46:26Z

I see. I'm experimenting with a few ways to reduce the compilation burden. For example, I'm trying to import only the specific parts needed from mathlib for each problem, rather than importing the entire library.

dwrensha · 2026-07-29T23:28:30Z

Please resolve the conflicts so that I can run CI on this.

Imbernoulli · 2026-07-30T07:05:19Z

Conflicts resolved — the branch is now rebased onto current main (c3f70ab), including your module-system migration from #235. All 443 new files are in module format (module / public import / @[expose] public section), and we took your Usa2016P4 from #233 over ours.

On memory: your migration gave us a big head start, and we did a full profiling pass on top of it (per-file peak RSS via ru_maxrss). Every file above ~3.5 GB was optimized — narrowed public imports (the import Mathlib baseline is ~3.4 GB per file), decomposition of the brute-force decide enumerations, CAS-factoring of the giant literal linear_combination certificates in Imo2015P4 (23.2 → 7.9 GB), and Elab.async false on the four heaviest files. We also hit and fixed 22 module-system compatibility issues beyond #235 (transitively-visible identifiers that now need explicit public imports, a delayOnMVars deadlock in Imo2022P6, and two local irreducible elaboration blowups).

With all that, the stock CI workflow (plain lake build, no swap, no tiering) passes on our fork — build + dashboard deploy green in ~1h03m: https://github.com/Imbernoulli/compfiles/actions/runs/30492225182

CI should be ready to run here whenever you approve it. Happy to split the PR (e.g. by year range, or the memory fixes separately from the new solutions) if that makes review easier.

dwrensha · 2026-07-30T12:03:12Z

+
+## Formalization
+
+We prove the result by a coordinate computation. Every triangle is similar to a


It's fine to use a parametrization in the solution, but the formalized problem statement should be in terms of an arbitrary triangle. For this particular problem, I know that Joseph Myers is working on some supporting Mathlib infrastructure: #PR reviews > PRs towards IMO geometry 2024 P4 @ 💬

dwrensha · 2026-07-30T12:15:28Z

@@ -1,13 +1,12 @@
 /-
 Copyright (c) 2024 David Renshaw. All rights reserved.
 Released under Apache 2.0 license as described in the file LICENSE.
-Authors: David Renshaw, hillosanation
+Authors: David Renshaw, Kimi K3


hillosanation's solution is shorter than yours. Is there a reason your solution should be preferred?

dwrensha · 2026-07-30T12:18:17Z

+      · exact le_min (le_min g1 g2) (le_refl _)
+    rw [hL, hmin]; ring
+
+set_option maxHeartbeats 0 in


i would prefer to avoid increasing resource limits like this.

dwrensha · 2026-07-30T12:20:38Z

+
+## Formalization
+
+We work in Cartesian coordinates on `EuclideanSpace ℝ (Fin 2)`.  Every configuration


Again, coordinaization is fine for solutions, but the problem should be stated directly in terms of the geometric objects from the English problem statement.

dwrensha · 2026-07-30T12:26:08Z

Splitting this PR into smaller pieces would definitely help. The parts I'm most worried about are the huge files and the geometry problems. Maybe we could start with some smaller pieces that avoid those?

Imbernoulli · 2026-07-30T14:27:57Z

Split done — here's part 1, avoiding the huge files and geometry problems as you suggested: #237 (218 non-geometry problems: number theory / algebra / combinatorics, all files ≤200 KB).

Plan for the rest, once part 1 is in:

Part 2: the ~210 geometry problems (≤200 KB each)
Part 3: the 11 huge files (Usa2023P3, Imo1964P5, Imo2015P4, Imo2013P6, Usa2009P3, Imo2006P6, Imo1972P2, Imo2008P6, Imo2002P6, Imo2016P6, Imo2021P3) — all already memory-optimized (e.g. Imo2015P4 23.2 → 7.9 GB elaboration peak via CAS-factored certificates, Usa2023P3 11.9 → 7.1 GB), so they should be much less scary than they look by line count.

I'll leave this PR open as the umbrella reference and can close it once the parts land.

Second part of dwrensha#234: the geometry problems with modest file sizes (<=200KB). Module-system format, zero sorry, axioms [propext, Classical.choice, Quot.sound] only.

…rebased on ea08008; upstream's versions kept for the 9 files it already solves)

Imbernoulli · 2026-07-30T14:36:06Z

All rebased onto current main (ea08008). For the 36 files that exist on both sides, we now keep upstream's version for the 9 you already solve (Usa2016P4, Usa1983P2, Imo1979P1, Imo1988P4, Imo2022P1, Imo2025P4, Usa2007P5, Usa2017P5, Usa2026P4) and ours for the 27 that are still stubs upstream. Both PRs are mergeable again.

Part 1 (ready for review): Add formalized solutions for 218 IMO and USAMO problems (part 1: non-geometry) #237 — 218 non-geometry problems, all ≤200 KB
Part 2 (staged next): 214 geometry problems
Part 3 (staged last): the 11 huge files, already memory-optimized

Happy to adjust the boundaries — e.g. if you'd rather have part 1 smaller (single contest, or a year range first) I can re-cut it in a few minutes.

…d 2)

…(review fix)

…cs, and two note spoilers (review fix round 3)

…on, formedQuadratic triple, simp args)

dwrensha reviewed Jul 27, 2026

View reviewed changes

Comment thread Compfiles/Usa2023P3.lean

@@ -0,0 +1,16537 @@

/-

dwrensha Jul 27, 2026

Copy link
Copy Markdown

Owner

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wow, that's a big file!

dwrensha reviewed Jul 27, 2026

View reviewed changes

Imbernoulli force-pushed the upstream-pr branch 2 times, most recently from efa450e to 8d5752b Compare July 29, 2026 22:57

Imbernoulli changed the title ~~Formalize and solve all IMO and USAMO problems with CI improvements~~ Complete formalization and solutions for all IMO (1959–2026) and USAMO problems Jul 29, 2026

Imbernoulli force-pushed the upstream-pr branch from 8d5752b to f41a407 Compare July 30, 2026 07:04

dwrensha reviewed Jul 30, 2026

View reviewed changes

Imbernoulli mentioned this pull request Jul 30, 2026

Add formalized solutions for 218 IMO and USAMO problems (part 1: non-geometry) #237

Merged

Add formalized solutions for all IMO (1959-2026) and USAMO problems (…

3f9c241

…rebased on ea08008; upstream's versions kept for the 9 files it already solves)

Imbernoulli force-pushed the upstream-pr branch from f41a407 to 3f9c241 Compare July 30, 2026 14:35

Imbernoulli added 6 commits July 31, 2026 13:21

Use determine for hardcoded answers in 4 problem statements (review fix)

c9089b6

Use determine for yes/no answers and the hardcoded 7 (review fix roun…

4c5ced4

…d 2)

Remove solutions from top-level doc comments; 3 more determine fixes …

1d4bfc5

…(review fix)

Fix informal solutionImportedFrom uses, answer-revealing determine do…

6a42b99

…cs, and two note spoilers (review fix round 3)

Address Hillosanation's review round 4 (determine docs, Bool conventi…

6cfc711

…on, formedQuadratic triple, simp args)

Address Hillosanation's inline review comments on 11 files

7b80345


		## Formalization

		We prove the result by a coordinate computation. Every triangle is similar to a


		## Formalization

		We work in Cartesian coordinates on `EuclideanSpace ℝ (Fin 2)`. Every configuration

Conversation

Imbernoulli commented Jul 27, 2026 • edited Loading Uh oh! There was an error while loading. Please reload this page.

Uh oh!

Complete formalization and solutions for all IMO (1959–2026) and USAMO problems

Stock CI passes — memory and speed work

Notes

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dwrensha commented Jul 28, 2026

Uh oh!

Imbernoulli commented Jul 28, 2026

Uh oh!

dwrensha commented Jul 29, 2026

Uh oh!

Imbernoulli commented Jul 30, 2026

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

Choose a reason for hiding this comment

Uh oh!

dwrensha commented Jul 30, 2026

Uh oh!

Imbernoulli commented Jul 30, 2026

Uh oh!

Imbernoulli commented Jul 30, 2026

Uh oh!

Reviewers

Assignees

Labels

Projects

Milestone

Development

Uh oh!

2 participants

Imbernoulli commented Jul 27, 2026 •

edited

Loading