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.
We present a new approach for benchmarking Large Language Model (LLM) capabilities on research-level mathematics. Existing benchmarks largely rely on static, hand-curated sets of contest or textbook-style problems as proxies for mathematical research. Instead, we establish an updatable benchmark evaluating models directly on the latest research results in mathematics. This consists of an automatic pipeline that extracts lemmas from arXiv and rewrites them into self-contained statements by making all assumptions and required definitions explicit. It results in a benchmark that can be updated regularly with new problems taken directly from human mathematical research, while previous instances can be used for training without compromising future evaluations. We benchmark current state-of-the-art LLMs, which obtain around 10-15% accuracy in theorem proving (pass@1) depending on the model, showing that there is currently a large margin of progression for LLMs to reach human-level proving capabilities in a research context.
Antoine Peyronnet, Fabian Gloeckle, Amaury Hayat
1Ecole Normale Superieure de Rennes · 2Ecole des Ponts Paris · 3Korean Institute for Advanced Study
How should we assess whether large language models can perform mathematical invention? I argue that this question is currently underspecified: mathematical creativity is not one capacity but several mechanistically distinct modes of meaning-making - reflexive introspection on mathematical practice, analogical import from the sciences, problem-driven construction, and the bridging of distant domains - together with a further, cross-cutting distinction between meaning pursued because a pattern was observed and meaning pursued because it is strategically wanted, a distinction I develop through the case of conjecture-formation. These mechanisms are likely non-substitutable, so that competence in one does not transfer to the others. Grounding each in a historical case study and in an architecture-level account of current transformer-based systems, I suggest that today's models concentrate their competence in modes shaped by recombination and search over existing building blocks; if that description holds, the remaining modes are out of reach in principle, not just slower - though whether it holds is itself the open, empirical part. Because proof is getting cheaper as AI improves at generating it - a shift the field's own leading voices are now diagnosing - mathematical value is migrating toward the modes current systems cannot yet perform, and evaluations of AI mathematical ability should be organized around this taxonomy rather than around aggregate benchmarks that conflate it.
Large Language Models (LLMs) are being applied to increasingly difficult problems and use cases. To navigate their vast solution spaces effectively, LLMs need to be creative. Yet the subjective nature of creativity and the limits of human judgment make training LLMs for creativity especially challenging. As a solution, we train LLMs on Codenames, a word-association game that exercises the two central axes of creativity, divergent and convergent thinking, while yielding objectively verifiable outcomes. This verifiability lets us bypass human judgment and train with Reinforcement Learning with Verifiable Rewards (RLVR). We train Qwen3-1.7B, 4B, and 8B models and evaluate them on ten creativity and four reasoning benchmarks. We find that the precision-diversity trade-off is scale-dependent: the 8B model prioritizes creativity over precision, while the 1.7B and 4B models gain reasoning precision at the cost of creativity. Concretely, the 8B model shows modest but consistent creativity gains (8 of 10 benchmarks) with only minor reasoning degradation, whereas the smaller models achieve substantial gains on reasoning tasks. Our study presents a scalable and effective solution to train LLMs for creativity.