IMO 2026 Lean Formalization

This repository contains Lean 4 formalizations and machine-checked proofs of all six problems from the 2026 International Mathematical Olympiad (IMO).

The formalization was produced with the Quokka pipeline.

View the compiled project online.

Author contact: zichenwang25@stu.pku.edu.cn

Problems

The official source of the problems is the IMO 2026 problems page.

If you are not familiar with Lean, you can also read the natural-language solutions translated directly from the machine-checked Lean proofs.

Browse all six rendered solutions online or download the combined PDF.

Problem	Statement	Formalized	Solution	Lean	Lines	Time
Q1	Natural language	Lean statement	Markdown · PDF · HTML	Proof	481	50 min
Q2	Natural language	Lean statement	Markdown · PDF · HTML	Proof	772	88 min
Q3	Natural language	Lean statement	Markdown · PDF · HTML	Proof	1,724	105 min
Q4	Natural language	Lean statement	Markdown · PDF · HTML	Proof	673	70 min
Q5	Natural language	Lean statement	Markdown · PDF · HTML	Proof	370	46 min
Q6	Natural language	Lean statement	Markdown · PDF · HTML	Proof	440	43 min

Each entry separates the official natural-language problem, its formalized Lean statement, the corresponding natural-language solution, and the machine-checked Lean solution. The formalized statement files are the successful pre-proof outputs and intentionally retain sorry. Line counts refer to the complete Lean solution files. Times are rounded total per-problem cumulative times.

Verification

Run the complete verification and print the axiom dependencies of the six main results:

./verify.sh

The script compiles all six complete proof files and fails if any main result depends on sorryAx. Standard Lean and mathlib axioms such as propext, Classical.choice, and Quot.sound may appear in the printed report.

Current repository verification result:

Check	Result
Complete proofs	P1–P6 compile successfully
Main theorem axioms	propext, Classical.choice, Quot.sound
sorryAx in main results	None
Toolchain	Lean 4.32.0, mathlib v4.32.0

Run Report

All six problems completed successfully.

Results

Problem	Result
P1	Success
P2	Success
P3	Success
P4	Success
P5	Success
P6	Success

Resource Usage

Reporting convention: each problem is divided into exactly two stages, stmt and proof. The stmt stage covers all processing performed before proof begins. Durations are cumulative wall times reported by the service and rounded to the nearest second. Because the problems ran concurrently, the summed durations represent cumulative compute time rather than the batch's elapsed clock time.

Problem	stmt time	stmt tokens	proof time	proof tokens	Total time	Total tokens
P1	00:21:22	318,715	00:28:52	627,482	00:50:14	946,197
P2	00:14:41	296,165	01:12:54	1,376,600	01:27:34	1,672,765
P3	00:34:28	466,762	01:10:43	854,439	01:45:12	1,321,201
P4	00:36:43	706,044	00:33:15	415,329	01:09:58	1,121,373
P5	00:19:58	345,610	00:26:26	415,247	00:46:24	760,857
P6	00:16:17	334,493	00:26:41	499,169	00:42:58	833,662
Total	02:23:29	2,467,789	04:18:52	4,188,266	06:42:21	6,656,055

Summary

• All six problems completed both stmt and proof successfully.
• No task retries or provider retries occurred.
• proof accounted for approximately 62.93% of the total token usage.
• P2 had the highest total token usage at 1,672,765 tokens.
• P3 had the longest cumulative time at 01:45:12.