humanfia-lab/ipho2026-formalized-results

IPhO 2026 Lean formalization results This dataset publishes two independent Lean 4 solution sets for the 23 theoretical subproblems of IPhO 2026: Result set Theory targets Compiles Active proof placeholders Codex v2 23/23 yes 0 Kimi K3 23/23 yes 0 The six selected experimental targets are outside the requested accuracy scope and are not included here. Each result directory is a standalone Lean project containing the theorem files and pinned build dependencies.… See the full description on the dataset page: https://huggingface.co/datasets/humanfia-lab/ipho2026-formalized-results.