Import IMO 2026 Question 6 formalization

[Vilin97]

Summary

Imports the verified Lean solution of IMO 2026 Question 6 from AxiomMath/IMO2026 at commit c5a6a089d06d3619afe7ff45c5ccab9e2a30d5d2 (2026-07-17). The project proves IMO2026Q6.main_theorem: every valid common-factor sequence has positive T,L with a (n + T) = a n + L for all n.

The source solution is preserved as one namespaced module and is licensed MIT. The upstream problem statement files were not copied because they contain open sorry placeholders; Question 3 targets an older Mathlib API and was intentionally excluded. The import uses targeted Mathlib/Lean modules, has no set_option, nolint, unchecked declarations, diagnostics, or broad import Mathlib.

Discovery and selection

The exact automation window was [2026-07-05T09:01:03Z, 2026-08-29T09:01:03Z). GitHub, Zulip, and the monitored X discovery cache were queried. Other serious candidates were rejected for duplicate pool coverage (Distance Geometry), missing/invalid licensing (Crouzeix draft), forbidden compiler overrides or excessive generated certificates (Sendov and Erdős-Simonovits), legacy API drift (IMO Question 3), or incompleteness/size (Conway refinement and large solver projects).

Verification

• lake build LeanPool — 9,660 jobs, exit 0, 0 warnings.
• lake exe mk_all --check --lib LeanPool/Challenge/Solution — pass.
• scripts/ci/build-challenges.sh — pass; only expected challenge sorry notices.
• lake exe runLinter LeanPool.IMO2026 and lake exe lint-style LeanPool.IMO2026 — pass.
• python -m lean_pool.quality --repo .. — pass (including axiom/backdoor audit).
• Axiom audit: main theorem depends only on propext, Classical.choice, and Quot.sound.
• Python Ruff check/format pass. This checkout contains no Python tests; pytest --cov reports “no tests ran”.

Optimization profile

The upstream source used umbrella import Mathlib and one elaborator option. Removing the option and replacing the umbrella import with 12 targeted imports reduced the standalone module check from about 6.0s to about 2.3s on the same workspace cache; the final full-pool rebuild completed in 43.1s wall time.

[github-actions]

Proof profile (new / modified Lean files)

lake build wall time (changed modules): 15.85 s (= 0.26 min) — user 12.09 s, sys 3.10 s.

This build covers the changed modules and their dependency cones on top of the restored cache. The serial per-file sums below are useful for ranking slow files, not as a build budget.

Total heartbeats: 72 maxHeartbeats units across 2 files (818 added LOC).

Sum of lean --profile: 6796.4 ms (= 6.80 s). Import-excluded time: 4786.4 ms (= 4.79 s).

Count-heartbeats wall-clock total: 6.32 s. Repeated import cost inside lean --profile: 2010.0 ms (= 2.01 s).

Heartbeat values come from Mathlib's linter.countHeartbeats and are already in maxHeartbeats units. Per-file wall clocks are measured under parallel load and are noisier than heartbeats.

LOC counts added lines in the profiled Lean files from this PR diff.

File	LOC	Heartbeats (maxHB)	Count wall (s)	lean --profile (s)	Without import (s)	Import (s)	Decls	Errors
LeanPool/IMO2026/Q6.lean	800	72	4.18	5.63	4.63	1.00	33	0
LeanPool/IMO2026.lean	18	0	2.14	1.17	0.16	1.01	0	0
Total	818	72	6.32	6.80	4.79	2.01	33	0

Aggregate phase totals

Phase	Time
import	2010.0 ms (= 2.01 s)
tactic execution	1250.0 ms (= 1.25 s)
interpretation	1226.0 ms (= 1.23 s)
type checking	1040.0 ms (= 1.04 s)
typeclass inference	463.0 ms (= 0.46 s)
tacticAnalysis	168.0 ms (= 0.17 s)
simp	166.0 ms (= 0.17 s)
elaboration	113.1 ms (= 0.11 s)
linting	105.3 ms (= 0.11 s)
initialization	64.4 ms (= 0.06 s)
parsing	64.1 ms (= 0.06 s)
process pre-definitions	38.9 ms (= 0.04 s)

Slowest changed modules (from lake build)

Changed module	Lake time
LeanPool.IMO2026.Q6	6.10 s
LeanPool.IMO2026	1.30 s

Per-file `lean --profile` output

LeanPool/IMO2026.lean

import took 1.01s
cumulative profiling times:
	elaboration 0.139ms
	import 1.01s
	initialization 30.4ms
	interpretation 126ms
	linting 0.283ms
	module linting 0.00147ms
	overlappingInstancesLinter 0.297ms
	parsing 0.0304ms
	tacticAnalysis 1.01ms
real 1.82
user 1.03
sys 0.80

LeanPool/IMO2026/Q6.lean

import took 1s
interpretation of Mathlib.Tactic._aux_Mathlib_Tactic_Linarith_Frontend___elabRules_Mathlib_Tactic_nlinarith_1._boxed took 457ms
cumulative profiling times:
	attribute application 0.373ms
	compilation (IR) 0.267ms
	compilation (LCNF base) 3.9ms
	compilation (LCNF impure) 1.3ms
	compilation (LCNF mono) 2.64ms
	congr simp thm 6.2ms
	elaboration 113ms
	fix level params 1.75ms
	import 1s
	initialization 34ms
	instantiate metavars 12.3ms
	interpretation 1.1s
	let-to-have transformation 0.332ms
	linting 105ms
	module linting 0.00134ms
	norm_num 10.1ms
	overlappingInstancesLinter 13.9ms
	parsing 64.1ms
	process pre-definitions 38.9ms
	ring 19.2ms
	share common exprs 15ms
	simp 166ms
	tactic execution 1.25s
	tacticAnalysis 167ms
	type checking 1.04s
	typeclass inference 463ms
real 3.89
user 5.49
sys 0.81

Advisory only — never blocks merge. Full log uploaded as the proof-profile artifact.

[greptile-apps]

Greptile Summary

The PR imports a verified formalization of IMO 2026 Question 6 and exposes its global translation-periodicity theorem through Lean Pool.

• Adds the sequence predicate and supporting number-theoretic development.
• Registers the project, source revision, license, provenance, and headline declarations.
• Connects the new entry module to the aggregate Lean Pool import.

Important Files Changed

Filename	Overview
LeanPool/IMO2026/Q6.lean	Adds the complete proof pipeline from finite small-prime supports through eventual and global translation periodicity.
LeanPool/IMO2026.lean	Adds the project entry module and imports the Question 6 formalization.
LeanPool/projects.yml	Registers the IMO 2026 Question 6 project and its principal declarations.
LeanPool.lean	Exposes the new project modules through the repository-wide aggregate import.

_{Reviews (2): Last reviewed commit: "Merge remote-tracking branch 'origin/mai..." | Re-trigger Greptile}

[greptile-apps]

Misstated stabilization mechanism

The description attributes good_stabilizes_core to control by a finite prefix product, but the declaration derives stabilization from the finite range of small-prime supports; the prefix product belongs to the subsequent periodicity construction. This conflates two proof stages in the generated project catalog.

File Used: .github/REVIEW_RULES.md (source)

Note: If this suggestion doesn't match your team's coding style, reply to this and let me know. I'll remember it for next time!

[Vilin97]

Changes requested by automated review

Reviewed exact head 1c3dad463d685659c19eddad166438984be8128f. The submission is a formalization of one IMO olympiad question (800 Lean lines), which is an undergraduate/educational contest exercise rather than the serious graduate/research-level completed project required by candidates/CRITERIA.txt and the review rubric; please move it to a challenge or another educational repository instead of adding it to Lean Pool. There is also an unresolved card error: good_stabilizes_core is proved from finite small-prime support stabilization, not from the prefix product (the prefix product is introduced only in the later periodicity construction). Correct that project metadata if the work is retained elsewhere.