We study mathematical discovery through the lens of neurosymbolic reasoning, where an AI agent powered by a large language model (LLM), coupled with symbolic computation tools, and human strategic direction, jointly produced a new result in combinatorial design theory. The main result of this human-AI collaboration is a tight lower bound on the imbalance of Latin squares for the notoriously difficult case n≡1(mod3). We reconstruct the discovery process from detailed interaction logs spanning multiple sessions over several days and identify the distinct cognitive contributions of each component. The AI agent proved effective at uncovering hidden structure and generating hypotheses. The symbolic component consists of computer algebra, constraint solvers, and simulated annealing, which provides rigorous verification and exhaustive enumeration. Human steering supplied the critical research pivot that transformed a dead end into a productive inquiry. Our analysis reveals that multi-model deliberation among frontier LLMs proved reliable for criticism and error detection but unreliable for constructive claims. The resulting human-AI mathematical contribution, a tight lower bound of 4n(n−1)/9, is achieved via a novel class of near-perfect permutations. The bound was formally verified in Lean 4. Our experiments show that neurosymbolic systems can indeed produce genuine discoveries in pure mathematics.
Figures & tables
Figure 1: Collaboration architecture and data flow. Rounded boxes represent actors (human, agent, symbolic tools); italic labels on arrows show the data exchanged. Solid arrows indicate instructions or programs. Dashed arrows indicate results or feedback. The AI agent manages all interactions between different components. It dispatches proofs to multiple frontier LLMs for critical reviews (left). Meanwhile, it maintains a three-component persistent memory system (right), consisting of a project state file, a searchable knowledge base, and a session handover protocol.
n
I∗
Time (s)
n
I∗
Time (s)
n
I∗
Time (s)
n
I∗
Time (s)
4
16/3
<1
19
152
1
34
1496/3
5
49
3136/3
54
7
56/3
<1
22
616/3
2
37
592
5
52
3536/3
32
10
40
<1
25
800/3
2
40
2080/3
74
13
208/3
<1
28
336
2
43
2408/3
139
16
320/3
1
31
1240/3
4
46
920
31
Table 1: Near-PP existence for n≡1(mod3) , 4≤n≤52 . Each achieves the optimal imbalance I∗=4n(n−1)/9 . Times are in seconds obtained on the machine equipped with CPU i7-1260P and 32 GB RAM under the operating system Ubuntu 24.04.3 LTS.
Phase / Step
Function
Role
Enumerate PPs ( n≤17 )
Exhaustive search
S
Algebraic analysis
Pattern search (negative)
S
Confirm dead end
Rigorous verification
S
Change research question
Strategic reframing
H
Compute naive bound
Numerical reasoning
A
Notice f(δ) always even
Uncovering hidden structure
A
Table 2: Contributions by component across discovery phases. A = agent, S = symbolic (solvers, CAS), H = human.
Can artificial intelligence truly contribute to creative mathematical research, or does it merely automate routine calculations while introducing risks of error? We provide empirical evidence through a detailed case study: the discovery of novel error representations and bounds for Hermite quadrature rules via systematic human-AI collaboration. Working with multiple AI assistants, we extended results beyond what manual work achieved, formulating and proving several theorems with AI assistance. The collaboration revealed both remarkable capabilities and critical limitations. AI excelled at algebraic manipulation, systematic proof exploration, literature synthesis, and LaTeX preparation. However, every step required rigorous human verification, mathematical intuition for problem formulation, and strategic direction. We document the complete research workflow with unusual transparency, revealing patterns in successful human-AI mathematical collaboration and identifying failure modes researchers must anticipate. Our experience suggests that, when used with appropriate skepticism and verification protocols, AI tools can meaningfully accelerate mathematical discovery while demanding careful human oversight and deep domain expertise.
Tan Bui-Thanh
Department of Aerospace Engineering & Engineering Mechanics, and Oden Institute for Computational Engineering & Sciences, University of Texas at Austin, Austin, TX, 78712, USA
We introduce the AI co-mathematician, a workbench for mathematicians to interactively leverage AI agents to pursue open-ended research. The AI co-mathematician is optimized to provide holistic support for the exploratory and iterative reality of mathematical workflows, including ideation, literature search, computational exploration, theorem proving and theory building. By providing an asynchronous, stateful workspace that manages uncertainty, refines user intent, tracks failed hypotheses, and outputs native mathematical artifacts, the system mirrors human collaborative workflows. In early tests, the AI co-mathematician helped researchers solve open problems, identify new research directions, and uncover overlooked literature references. Besides demonstrating a highly interactive paradigm for AI-assisted mathematical discovery, the AI co-mathematician also achieves state of the art results on hard problem-solving benchmarks, including scoring 48% on FrontierMath Tier 4, a new high score among all AI systems evaluated.
AI systems are increasingly capable of contributing to mathematical research. In research practice, frontier-model reasoning is a limited resource, and expert mathematical review is even more sharply constrained. Allocating these scarce resources well is therefore central to making AI-assisted mathematical discovery efficient. In most current AI-for-math workflows, human effort is concentrated at the beginning and end, in selecting suitable research problems and later reviewing the resulting artifacts. These two stages are becoming bottlenecks for research-level mathematics. We address them by proposing a new human-AI discovery paradigm. The human input is no longer a single problem selected in advance, but a research direction in which the experts have interest and expertise. The system then searches a broad literature corpus for candidate problems in that direction. Inspired by search and recommender systems, we build Find, Attempt, and Recommend (FAR), a literature-to-review cascade that automates the search for suitable problems and focuses human attention on artifacts that have passed several stages of filtering. In a combinatorics pilot, the pipeline starts from 5,245 combinatorics papers, recovers 6,453 candidate conjectures or open problems, and filters them to 4,717 apparently well-posed and still-open conjectures. Subsequent reasoning and automated triage stages surface 598 potential resolutions and select 77 items for author-team review. Among them, we identify many interesting discoveries, including results on conjectures and questions of Davies--Jenssen--Perkins--Roberts, Erdős--Straus, Ikenmeyer--Pak--Panova, and Lund--Saraf--Wolf. These results demonstrate the effectiveness of this new mode of human-AI collaboration for mathematical discovery.