With the power of Humanize, we, the Humanfia team, have aced all 6/6 IMO 2026 problems using a fully agentic, YOLO-style approach. Every solution has been formally verified by Lean 4.

We build with open source, and build for open source. We release everything including:

• the formal Lean 4 statements from AxiomMath;
• the final lean solutions (gpt and kimi);
• the exact GPT and Kimi plans, shared Codex review template, and scripts used to reproduce the solving process.

The project is pinned to Lean 4.31.0 and Mathlib v4.31.0.

Both the Humanfia(GPT-5.6) and Humanfia(Kimi-K3) workers solved all six problems. The Kimi-k3 run is a hybrid: a Kimi worker paired with a Codex reviewer, and its numbers below are the combined worker + reviewer cost. Times are API time consumption (time actually spent in model API calls), compared with the times reported by AxiomProver. The fastest reported time for each problem is bolded.

The formal Lean 4 problem statements under base/IMO2026 are sourced from AxiomMath/IMO2026. The AXLE verifier sends an original statement and candidate proof to the configured verification endpoint and writes a JSON report.

python3 scripts/verify-imo2026-axle.py \
  --problem imo2026_q1 \
  --original base/IMO2026/Q1/problem.lean \
  --candidate gpt-5.6-solution/IMO2026Q1.lean \
  --output reports/gpt-5.6-q1.json

This step requires outbound HTTPS access. The defaults are a 900-second request timeout and four retries. Exit status 0 means AXLE returned okay: true, 1 means the proof was rejected, and 2 means verification or input handling failed.

• Humanize
• Elan, which provides Lean and Lake
• Git
• Python 3 for the validation and AXLE scripts
• A C/C++ build toolchain required by Lean dependencies
• Internet access during the first Mathlib setup

Lean is installed through Elan, the Lean toolchain manager. On Ubuntu or Debian, first install the system packages needed by Elan and Lean:

sudo apt-get update
sudo apt-get install -y curl git build-essential

On macOS, install the Xcode command-line tools instead:

xcode-select --install

Then install Elan on either platform:

curl https://elan.lean-lang.org/elan-init.sh -sSf | sh
source "$HOME/.elan/env"

Verify the installation from this repository. Entering base makes Elan download and select the project's pinned Lean 4.31.0 toolchain automatically:

(
  cd base
  lean --version
  lake --version
)

The Lean version should be 4.31.0. If elan, lean, or lake is not found, open a new shell or run source "$HOME/.elan/env" again. A global elan default is unnecessary because base/lean-toolchain pins the version for this project. See the official Lean installation guide for other platforms.

From the repository root:

(
  cd base
  lake update
  lake exe cache get
  lake build
)

The lean-toolchain file makes Elan select Lean 4.31.0 automatically. The Mathlib cache step avoids compiling all of Mathlib from source.

Run Lean from the base project so it uses the pinned Mathlib environment:

(cd base && lake env lean ../gpt-5.6-solution/IMO2026Q1.lean)

To check the corresponding Kimi solution:

(cd base && lake env lean ../kimi-solution/IMO2026Q1.lean)

Lean normally prints nothing when a file succeeds. A compilation error causes a non-zero exit status.

cd base

for solution_dir in ../gpt-5.6-solution ../kimi-solution; do
  for solution in "$solution_dir"/*.lean; do
    echo "Checking $solution"
    lake env lean "$solution"
  done
done

lake build alone does not compile the files in the two solution directories, so use the explicit lake env lean commands above.

The local validator checks that a candidate:

• preserves the original definitions, theorem signatures, theorem order, and protected docstrings;
• contains none of sorry, admit, axiom, or native_decide;
• retains the required namespace terminator for Q3 and Q4.

It is a structural check, not a replacement for Lean type-checking.

Run this command from the repository root:

python3 scripts/validate-imo2026-output.py \
  --problem imo2026_q1 \
  --original base/IMO2026/Q1/problem.lean \
  --candidate gpt-5.6-solution/IMO2026Q1.lean

for solution_dir in gpt-5.6-solution kimi-solution; do
  for question in 1 2 3 4 5 6; do
    python3 scripts/validate-imo2026-output.py \
      --problem "imo2026_q${question}" \
      --original "base/IMO2026/Q${question}/problem.lean" \
      --candidate "${solution_dir}/IMO2026Q${question}.lean"
  done
done

Copy a problem skeleton, replace its proof placeholders, and keep the original declarations and theorem headers unchanged:

cp base/IMO2026/Q1/problem.lean /tmp/IMO2026Q1.lean
${EDITOR:-vi} /tmp/IMO2026Q1.lean

Then run both local checks:

python3 scripts/validate-imo2026-output.py \
  --problem imo2026_q1 \
  --original base/IMO2026/Q1/problem.lean \
  --candidate /tmp/IMO2026Q1.lean

(cd base && lake env lean /tmp/IMO2026Q1.lean)

Change q1, Q1, and IMO2026Q1.lean consistently for another problem.

Comparator and Landrun binaries are not included in this repository. If you already have them, build the bundled lean4export source:

(cd tools/lean4export && lake build)

The runners require the resulting executable together with Comparator and Landrun in the runtime template:

install -m 0755 tools/lean4export/.lake/build/bin/lean4export \
  /tmp/imo2026-humanize-runtime-v431/checker-tools/lean4export

Each experiment creates its own problem-specific Comparator challenge and configuration inside the isolated workspace, then invokes scripts/check-with-comparator.sh.

The experiment harness is separate from ordinary proof checking. It was built for a pre-provisioned Linux environment and is not a portable one-command runner for macOS or a fresh Linux installation.

Run one question through the GPT-5.6 worker/reviewer pipeline with the exact checked-in experiment plan:

bash scripts/run-imo2026-gpt-5-6.sh \
  --prompt gpt_plan.md \
  --question problem/2026-q1.lean

The question name selects Q1 through Q6. If the named path does not exist, the entrypoint uses the corresponding canonical statement under base/IMO2026. An existing question file is used directly and snapshotted into the isolated workspace. gpt_plan.md is the parameterized form of the active plan embedded in the successful experiment shell. The runner renders its problem, module, model, and turn-limit placeholders before starting the loop. The shared Codex review prompt is regular-review.md.

Validate the interface and prerequisites without creating a run:

bash scripts/run-imo2026-gpt-5-6.sh \
  --prompt gpt_plan.md \
  --question base/IMO2026/Q1/problem.lean \
  --dry-run

Additional options such as --run-id, --out-root, --max-turns, --prepare-only, and the recovery modes are forwarded to the internal scripts/run-imo2026.sh engine.

Run one question using Kimi K3 as the worker, Codex as the reviewer, and the exact checked-in Kimi experiment plan:

bash scripts/run-imo2026-kimi-k3.sh \
  --prompt kimi_plan.md \
  --question problem/2026-q1.lean

The compact entrypoint has the same question-path behavior as the GPT-5.6 entrypoint. kimi_plan.md is rendered with the selected problem, module, model, reviewer, and turn-limit values. Additional runner options are forwarded to the native Kimi-worker/Codex-reviewer engine in scripts/run-imo2026-kimi.sh.

The repository does not require an inputs/ directory. The compact entrypoints select one problem from --question; the full engines default internally to Q1–Q6. --problem can select one or more explicit IDs, and --failure-file remains available as an optional override.

The harness expects:

• Linux utilities including proot, setpriv, getent, flock, jq, rg, a C compiler, and GNU timeout;
• a working Codex binary and Codex configuration/authentication directory;
• for Kimi runs, native Kimi Code with a configured K3 alias and thinking enabled;
• a populated base/.lake/packages Mathlib checkout;
• an external Comparator binary and Landrun binary;
• a runtime template containing Lean, Mathlib, Comparator, Landrun, and lean4export;
• /mathlib-packages linked to the pinned package cache;
• isolated users named humanize-imo-q1 through humanize-imo-q6, unless HUMANIZE_USER_PREFIX is changed.

The default runtime template layout is:

/tmp/imo2026-humanize-runtime-v431/
├── root/.elan/bin/lake
├── mathlib-packages/mathlib/
├── checker-tools/lean4export
└── comparator-tools/
    ├── comparator
    └── landrun

The checked-in scripts do not have executable file modes, while the harness requires its Comparator wrapper to be executable. Prepare them once with:

chmod +x scripts/*.sh scripts/*.py

The files scripts/nonet-preload.c and scripts/nonet-shell.c are intentionally kept as runtime dependencies. At the start of a run, each engine compiles nonet-preload.c into an LD_PRELOAD library that rejects socket creation and connection/bind operations with EACCES. It compiles nonet-shell.c into the worker shell that installs that preload library before executing the real shell. This supplements the runner-generated seccomp socket-denial wrapper and keeps worker shell commands offline; reviewers retain only the network access required for AXLE verification.

After provisioning the environment, run one problem first:

BASE_CODEX_HOME=/path/to/codex-home \
CODEX_BIN=/path/to/codex \
LOCAL_RUNTIME_TEMPLATE=/tmp/imo2026-humanize-runtime-v431 \
bash scripts/run-imo2026.sh \
  --problem imo2026_q1 \
  --jobs 1 \
  --fallback-jobs 1 \
  --probe-count 1

This runner is fixed to the gpt-5.6-sol model and rejects another CODEX_MODEL value.

Install the native kimi command on Linux or macOS with the official installer:

curl -fsSL https://code.kimi.com/kimi-code/install.sh | bash
kimi --version
kimi login

Kimi Code stores its configuration, credentials, and sessions under ${KIMI_CODE_HOME:-$HOME/.kimi-code}. Do not commit that directory. The native worker shell requires the resolved binary path and a readable configured home:

export BASE_KIMI_HOME="${KIMI_CODE_HOME:-$HOME/.kimi-code}"
export KIMI_BIN="$(readlink -f "$(command -v kimi)")"
test -s "$BASE_KIMI_HOME/config.toml"

See the official Kimi Code installation guide for Windows, npm, upgrade, and login instructions. The Kimi configuration must define the kimi-for-coding/k3 alias with model ID k3 and thinking enabled.

Run one problem first. Native Kimi performs the proof work and Codex performs the isolated AXLE-backed review:

BASE_KIMI_HOME=/path/to/kimi-code-home \
BASE_CODEX_HOME=/path/to/codex-home \
KIMI_BIN=/absolute/path/to/kimi \
LOCAL_RUNTIME_TEMPLATE=/tmp/imo2026-humanize-runtime-v431 \
bash scripts/run-imo2026-kimi.sh \
  --problem imo2026_q1 \
  --jobs 1 \
  --fallback-jobs 1 \
  --probe-count 1

The Kimi worker model is fixed to kimi-for-coding/k3. The reviewer defaults to Codex model gpt-5.5 with xhigh reasoning effort.

Use bash scripts/run-imo2026.sh --help for the GPT options and bash scripts/run-imo2026-kimi.sh --help for the Kimi-worker/Codex-reviewer options.

Useful options include:

• --problem imo2026_qN — select a problem; repeat to select several;
• --max-turns N — set the worker/reviewer turn limit;
• --prepare-only — create and audit isolated workspaces without starting a model;
• --resume-prepared, --resume-worker-only, and --resume-review-only — continue an existing run;
• --run-id ID and --out-root PATH — control result locations.

Even --dry-run performs the harness prerequisite checks.

Recovery must reuse the original RUN_ID, OUT_ROOT, LOCAL_RUNS_ROOT, LOCAL_RUNTIME_TEMPLATE, and credential locations. Preserve both $OUT_ROOT/$RUN_ID, which contains job state and provenance, and $LOCAL_RUNS_ROOT/$RUN_ID, which contains the real workspaces and per-job model homes. The workspaces and agent-homes entries in the output directory are symlinks into that local run tree; keeping only the output directory is not enough to resume.

Restore the original environment and inspect each job's state before choosing a recovery mode:

export RUN_ID=the-original-run-id
export OUT_ROOT=/path/to/original/output-root
export LOCAL_RUNS_ROOT=/path/to/original/local-runs-root
export LOCAL_RUNTIME_TEMPLATE=/path/to/imo2026-humanize-runtime-v431

find "$OUT_ROOT/$RUN_ID/jobs" -name status.txt -print -exec cat {} \;

Use --resume-prepared only for jobs in prepared or pending state:

bash scripts/run-imo2026.sh --run-id "$RUN_ID" --resume-prepared

Worker-only and reviewer-only recovery each require exactly one selected problem. They preserve the prepared workspace and continue the recorded round:

bash scripts/run-imo2026.sh --run-id "$RUN_ID" \
  --problem imo2026_q1 --resume-worker-only

bash scripts/run-imo2026.sh --run-id "$RUN_ID" \
  --problem imo2026_q1 --resume-review-only

For a Kimi-worker/Codex-reviewer run, use the same environment and replace run-imo2026.sh with run-imo2026-kimi.sh. Also restore the original BASE_KIMI_HOME, BASE_CODEX_HOME, and KIMI_BIN. Do not start a new run, delete either preserved run tree, or copy a candidate into a fresh workspace as a substitute for recovery.

Runs are written under runs/<RUN_ID>/. Important artifacts include:

• RUN.md — run configuration and provenance;
• jobs/ — per-problem status, hashes, and local-check logs;
• metrics.tsv — final per-job status and timing;
• codex-sessions.tsv — GPT worker/reviewer sessions or Kimi-run Codex reviewer sessions;
• kimi-sessions.tsv — Kimi worker sessions for hybrid runs;
• workspaces and agent-homes — links to the isolated runtime directories;
• rate-limit and transport-failure logs when those conditions occur.

Workers have network access blocked. Reviewers receive network access only for the prompted AXLE verification step. Existing solution directories are not mounted into either model namespace.