AIMing: Interactive Conjecture Proving

Proof-generating systems return many candidates for the same theorem. Lean's kernel determines whether each candidate is correct, but not whether the candidates contain different mathematical reasoning. We study one measurable component of mathematical creativity: whether repeated successful generations explore distinct proof ideas rather than new formal expressions of the same idea. We analyze LeanRoute-216, which began with 36 kernel-verified and human-reviewed Lean proofs for 36 fixed propositions. Five additional proofs were then generated for each proposition with the goal of obtaining diverse proofs, producing 216 kernel-verified proofs in total. A graph-derived route-level review identified 61 diverse routes among the 216 distinct proof strings. This observation motivated a closer study of the distinction between formal variation and mathematical route diversity. Across the benchmark's 180 parent-candidate pairs, 25 were labeled as route changes and 155 as same-route comparisons. All pairs of candidate proofs were human-evaluated in a blinded second pass, with 95.6% agreement with the original route-change labels (κ = 0.793). Five theorem panels were used to refine the rubric and judging prompts, while the remaining 31 panels were held out for evaluation. On these 31 panels, LLM judges recognize route changes more reliably than lexical baselines, but remain substantially weaker at identifying the kind of change. These results support route diversity as an evaluation target separate from correctness and show how route-level auditing can inform proof search and the curation of synthetic reasoning data.

As AI use progresses in research-level mathematics, automated information retrieval systems for constructing relevant prompts are increasingly important. Existing benchmarks and datasets for identifying which prior results are necessary to prove a statement do not align well with current workflows in which a natural language proof is in progress, but it is unclear what the next step(s) should be. We introduce NaturalPRISM, a benchmark task and dataset containing 1.7 million pairs of intermediate proof states and the premise invoked in the next step of the proof. All pairs are extracted from natural language research-level mathematics papers published on arXiv, and span all 32 subject categories. We evaluate the effect of fine-tuning retrieval models for domain-specific vs. domain-agnostic use cases, and find that the combination of sufficient training data with alignment between the training and testing distributions allows smaller specialized models to dramatically outperform larger general models.

Generating mathematical conjectures from natural-language context is challenging because theorem-relevant information is distributed across multiple forms of mathematical context, including definitions, objects, assumptions, and constructions. We study which of these contextual signals help a model recover the specific claim supported by the surrounding setup, using 61 main theorems from 12 papers across four mathematical domains. For each theorem, we redact the result and represent the remaining setup using six context components. A paired ablation design compares full context, six leave-one-out conditions, and six single-component conditions, yielding 793 generated conjectures. Context components were largely complementary: removing one component usually had little effect, whereas retaining only one substantially reduced expected-theorem alignment. Local Mathematical Objects provided the strongest standalone signal, while Structural Constraints and Conditions produced the largest alignment decrease when removed. These findings suggest that target-aligned conjecture generation depends on combining information that identifies relevant objects with information that constrains admissible claims.

Mathematical reasoning systems should be consistent when the same concept is expressed in equivalent forms. This requires not only recognizing shared mathematical meaning but also identifying the representation changes and reconstructing a traceable route between forms. We study this problem through mathematical theorems, whose equivalent formulations preserve the same underlying result while differing substantially in representation. In this setting, theorem recognition is only the first step: a robust system must also identify the intervening transformations and recover their order. We introduce an evaluation of robust procedural mathematical reasoning with three components: theorem identification, transformation identification, and ordered reconstruction. Using validated theorem-representation pairs from an existing corpus, we build a procedural-robustness dataset with typed operations, reference procedures, and matched contrasts that distinguish valid reformulations from invalid ones. We first measure closed-book performance of four open-weight models to establish a baseline, then evaluate retrieval-augmented generation (RAG) as support mechanism for the same task. Models identify theorem identity more reliably than they recover the transformations and ordered routes connecting equivalent representations. RAG improves every stage, but procedural reconstruction remains the main bottleneck. The framework supports more consistent and traceable mathematical systems, with potential applications in mathematical search, tutoring, autoformalization, and scientific discovery.

Large language models (LLMs) are increasingly integrated into complex workflows as automated evaluators, yet their reliability in assessing unconventional reasoning processes remains under-explored. Current evaluation frameworks often overlook models' robustness to procedural equivalence, the ability to recognize valid but non-canonical paths to a correct result. In this work, we introduce a benchmark specifically designed to test LLMs in an evaluative capacity, using linear-equation problems with diverse solution variants as a controlled proxy for correctness-critical, multi-step verification tasks in science and engineering. We further define a process-centric evaluation framework across three dimensions: (i) final-answer correctness, (ii) step-level correctness, and (iii) localization of the initial logical error. Our evaluation of state-of-the-art open LLMs reveals a significant robustness gap: models that accurately evaluate canonical solutions often fail when presented with perturbed but logically equivalent variants. Models exhibit high false-negative rates by rejecting valid alternative solutions and show signs of bias. Our results suggest that while adaptation strategies can narrow this gap, achieving reliable process-level verification remains a critical challenge for deploying LLM evaluators in correctness-critical domains.

AI systems increasingly operate between flexible input representations and formal objects used by downstream tools. A key challenge is recognizing when an unfamiliar formulation denotes a known formal object. We study this challenge through theorem recognition: given an equivalence-preserving transformation of a theorem condition, a model must recover the theorem identity associated with the standard statement. We introduce TREAT, a benchmark designed to isolate this representation-dependent access problem. Rather than paraphrasing theorem text, TREAT changes the mathematical form of theorem conditions themselves, expressing known results through residual equations, witness statements, optimization identities, set relations, operator forms, and proof-intermediate characterizations. Starting from scraped theorem pages, we filter for entries with usable mathematical expression forms, extract canonical theorem conditions, and generate transformed variants with recorded assumptions and inverse mappings. The final corpus contains 737 theorem identities and 29,900 transformed rows. On a test panel, the best model retrieves the correct theorem identity in only 60.73% of cases. Other systems reveal different failure modes, including abstention, wrong-theorem commitments, and malformed structured outputs. These results suggest that theorem knowledge can be fragile under equivalent changes in representation. TREAT therefore provides a controlled testbed for evaluating representation-robust access to formal knowledge, with broader relevance to domains that require stable target objects, explicit equivalence relations, validation procedures, and auditable scoring.