ShadowBench

Test split for the ICML 2026 AI4Math Workshop & Challenge 4 — ShadowBench: end-to-end autoformalization and theorem proving in Lean 4. Given a natural-language proof, a list of allowed Lean 4 imports, and formalization rules, produce a Lean 4 snippet that states the canonical theorem and proves it.

This release ships 126 curated problems. The competition splits them into two phases on Codabench:

• Validation Phase — 10 L2 problems (annotated). Use this to verify your submission format and pipeline. Generous submission limits, instant feedback.
• Evaluation Phase — all 126 problems (L2/L3/L4 across 8 areas). Counts toward the final leaderboard.

The same test.jsonl covers both phases; Codabench decides which subset to score against the submission.

Fields

Submission

Submit on Codabench. One .jsonl per submission, one row per problem:

{"idx": "...", "formal_proof": "<full Lean snippet>", "llm_history": [{"role": "...", "content": "..."}]}

llm_history is required (non-empty chain of role/content messages).

See the competition page for full rules and grading.