ProofJudge

Agentic LLM-as-judge evaluation harness for Mathlib (Lean 4) proof quality.

The dataset is a collection of PRs to mathlib - their first commit, and final one. The judge is rated as successful if it rates the final accepted PR over the initial rejected one.

The judge scores five dimensions independently on a 1-10 scale — library leverage, automation fit, structural clarity, statement quality, mathlib conventions. The harness combines them into a fixed weighted mean. See rubrics/rubric_v2.md.

Setup

The evaluation dataset is hosted on HuggingFace at SJCaldwell/proofjudge. Files are downloaded and cached automatically on first run via huggingface_hub.

Usage

Build Sandbox

The sandbox is used to place mathlib source code at the time of the PR, so the agentic judge can understand the context of the PR.

python scripts/run_eval.py build-image

Run Eval

You can run the eval on one datapoint, or the whole set.

# Full run
python scripts/run_eval.py evaluate

# Single PR for testing
python scripts/run_eval.py evaluate --pr 254

# Different model
python scripts/run_eval.py evaluate --model "openai:gpt-4o"

Analyze Results

python scripts/run_eval.py analyze results/results_*.jsonl --with-metadata

Configuration

All settings via env vars (prefix PROOFJUDGE_):

Variable	Default	Description
PROOFJUDGE_HF_DATASET	SJCaldwell/proofjudge	HuggingFace dataset repo ID
PROOFJUDGE_HF_DATASET_REVISION	v0.2.0	Dataset revision (tag, branch, or commit SHA)
PROOFJUDGE_SPLIT	test	test (218 held-out pairs) or dev (123 calibration pairs)
PROOFJUDGE_LOCAL_EVAL_PATH	–	Local eval.jsonl, bypasses HuggingFace (set with the next)
PROOFJUDGE_LOCAL_CONTEXTS_PATH	–	Local contexts.jsonl
PROOFJUDGE_RUBRIC_PATH	rubrics/rubric_v2.md	Rubric to score against
PROOFJUDGE_JUDGE_MODEL	anthropic:claude-sonnet-4-20250514	Pydantic AI model
PROOFJUDGE_MAX_CONTAINERS	4	Concurrent sandboxes
PROOFJUDGE_DOCKER_IMAGE	proofjudge-sandbox:latest	Sandbox image

Results layout

results_archive/rubric_v1/    runs under the original 1-7 rubric (the published Table 1)
results_archive/rubric_v2/    runs under the current rubric
results_archive/superseded/   runs retained for audit but NOT to be quoted:
                              schema-faulted, provenance-contaminated, or killed mid-run

Every result row carries rubric_sha, so a file states which rubric produced it rather than relying on its directory. A leftover *.partial.jsonl means that run did not finish.

Reproducibility notes

• Running from a git worktree needs PYTHONPATH=<worktree>; a _proofjudge.pth in the venv otherwise pins the main checkout onto sys.path and you silently score with the wrong package. The harness now refuses to run in that state.