Proposal: tensor-product decomposition proof benchmark series

[DengZhiyuan-math]

Proposal

We are planning a series of proof-oriented benchmarks around tensor-product decomposition, and we would like to ask whether an OpenProver adapter would fit this repository's benchmark direction.

The first benchmark focuses on binary tensor products of O(3) irreducible representations using e3nn-style notation. For example:

2e x 3o -> 1o + 2o + 3o + 4o + 5o

Each initial problem provides the decomposition rule explicitly. The goal is to evaluate reliable rule application, mathematical explanation, and exact symbolic output rather than memorization of representation theory.

Planned benchmark series

We intend to grow the benchmark in stages:

1. Binary O(3) irreps — angular-momentum range and parity multiplication.
2. Direct sums and multiplicities — distributing tensor products and combining repeated irreps.
3. Multi-factor products — associativity, intermediate decompositions, and recoupling-style reasoning.
4. Selection rules and consistency checks — allowed channels, dimension identities, parity constraints, and detection of invalid decompositions.
5. Optional Lean track — a small reusable Lean specification and selected formally verified examples, if formal Lean statements are preferred for OpenProver integration.

Current artifacts

The current local prototype includes:

• deterministic procedural generation with fixed seeds;
• easy, medium, and hard JSONL splits;
• canonical exact scoring that rejects parity errors, missing/extra terms, duplicates, malformed syntax, and wrong ordering;
• an OpenProver adapter that converts each problem into an informal theorem document;
• a required FINAL ANSWER: marker extracted from PROOF.md and checked by the exact scorer;
• bounded batch execution with per-problem run directories and incremental results.json;
• a manual GitHub Actions smoke workflow with token and worker limits.

For the first version, the symbolic oracle remains the scoring authority. We do not plan to write hundreds of trivial per-example Lean equalities, because the expected decomposition would appear directly in each theorem target and many examples would reduce to rfl or decide. A more useful Lean contribution would be one general specification plus selected structural theorems and smoke examples.

Scope question

Which integration direction would the maintainers prefer?

1. A small runner under scripts/ that reads an externally hosted benchmark dataset.
2. A documented third-party integration maintained outside this repository.
3. A Lean-formalized benchmark adapter before upstream inclusion.
4. Another benchmark interface or result schema already planned for OpenProver.

If this direction is of interest, we can first share a small, explicitly licensed sample and a focused runner PR. We will keep the complete dataset external until its publication, provenance, and license are finalized.

Feedback on scope, preferred theorem format, and expected verification level would be very helpful before we prepare a PR.

[DengZhiyuan-math]

Implementation update

We have now organized the prototype into an OpenProver-compatible benchmark package.

The current implementation has:

• a single-problem adapter that writes THEOREM.md, invokes OpenProver in informal-proof mode, extracts exactly one FINAL ANSWER: line from PROOF.md, and applies the canonical scorer;
• a bounded batch runner with --split, --start, --limit, --dry-run, --resume, and per-problem token/worker limits;
• one run directory per problem plus an incrementally and atomically written top-level results.json;
• a machine-readable benchmark manifest describing the dataset, OpenProver mode/version, output contract, and scoring authority;
• a manual GitHub Actions smoke workflow capped at 10 problems per invocation;
• offline end-to-end tests using a fake OpenProver executable, so orchestration and scoring can be validated without model credentials.

The initial dataset remains private/local while we finalize its public repository, provenance statement, and license. We have not made a public data release or prepared an upstream PR yet.

To choose the next deliverable, two maintainer preferences would be especially helpful:

1. Would an external-dataset runner under scripts/ be useful as the first contribution?
2. Should we include a small Lean reference specification before proposing a PR, even though sample-level scoring remains exact symbolic scoring?

If an external runner is the preferred first step, we can prepare a minimal review package with the runner, manifest, tests, documentation, and 3–5 explicitly licensed sample problems. If Lean is preferred first, we will scope it to one reusable specification and selected structural theorems rather than embedding the expected answer in hundreds of trivial per-sample equality targets.