Datasetpublic

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.

sourceHugging Faceotherupdated 2mo agoView on Hugging Face

0likes123downloads

Dataset Card

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.

This repository contains release artifacts only.

Layout

—codex-v2/: Codex v2 formalizations and proofs.
—kimi-k3/: Kimi K3 formalizations and proofs.
—RESULTS.md: scope and verification summary.
—manifest.json: source revisions and release metadata.

Build

Run the following in either result directory:

bash

lake exe cache get
lake build

The original IPhO material remains subject to the rights of its authors and organizers. This repository does not assert a new license over the source problems.