Humanfia at IChO 2026

Note

This is part of RSI Effort at NVIDIA Research. Humanize is an open agent loop/flow framework that led by NVIDIA Research, UCLA PolyArch, and MIT HAN Lab. We are skying the limit with the power of agents with community members.

The GPT full-theory experiment has completed all 68/68 Lean formalization targets across the 9 IChO 2026 theory problems, under their declared input scopes: 66 original-input results and 2 explicitly conditional results. See the complete formalization release. This is a formalization-completion result, not a claim of 100% official-answer accuracy.

Kimi-K3 has now also completed all 68 numbered theory subquestions: the earlier 32-target answer-blind run plus the remaining 36 formalizations. Combined coverage is 68/68 under those two releases' disclosed scopes. This is likewise formalization completion, not a claim of 100% official-answer accuracy.

The earlier GPT selected-set experiment remains 32/32 answer-blind. The projects are pinned to Lean 4.31.0 and Mathlib v4.31.0.

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

• the complete GPT full-theory formalization: 68 subquestions, including the latest T8-A8 contest-model proof and its 12 checked lemmas;
• the GPT-5.6 Sol native Codex /goal baseline: 68/68 compiled, 32/68 (47.06%) independently accepted;
• the Kimi-K3 native Codex /goal baseline: fresh 68-target run, 31/68 (45.59%) independently accepted; 2 review-format errors disclosed;
• the Kimi-K3 remaining 36 formalizations, which together with the earlier 32 answer-blind targets cover all 68 theory subquestions;
• the final answer-blind Lean 4 statements and proofs Kimi-K3 and GPT-5.6 Sol;
• the final worked solutions Kimi-K3 and GPT-5.6 Sol;
• the grading reports, experiment records, checksums, and provenance used to audit the results.

Notably, humanize enables open source models like Kimi-K3 to achieve 68/68 Lean formalization coverage at IChO 2026 (32 answer-blind + 36 remaining) as well! As Jensen shared, We all love open models X open harness 🎉 and the combination achieves full score at every competition:

• IMO2026 / IOI2026 / IPhO2026 / IChO2026 / IBO2024

Results

Separate native Codex /goal baseline

Experiment	Scope	Lean compilation	Semantic review	Combined acceptance	Official-answer score
GPT-5.6 Sol native /goal	68 subquestions, peak 32 concurrent	68/68	45/68	32/68 (47.06%)	415/437 (94.97%); 57.875/60 (96.46%)
Kimi-K3 native /goal	68 subquestions, peak 32 concurrent	66 canonical + 2 alternate-path	46/68	31/68 (45.59%)	340.2/437 (77.85%); 47.674/60 (79.46%)

The Kimi native run has 67 completed goals and one final failure (T1-A6). Independent review produced 66 structured verdicts and 2 format errors; proof review passed 44/68. It is separate from the historical Kimi 32+36 run.

These fresh answer-blind baselines use native persisted goals, not the Humanize review/redraft solver loop. Independent post-run reviews did not feed back into the solvers. All 68 original outputs, including rejected, blocked and conditional results, are preserved. The 47.06% and 45.59% figures are formalization acceptance; the chemistry scores are separate official-rubric comparisons. See the GPT protocol and grade and the Kimi protocol and grade.

Full theory formalization: 68/68 targets accepted

Experiment	Theory coverage	Formalization review	Proof review	Declared scope
GPT-5.6 Sol full68	9 problems / 68 numbered subquestions	68/68	68/68	66 original-input + 2 conditional
Kimi-K3 32+36	9 problems / 68 numbered subquestions	68/68	68/68	32 answer-blind + 31 original Kimi-NL + 3 conditional + 2 authorized corrections

All theoretical-paper formalization targets have passed the experiment's acceptance gates. T4-A8 supplements the printed flow unit with m³/day. T8-A8 uses two user-authorized, experiment-local contest-model axioms: the dark condition has no drawn H₂/CO product stack, and higher photon energy among the three illuminated conditions implies a strictly larger H₂ mole fraction. These are disclosed model inputs, not additional facts proved from the problem figures or universal chemistry laws. The latest T8 proof concludes a=N, b=B, c=G, d=R and includes 12 rechecked lemmas.

Kimi-K3's 68/68 is the union of two published campaigns, not a fresh full-paper answer-blind rerun. The additional 36-target release formalizes supplied Kimi natural-language answers. Its disclosed scopes are T2-A6, T7-A6 and T8-A8 (conditional contest-model inputs) plus authorized answer corrections on T1-A1 and T8-A4. The remaining 31 of those 36 preserve the original Kimi answers. Combined with the earlier 32 answer-blind targets, that is 68 distinct numbered subquestions.

Lean checks deductions from the encoded inputs; it does not itself certify that every encoding matches the official chemical answer. Post-run answer scoring is separate and is not represented by 68/68. The historical selected-set scores in their own section belong to different experiments.

Full68 answer scoring — generous, non-official

Run	Raw points	Raw accuracy	Weighted theory score	Weighted accuracy
GPT-5.6 Sol full68	424.5/437	97.14%	58.736/60	97.89%
GPT-5.6 Sol native /goal	415/437	94.97%	57.875/60	96.46%
Kimi-K3 native /goal	340.2/437	77.85%	47.674/60	79.46%
Kimi-K3	417.5/437	95.54%	58.209/60	97.02%

This user-requested generous grading accepts equivalent representations, reasonable rounding and justified partial credit, without erasing substantive chemical errors. It is not an official IChO jury score. GPT full68's remaining deductions are T3-A3 (15/23) and T8-A4 (24.5/29). The GPT native /goal score is a separate official-rubric comparison of those frozen answers; its main deductions are T3-A1/A2, T3-A3 (21/23), T8-A4 (20/29), T8-A6 (6/10) and T9-A8 (16/18). The Kimi native /goal score is likewise a separate official-rubric comparison; its larger deductions include T3-A3 (12/23), T3-A6 (0/12), T6-A6 (9/20), T7-A3 (2/15) and T8-A8 (0/4). Kimi's published Humanize score is the independent official-key regrade of the nine natural-language solutions; the 32+36 Lean artifacts were not given a second generous marking. Formalization 68/68 and these answer scores measure different things.

Answer-blind Lean results — all 68 theory subquestions

The table below covers every numbered theory subquestion, not the earlier 32-target subset. Official-answer comparison happened only after generation and review had finished. These scores are rubric reconstructions, not IChO jury scores.

GPT-5.6 Sol Humanize uses the complete 68-target formalization. Kimi-K3 is the 32-target answer-blind run plus the remaining 36 formalizations. Native /goal is a one-shot baseline with no review/redraft, so its Lean pass rate is much lower. The old selected-set snapshot remains 168/168 raw and 47/47 outputs on those 32 IDs for the two Humanize runs; see the GPT validation report.

Run	Expected raw rubric points	Formalization review	Proof review	Lean build	Placeholders	Official-answer comparison
GPT-5.6 Sol	424.5/437 (97.14%)	68/68	68/68	passed	0	424.5/437
Kimi-K3	417.5/437 (95.54%)	68/68	68/68	passed	0	417.5/437
GPT-5.6 Sol native /goal	415/437 (94.97%)	45/68	32/68	passed	0	415/437
Kimi-K3 native /goal	340.2/437 (77.85%)	46/68	44/68	66/68 canonical	0	340.2/437

The normalized records are published in the humanfia-lab/icho-2026 dataset. Those records include official solution and rubric text as post-run evaluation metadata; those fields were never model inputs.

Historical natural-language runs

The earlier natural-language-only experiments are separate from the full68 formalization release. Their original grading reports remain available: GPT-5.6 Sol max and Kimi-K3 max. Their scores are not reused for full68.

The historical Kimi campaign used anthropic-kimi-k3 through Claude Code as the model client, with Humanize providing the agent loop and review workflow. Its four grounding-log completeness warnings are disclosed in the run README; they do not change the compile or proof-review results.

Reproduce the verified result

Clone the repository and verify the released files:

git clone https://github.com/humanfia/icho2026.git
cd icho2026

for run in gpt-5.6-sol-answer-blind kimi-k3-answer-blind kimi-k3-nl-36-formalization gpt-5.6-sol-native-goal68 kimi-k3-native-goal68; do
  (cd "$run" && sha256sum -c CHECKSUMS.sha256)
done

Build the pinned Lean projects:

for run in gpt-5.6-sol-answer-blind kimi-k3-answer-blind kimi-k3-nl-36-formalization; do
  (
    cd "$run"
    lake exe cache get
    lake build
  )
done

A successful lake build type-checks the released formalizations and proofs under the toolchain pinned inside each project.

For the complete 68-question GPT project and its separate 13-module T8 audit, follow the full68 reproduction instructions. The Kimi remaining-36 project has its own reproduction notes. The native /goal baselines are separate per-target Lean projects; see the GPT verification notes and the Kimi verification notes.

Released artifacts

• gpt-5.6-sol-max and kimi-k3-max contain Q1.md through Q9.md.
• Each full-paper run includes GRADING.md and EXPERIMENT.md.
• gpt-5.6-sol-answer-blind and kimi-k3-answer-blind are standalone Lean 4 projects with pinned dependencies and checksums.
• kimi-k3-nl-36-formalization is the remaining 36-target Kimi Lean project; together with kimi-k3-answer-blind it covers all 68 theory subquestions.
• gpt-5.6-sol-native-goal68 is the separate GPT-5.6 Sol native Codex /goal baseline over all 68 theory subquestions.
• kimi-k3-native-goal68 is the separate Kimi-K3 native Codex /goal baseline over all 68 theory subquestions.
• FIRST_TURN_ABLATION.md compares the nine unreviewed Kimi round-0 outputs with the final Humanize result under the same grading convention.

Scope

The preserved runs cover the nine theoretical problems. The separate practical laboratory examination is not part of these model runs or scores.