AI for Scientific Discovery

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.

Spectral co-clustering is a useful tool for discovering latent structure in word-document matrices, but its reliance on singular value decomposition (SVD) can make standard formulations expensive on high-dimensional data. This paper presents two randomized approximations for normalized spectral co-clustering of bipartite text data when the numbers of document and word clusters may differ. The first method uses randomized SVD through random projection, while the second combines partial SVD with element-wise random sampling. Across real-world and synthetic datasets, both methods reduce runtime relative to the full-SVD baseline, but their behavior depends on matrix sparsity. The random projection method is the more reliable approximation across the tested settings, whereas the sampling-based method is most useful on denser matrices and provides limited benefit on already sparse text data. These results show that randomized approximations for spectral co-clustering should be selected according to the underlying structure of the data.

Crop modelling is essential for agricultural water management but often relies on simplified water balance routines that limit representation of soil moisture dynamics. To address this limitation, we developed a coupled model that integrates the 1‐D Richards equation, solved using a finite difference method into the FAO AquaCrop. The coupled model was calibrated and validated using soil moisture, canopy cover, above‐ground biomass and seed cotton yield data from field experiments in the southeastern United States. Compared with hourly field measurements of soil moisture, AquaCrop-Richards achieved an average root mean square error (RMSE) of 0.023 m³ m⁻³ across three soil depths over the growing season. Model performance for canopy cover, biomass and yield resulted in RMSE values of 12.18%, 1.77 t ha⁻¹ and 0.96 t ha⁻¹, respectively, against observations. Under fully irrigated conditions, both models produced statistically indistinguishable yield estimates. However, under rainfed conditions, AquaCrop simulated 15.5% higher yields than AquaCrop-Richards. Analysis showed that AquaCrop produced rapid stepwise drainage, resulting in root‐zone water content 33%-37% lower than the coupled model. This reduced soil moisture triggered earlier water stress which led to yield overestimation. These results indicate that AquaCrop‐Richards improves soil moisture representation and is robust under water‐limited conditions.

Cotton is a one of the major crops in the southeastern United States. It significantly impacts regional water resources since it consumes a large amount of freshwater for irrigation. Current irrigation practices fail to optimize water use accurately since they are largely dependent on soil moisture sensors and grower experience. They do not consider dynamic factors such as soil texture, prevailing weather conditions, and the crop's phenological stage. In this paper we propose an innovative approach to enhance the irrigation efficiency through the use of Deep Reinforcement Learning (DRL) model. It takes into consideration the dynamic variables and optimizes irrigation. We utilize a crop growth simulation model as a learning environment to devise an optimal irrigation strategy. By continuously learning from crop feedback and environmental inputs, the DRL system dynamically modifies irrigation amount to optimize production while consuming the least amount of water. Our approach presents a viable alternative for sustainable irrigation decisions in water-intensive crops, since preliminary findings indicate that it can greatly conserve water without sacrificing crop health or productivity. The goal of this research is to aid in the advancement of precision irrigation technologies that guarantee cotton production's sustainability and resource efficiency. 

In developing Version 2.0 of our Flood Image Classifier, we underscore the significant role of Convolutional Neural Networks (CNNs), mainly Faster R-CNN and YOLOv3, in detecting and segmenting flood-related labels in images. Additionally, our research delves into the potential of Vision Transformers (ViT) for advanced object detection and image classification for flood-related images extracted for the USGS river cameras. Transformer methods offer improved predictions of flood depth and inundation areas, marking a substantial step forward in flood vision technology. The integration of advanced image processing techniques, the enhancement of CNN capabilities, and the incorporation of cutting-edge detection and classification models are pivotal in developing a comprehensive, real-time flood monitoring system. This system is designed to equip frontline decision-makers and emergency responders with essential insights into flooding conditions, thereby significantly contributing to disaster management and response through the innovative use of our flood image classifier, Version 2.0.