Dataset · Hugging Face

humanfia-lab/icho-2026

Name: icho-2026
Creator: humanfia-lab
License: other
Keywords: task_categories:text-generation, language:en, license:other, size_categories:n<1K, format:json, modality:text, library:datasets, library:pandas, library:polars, library:mlcroissant, region:us, chemistry, lean, theorem-proving, formalization

IChO 2026 Lean 4 formalizations: verified model variants This repository contains three independently generated Lean 4 proof sets for the same 32 selected IChO 2026 theory subquestions. Practical papers P1–P3 remain outside the corpus. Proof-origin labels Config Records proof_generator.label Meaning kimi-k3 32 Kimi-K3 Proofs generated in the clean K3 rerun with kimi-k3[1m] through Claude Code. gpt 32 GPT Proofs generated in a fresh answer-blind… See the full description on the dataset page: https://huggingface.co/datasets/humanfia-lab/icho-2026.

View on Hugging FaceReport an issue

Author / organization	humanfia-lab
License (as declared)	other
Downloads	149 (as reported by Hugging Face)
Likes	0
Created	11 August 2026
Last updated at source	1 September 2026

chemistryleantheorem-provingformalization

Embed this entry

<iframe src="https://silytics.si/embed/item/ddf81cc5-51d3-4e49-aa8e-14962198a0b5" width="420" height="190" style="border:0" loading="lazy" title="Silytics entry"></iframe>

Free, no tracking. More about feeds and embeds.

Popularity, last 2 days

149 now (+6 since 2026-10-16). Counts as reported by the source, snapshotted daily by Silytics.

More from humanfia-lab

Silytics shows public metadata from Hugging Face and links to the original. Information may be incomplete or out of date. Last refreshed 17 October 2026. Licenses and terms of the original apply to the work itself. Not financial, legal or professional advice.