README.md

metadata

license: cc-by-4.0
task_categories:
  - text-generation
language:
  - en
tags:
  - lean4
  - theorem-proving
  - autoformalization
  - mathematics
  - benchmark
pretty_name: ShadowBench
configs:
  - config_name: default
    data_files:
      - split: test
        path: test.jsonl

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

Field	Description
idx	Problem id. Path encodes the namespace: ABM.<area>.<level>.<problem_slug>.
informal_proof	LaTeX problem statement / informal proof
formalization_rules	Per-problem hints, including the canonical declaration name
imports	Lean 4 import lines available to your proof

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.