We introduce a code-based challenge for automated, open-ended mathematical discovery based on the k-server conjecture, a central open problem in competitive analysis. The task is to discover a potential function satisfying a large graph-structured system of simple linear inequalities. The resulting evaluation procedure is sound but incomplete: any violated inequality definitively refutes a candidate, whereas satisfying all inequalities does not by itself constitute a proof of the corresponding conjecture's special case. Nevertheless, a candidate that passes all constraints would be strong evidence toward a valid proof and, to the best of our knowledge, no currently known potential achieves this under our formulation in the open k=4 circle case. As such, a successful candidate would already be an interesting contribution to the k-server conjecture, and could become a substantial theoretical result when paired with a full proof. Experiments on the resolved k=3 regime show that current agentic methods can solve nontrivial instances, and in the open k=4 regime they reduce the number of violations relative to existing potentials without fully resolving the task. Taken together, these results suggest that the task is challenging but plausibly within reach of current methods. Beyond its relevance to the k-server community, where the developed tooling enables researchers to test new hypotheses and potentially improve on the current record, the task also serves as a useful benchmark for developing code-based discovery agents. In particular, our k=3 results show that it mitigates important limitations of existing open-ended code-based benchmarks, including early saturation and the weak separation between naive random baselines and more sophisticated methods.
Figures & tables
k
m
k -taxi
edges
violations
3
6
no
2′100
0
3
8
no
41′920
0
3
6
yes
193′662
0
3
8
yes
20′068′416
1
4
6
no
6′006
0
4
8
no
261′200
0
Table 1: Summary of the pre-generated circle discretizations. Extended discussion: Appendix B.4 .
Method
Perfect Runs
Max Score
combined
m=6
m=8
combined
m=6
m=8
Best-of-N
0/10
0/10
0/10
0.907{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.064}
0.958{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.027}
0.948{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.039}
Shinka
0/10
4/10
0/10
0.913{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.146}
0.956{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.079}
0.949{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.090}
LoongFlow
2/10
5/10
2/10
0.938{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.084}
0.972{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.038}
0.964{\color[rgb]{0.5117,0.5117,0.5117}\pm 0.052}
Table 2: Perfect runs and final scores summary (higher is better) over 10 independent runs of Best-of- N , Shinka , and LoongFlow all using gpt-oss-120b capped at 100 evaluations, evaluated on two instances ( k=3 ) with m∈6,8 and no k -taxi augmentations. Methods are given with the same initial solutions and task descriptions. “Perfect Runs” reports the fraction of runs achieving perfect score for each corresponding metric. “Final Score” reports per-run maxima for the combined metric (multiplicative across instances) and each instance, aggregated as mean ± std across runs.
Found by
Violations
Codex (gpt-5.2)
3
Shinka (gpt-oss-120b)
14
Humans [ 12 ]
17
Table 3: Best-found k -competitive potential. Candidates are evaluated on the k -taxi augmented k=4,m=6 circle metric.
Appendix figures & tables2 assets
Supplementary material from the paper’s appendix.
Appendix
Figure 1: 10 independent runs of ShinkaEvolve , Best-of- N , LoongFlow per task design: (i) no search, just suggest a canonical potential, (ii) with search over canonical potentials, (iii) with search without canonical potential hint. All methods had the same starting conditions per task design and had 100 evaluations cap.
Metric
Best-of-N
Shinka
LoongFlow
-search
+search
any
-search
+search
any
-search
+search
any
Perfect
0
1
0
0
6
0
0
4
0
Mean Final
0.953
0.971
0.948
0.916
0.983
0.901
0.962
0.975
0.866
Median Final
0.951
0.960
0.963
0.927
1.000
0.914
0.963
0.970
0.845
Min Final
0.951
0.951
0.897
0.854
0.951
0.800
0.951
0.951
0.779
Max Final
0.957
1.000
0.963
0.954
1.000
0.963
0.963
1.000
0.963
Appendix
Table 4: Support summary for the Figure 1 . “-search” means no search with canonical hint setting, “+search” means with search setting with canonical hint and “any” means with search and without canonical hint setting. The evaluations were done on one k=3,m=6 without k -taxi augmentations instance.
We study autonomous mathematical discovery in the Station, an open-world multi-agent environment in which AI agents from different model families pursue a shared research goal without a central coordinator or scripted pipeline. Agents choose their own research directions, conduct experiments, collaborate and publish papers. These papers accumulate into a shared body of knowledge that later agents can read, cite and extend. We evaluated the Station on 12 mathematical construction problems from the AlphaEvolve study and two additional case studies. Five of the 12 problems yielded results novel relative to the prior literature: a new infinite family of finite field Kakeya sets, new exact 604-point kissing configurations in eleven dimensions, improved bounds for the discretized Kakeya needle and sign uncertainty problems, and a substantially improved lower bound for Erdős's minimum overlap problem. Agents also discovered novel infinite families for Book Ramsey numbers. Their research extended beyond searching for high-scoring constructions: agents developed explanations of their findings and proved theorems outside the assigned tasks. These explanations guided further discoveries and were preserved in the agents' papers, making the underlying insights easier for external researchers to understand and build upon. All presented discoveries are supported by exact constructions or proofs formally verified in Lean. We release the source code, full agent dialogues, papers and verification code, providing a transparent record of how these discoveries emerged.
Stephen Chung, Wenyu Du, William J. Wesley
DualverseAI · University of Cambridge · University of Hong Kong +1
As automated reasoning systems advance rapidly, there is a growing need for research-level formal mathematical problems to accurately evaluate their capabilities. To address this, we present Formal Conjectures, an evolving benchmark of currently 2615 mathematical problem statements formalized in Lean 4. Sourced from areas of active mathematical research, the dataset features 1029 open research conjectures providing a zero-contamination benchmark for mathematical proof discovery, and 836 solved problems for proof autoformalization. Notably, the repository provides a structured interface connecting mathematicians who formalize and clarify problems with the AI systems and humans attempting to solve them. Demonstrating its immediate utility, the benchmark has already been leveraged to make new mathematical discoveries, including the resolution of open research conjectures. We describe our approach to ensuring the correctness of these formalizations in a collaborative open-source project where contributions stem from an active community. In this framework, AI-generated proofs and disproofs serve as a valuable auditing mechanism to iteratively improve the fidelity of the benchmark. Finally, we provide a standardized evaluation setup and report baseline results on frozen evaluation subsets, demonstrating a climbable signal that measures the current frontier of automated reasoning on research-level mathematics.
Moritz Firsching, Paul Lezeau, Salvatore Mercuri +8
Google DeepMind · Imperial College London · Stockholms universitet +1
We introduce qtBench, a benchmark of 29 open problems in algebraic combinatorics. These problems ask for a simple combinatorial algorithm that explains given polynomial coefficients or identities. To help AI agents search for such algorithms, we provide a scaffold for playing with combinatorial objects, countering cheating attempts, and testing candidate solutions. To explore how far frontier AI systems can go on these problems, we collaborated with OpenAI, whose researchers obtained proposed solutions to several of them. This highlights bigger meta-problems: is AI discovery at scale ethical? How should these results be released? How should proof digestion be organized? We discuss these questions and give our views.
Eugenio Cainelli, Lorenzo Luccioli, Alessandro Iraci +1