Large language models produce outputs presented as discoveries - new proofs, conjectures, or molecules. Whether such an output that appears creative is truly original and effective is hard to establish: open-ended outputs require subjective judgment, the output may replicate something seen in training, or the task may be too simple to need creativity. We present ALPS (Austin-Law Proof-Synthesis), a benchmark that designs a task to measure valid creativity: producing a solution that is original and can be proven correct. Each instance is a single equational law, certified to require either the construction of an infinite mathematical structure satisfying the law, or a proof that no such structure exists. Submissions are verified by automated proof checking with no human involvement, and a public generator produces new instances without limit, so LLMs are never evaluated on problems they may have seen. A portfolio of eight configurations of leading automated provers resolves 2.2% of the 4,141-law evaluation pool, and a twentyfold budget increase adds 0.6%: the obstacle is not compute, but the absence of any method that produces the tailored structure each law requires. Under a fixed protocol, the strongest reasoning model we test succeeds in 14% of instances on the proof side, but none on the construction side. The remaining 97.2% of the pool is unresolved at every configuration and budget we test. We release ALPS in full: the corpus, the generator, and the automated judge.
Figures & tables
Verifiable
Renewable
Constructive
no subjectivity
no contamination
no set procedure
Static problem sets
✓
✓
MATH, code, miniF2F
Synthetic puzzles
✓
✓
random SAT, ETP
Open discovery
✓
✓
Table 1: Each property removes one confound in measuring valid creativity: verification removes subjective judging, renewal removes contamination, and construction removes solution by any instance-independent method. Each prior benchmark family ( Hendrycks et al. 2021 ; Chen et al. 2021 ; Zheng et al. 2021 ; Selman et al. 1996 ; Bolan et al. 2025 ; Gottweis et al. 2026 ; Jumper et al. 2021 ) fulfills two of the three, but measuring valid creativity requires all three.
Molecule design
ALPS instance
Specify
target profile: bind the pocket, non-toxic, synthesizable
a law L the operation must satisfy on every assignment
Construct
propose a structure satisfying all constraints
propose a magma satisfying L
Verify
synthesis and assay confirm the profile
a proof certificate confirms the model
Table 2: Discovery proceeds by the same three phases in either domain; in ALPS, every phase is machine-checkable.
Screening stage
Removed
Remaining
Generated candidates
—
10,474
Finite-model filter
1,085
9,389
Admissibility prover
1,906
7,483
Admissible pool:
Proven trivial
3,080
Austin classes (262 laws)
195
Table 3: The screening pipeline. In the top block, each stage removes the number of candidates shown and passes the remainder to the next. The bottom block partitions the certified pool by the proofs screening produced: 3,080 proven trivial, 262 proven Austin (reported as 195 equivalence classes), and 4,141 unresolved by screening, summing to 7,483.
Figure 1: The two checks on two laws. Left: a sample submission on a toy, inadmissible law passes both checks; for admissible laws, admissibility forces the witnessing model to be infinite. Right: o4-mini’s submission on a hard-tier law passes check (a) but fails check (b), the “too-strong” failure mode most common across the LLMs we evaluate.
Budget (s)
New models
New trivial
Unresolved
30
4
87
4,050
60
0
8
4,042
120
0
5
4,037
300
0
4
4,033
600
0
6
4,027
Table 4: Newly resolved laws at each per-configuration budget over the 4,141-law residual. All models appear at 30 seconds; every later resolution is a triviality proof, and 4,027 laws (97.2%) remain unresolved.
Certified-easy ( n=63 )
Hard ( n=25 )
LLM
Default
Waypoints
↓ Effort
Construction
GPT-4.1
0
0
—
0
o4-mini
0
0
0
0
o3
6
9
0
0
Table 5: Verified LLM solves under the fixed protocol. Waypoints are prover-derived lemmas included in the prompt. Reasoning effort is medium except where marked ↓ , which denotes low effort; GPT-4.1 has no effort setting.
Appendix figures & tables4 assets
Supplementary material from the paper’s appendix.
Appendix
Configuration
30
60
120
300
600
Total
Models
twee/complete
69
5
4
3
5
86
4
eprover/triv/auto
64
2
2
1
1
70
0
vampire/triv/casc+lpo
30
1
1
1
0
33
0
vampire/triv/casc
24
1
0
1
0
26
0
vampire/triv/discount
22
0
0
0
0
22
0
vampire/sat/otter+lpo
13
1
0
0
0
14
0
Appendix
Table A1: Distinct laws resolved by each configuration at each per-configuration budget in seconds, over the 4,141-law residual. Counts overlap across configurations. “Models” counts laws resolved by exhibiting a nontrivial model rather than by proving triviality.
LLM
Too strong
Too weak
Both fail
One check
o3
23
2
0
25
o4-mini
11
4
10
15
GPT-4.1
10
11
4
21
Appendix
Table A2: Final-round classification of all 25 hard-tier construction submissions per LLM. “Too strong” entails the law but admits only one-element models (passes check (a), fails (b)); “too weak” maintains two distinct elements but fails to entail the law (passes (b), fails (a)). The last column counts laws on which the LLM clears exactly one of the two checks.
Order
Screened
Austin
Austin per 1,000
5
115
11
95.7 ‡
6
1,418
29
20.5
7
4,803
117
24.4
8
4,138
105
25.4
Appendix
Table A3: Admissible-law yield by order, over all 10,474 screened candidates. Density rises monotonically across the orders the extension engine generates, so the supply does not thin as the corpus grows. ‡ Order 5 is excluded from the trend: those laws come from ETP’s curated enumeration rather than a uniform draw from the generator.
Run
Records
Completion
Prompt
o3 cert-63, waypoints
127
3,094,531
164,044
o3 cert-63, no waypoints
99
3,289,573
130,963
o3 low effort
9
152,309
20,724
o3 reproduction
14
575,997
59,653
o4-mini cert-63
63
974,972
147,300
GPT-4.1 cert-63, waypoints
63
61,670
149,538
Appendix
Table A4: Token usage across all reported language-model runs. A solved certified-easy law costs a median of 49,221 completion tokens.