💻 computer science

Mathematical Scientific Discovery Using Large Language Models: A Systematic Literature Review

This systematic literature review, adhering to PRISMA 2020 guidelines, analyzes 32 studies on using large language models for mathematical discovery to identify seven technical paradigms, highlight the superior efficacy of evolutionary search combined with formal verification, and provide a taxonomy to guide future research in the field.

Original authors: Vinita Gangaram Jansari, Carlos Toxtli Hernandez, Michael Burr, Austin LaHue, Ben Nye, Luis David Garcia Puente

Published 2026-08-03

📖 4 min read☕ Coffee break read

CC BY 4.0

Original authors: Vinita Gangaram Jansari, Carlos Toxtli Hernandez, Michael Burr, Austin LaHue, Ben Nye, Luis David Garcia Puente

Original paper licensed under CC BY 4.0 (https://creativecommons.org/licenses/by/4.0/). ✨ This is an AI-generated explanation of the paper below. It is not written or endorsed by the authors. For technical accuracy, refer to the original paper. Read full disclaimer

Imagine a world where math isn't just about solving puzzles someone else wrote down, but about inventing the puzzles themselves. For centuries, the most exciting part of mathematics—the "Eureka!" moment of discovering a brand-new truth, a strange new pattern, or a rule that no one has ever seen before—was thought to be a superpower unique to humans. It required a special kind of intuition, a spark of creativity that computers just couldn't have. But recently, a new kind of artificial intelligence called a "Large Language Model" (or LLM) has started to change the game. Think of an LLM not as a calculator, but as a super-reading machine that has swallowed almost every math book, code manual, and scientific paper ever written. It doesn't just memorize them; it learns the "grammar" of math and code so well that it can start writing its own sentences. The big question researchers are asking is: Can this machine-reading super-brain do more than just answer questions? Can it actually discover new math that humans haven't found yet?

This is exactly what a team of researchers from Clemson University and Colorado College set out to investigate in a massive new study. They didn't just look at one cool experiment; they went on a digital treasure hunt, sifting through hundreds of research papers published up to the end of 2025 to find the ones where AI was actually creating new mathematical knowledge. They used a strict, scientific checklist (called PRISMA) to make sure they didn't miss anything important and to filter out studies that were just about solving old problems. After the dust settled, they found 32 studies that showed something truly remarkable: AI is starting to become a partner in mathematical discovery, not just a calculator.

The researchers found that the most successful AI "mathematicians" aren't just guessing randomly. Instead, they use a few clever tricks. One of the most powerful methods is like a digital version of evolution. Imagine a computer creating thousands of tiny, simple math programs. It tests them, keeps the ones that work best, and then uses the AI to "mutate" them—making small, creative changes to see if they get even better. Over time, this process evolves solutions that are so good they beat records humans have held for decades. For example, the study highlights how these systems recently found a faster way to multiply matrices (a specific type of math grid) that improved upon a famous algorithm from 1969, something no human had managed to do in over 50 years.

Another popular method is like a video game where the AI plays against itself. One part of the AI tries to create a difficult math problem (a "conjecture"), and another part tries to solve it. As the solver gets better, the problem-maker has to get smarter, creating a loop where they both level up together. This has helped AI generate thousands of new, verified math theorems and lemmas (small stepping-stone proofs) that are now being added to digital libraries. However, the paper is very clear that these AI systems aren't magic wands yet. They are still very hungry for computer power, often needing millions of tries to find one good answer. Also, while they are great at finding patterns, they sometimes produce answers that are technically correct but boring or useless to human mathematicians.

The study also points out that for these discoveries to be trusted, they need a "referee." In the world of math, you can't just say "I think this is true." You have to prove it. The most popular referee in these AI experiments is a tool called "Lean," a digital proof-checker that acts like a strict grammar police for math. If the AI says it found a new theorem, Lean checks every single step to make sure it's 100% logical. The researchers found that the most successful projects were the ones where the AI and the referee worked together in a tight loop, with the referee giving immediate feedback to the AI so it could fix its mistakes on the fly.

So, what's the bottom line? The paper suggests that we are standing on the edge of a new era. AI isn't replacing mathematicians, but it is becoming a powerful "idea sandbox." It can churn out millions of possibilities, spot patterns in massive amounts of data that humans would miss, and even solve problems that have been stuck for half a century. But the final step—turning a machine-generated code snippet into a beautiful, understandable mathematical insight—still needs a human touch. The future looks like a team sport: the AI does the heavy lifting of searching and testing, and the human mathematician provides the intuition to decide what's actually interesting. It's a partnership where the machine brings the speed and the scale, and the human brings the soul.

Technical Summary: Mathematical Scientific Discovery Using Large Language Models

1. Problem Definition

The paper addresses the automation of mathematical discovery, a domain distinct from traditional automated theorem proving (ATP). While ATP focuses on verifying or proving existing statements, mathematical discovery involves the generation of new mathematical knowledge, including conjectures, theorems, lemmas, counterexamples, algorithms, and constructions. Historically, this creative aspect of mathematics has been viewed as uniquely human, requiring intuition and deep domain expertise. The paper investigates how Large Language Models (LLMs), trained on large-scale mathematical corpora, can be leveraged to autonomously generate novel mathematical objects and advance mathematical research, moving beyond mere problem-solving to knowledge creation.

2. Methodology

The authors conducted a Systematic Literature Review (SLR) following the PRISMA 2020 guidelines.

Search Strategy: The search covered publications from major academic databases (Semantic Scholar, arXiv, OpenReview, JMLR, Nature, ACL Anthology) up to December 31, 2025. Keywords included combinations of "large language model" with "theorem generation," "conjecture," "mathematical discovery," and related terms.
Selection Criteria:
- Inclusion: Studies must address mathematical discovery (I1), employ LLMs/neural architectures as a core component (I2), demonstrate the generation of new knowledge rather than just solving existing problems (I3), focus on mathematical domains (I4), and be peer-reviewed or preprints (I5).
- Exclusion: Studies focusing solely on problem solving (E1), non-mathematical domains (E2), purely symbolic/non-LLM methods (E3), duplicates (E4), non-English texts (E5), or lacking methodological detail (E6).
Data Extraction: From an initial pool of 63 records, 32 studies met the inclusion criteria after rigorous screening. Data extracted included technical architectures, formal verification systems, datasets, evaluation metrics, and specific mathematical discoveries.
Analysis Framework: The authors synthesized findings into a technical taxonomy of seven distinct paradigms and analyzed trends in verification systems, datasets, and mathematical domains.

3. Key Contributions

The paper makes five principal contributions:

Comprehensive Review: A rigorous PRISMA-compliant review of 32 studies published through 2025, consolidating a rapidly evolving field.
Technical Taxonomy: The identification and detailed analysis of seven distinct technical paradigms for LLM-based mathematical discovery:
- Evolutionary Search Methods
- Reinforcement Learning (RL) and Guided Search
- Self-Play and Expert Iteration
- Neuro-Symbolic Hybrid Systems
- In-Context Learning Pipelines
- Specialized Pretraining Objectives
- Equation Discovery Techniques
Synthesis of Infrastructure: A comprehensive overview of the formal verification systems (Lean, Isabelle, Metamath, PVS), datasets (Mathlib, LeanWorkbook, miniF2F), and evaluation benchmarks used in the field.
Actionable Guidance: Practical recommendations for practitioners regarding architecture selection, verification strategies, training data generation, and sample efficiency.
Identification of Challenges: A clear delineation of open challenges, including computational overhead, domain specificity, verification bottlenecks, and the difficulty of evaluating "interestingness."

4. Key Results and Findings

4.1 Technical Paradigms

Evolutionary Search: Identified as the most successful paradigm for significant discoveries. Systems like FunSearch and AlphaEvolve use LLMs as mutation/crossover operators within a program search space. They have achieved breakthroughs such as improving Strassen's matrix multiplication algorithm (reducing scalar multiplications for 4x4 complex matrices from 49 to 48) and establishing new lower bounds for the cap set problem and kissing number problem.
Reinforcement Learning: Framing discovery as sequential decision-making (e.g., AlphaTensor treating tensor decomposition as a game) has yielded hardware-specific optimizations and counterexamples to long-standing conjectures.
Self-Play and Expert Iteration: Frameworks like STP and LEGO-Prover utilize a dual-role loop where a model acts as both conjecturer and prover. This approach effectively addresses data scarcity by generating its own training curriculum, significantly improving success rates on benchmarks like LeanWorkbook and miniF2F.
Neuro-Symbolic Hybrids: Systems like Lemmanaid combine LLM generation with symbolic instantiation and verification (e.g., in Isabelle). This approach balances neural creativity with logical rigor, filtering out invalid conjectures.
In-Context Learning: Approaches like LeanConjecturer and the Conjecturing-Proving Loop leverage real-time context accumulation from formal repositories (e.g., Mathlib) to guide generation without modifying model weights, enabling the rediscovery of research-level results.
Specialized Pretraining: Methods like Skip-Tree Training shift from next-token prediction to structural prediction (e.g., predicting missing subtrees in Abstract Syntax Trees), improving performance on formal reasoning tasks.
Equation Discovery: Benchmarks like LLM-SRBench highlight the difficulty of true equation discovery, with top methods achieving only ~31.5% accuracy, indicating a need for better evaluation to prevent memorization.

4.2 Formal Verification and Datasets

Lean (specifically Lean 4) is the dominant verification system, used in 28.1% of the reviewed studies, largely due to its extensive Mathlib library and active community.
Datasets: The field relies on a mix of human-curated formal libraries (Mathlib, AFP) and synthetic data generation via self-play (e.g., LeanNavigator generating 4.7 million theorems).
Benchmarks: Standard benchmarks include miniF2F (488 problems), LeanWorkbook, and specialized benchmarks for equation discovery and combinatorial identities.

4.3 Mathematical Domains

The literature is heavily concentrated in Combinatorics and Graph Theory (12 studies), followed by Algebra and Number Theory (8 studies). Significant breakthroughs include:

Matrix Multiplication: Improvements to Strassen's algorithm.
Extremal Combinatorics: New constructions for cap sets and kissing numbers.
Topology: New connections between algebraic and geometric structures in knot theory.
Constants: New continued fraction representations for $\pi$ and $e$ (Ramanujan Machine).
Olympiad Geometry: Generation of competition-level geometry problems.

4.4 Success Factors and Limitations

Success Factors: The most impactful systems integrate formal verification in-the-loop (not just post-hoc), utilize iterative solution accumulation (self-evolution), and exploit deep domain-specific structures (e.g., tensor decompositions).
Limitations:
- Computational Cost: High-fidelity discovery requires millions of evaluations or billions of tokens.
- Domain Specificity: Current systems are often siloed and difficult to transfer across domains.
- Verification Bottleneck: Formal proof assistants are slower than neural generators, creating a bottleneck.
- Quality vs. Quantity: Systems produce vast amounts of trivial or tautological outputs; distinguishing "interesting" insights remains a challenge.
- Interpretability: Machine-generated proofs are often dense and unreadable to humans.

5. Significance and Claims

The paper claims that the field has moved from theoretical possibility to practical research, with AI systems independently contributing to mathematical knowledge.

Impact: The review highlights that AI has already surpassed human records in specific areas (e.g., matrix multiplication, combinatorial bounds) that had remained unchanged for decades.
Collaboration: The authors posit a future of "epistemic complementarity," where AI handles pattern recognition and counterexample generation across massive dimensions, while human mathematicians synthesize these findings into theoretical frameworks.
Democratization: Open-source implementations (e.g., ShinkaEvolve, CoEvo) are lowering barriers to entry, allowing mathematicians to use discovery engines as "ideation sandboxes."
Future Outlook: While current systems are limited by computational costs and narrow specialization, the integration of reasoning models, multi-modal capabilities, and more efficient evolutionary algorithms represents the next frontier. The ultimate goal remains the creation of AI systems capable of independently advancing mathematical knowledge, a challenge the paper views as increasingly within reach but not yet fully realized.

The paper concludes that while significant progress has been made, the field must address the "generality gap," the "creative ceiling" (transformative conceptual leaps), and the "objective metric for interestingness" to fully realize the potential of LLMs in mathematical discovery.