Source-linked AI summary
Explanations, Prompts, and Formalizations: Arguments for New Norms in LLM-Enabled Mathematical Research
Axel Boldt
TL;DR
The paper addresses missing transparency and verification practices for mathematical results obtained with LLMs, alongside the difficulty of making such results understandable. It argues for human-written explanations, disclosure of prompts and software setup, and formalizations that support machine checking, while noting that formalization and reproducibility remain imperfect.
Problem
Existing norms for publishing LLM-derived mathematics do not fully require disclosure of precise prompts and software setups, machine-checkable formalizations, or human explanations.
Method
The paper argues for publication practices requiring human explanations, detailed prompt and harness disclosure, and formalization of LLM-obtained mathematical work.
Results
The paper concludes that human authors should explain LLM-derived mathematics, disclose prompts and harnesses, and provide formalizations, with canonization recommended but not required.
Takeaways & Limitations
Detailed disclosure enables repeated experiments and output comparison, while human explanations and formalizations improve understanding and checking of LLM-derived results.
Takeaways & Limitations
Formalization cannot guarantee correctness, and specifying the LLM, prompts, and harness does not make outputs fully deterministic or completely reproducible.
Abstract
from arXiv · showhide
As several mathematical conjectures have recently been settled using large language models (LLMs), the mathematical community has formulated norms and recommendations regarding the publishing of such results. These norms do not cover the disclosure of the prompts and precise software setup used to obtain those results, nor do they require that results be formalized in a manner that allows for machine verification. I argue that both of these are essential. In addition, since LLM-obtained results may be hard to understand, human authors have the responsibility to invent intuitive explanations.
1. Recent LLM-supported developments in mathematics
LLMs have recently been used to settle mathematical conjectures, including major problems, but these results have varied in transparency, explanation, and formal verification. Formalization enables automatic checking, although it remains laborious and nontrivial.
- Formal computer languages allow mathematical proofs to be checked automatically and support machine-assisted construction of new proofs.
- In late 2025, LLMs became capable of proving or disproving conjectures by searching prior work and constructing mathematical arguments, sometimes incorrectly.
- The First Proof project collected autonomous LLM solutions to expert-solved research questions, and many initial solutions were unsatisfying or defective.
- In May 2026, an LLM disproved Erdős’s unit-distance conjecture by constructing a counterexample based on an algebraic-number-theory construction.
- In July 2026, an LLM proved the cycle double cover conjecture, with the exact prompt and a Lean formalization of the prior work and proof released.
- Later in July 2026, an LLM disproved the Jacobian conjecture, but the short counterexample was initially published without elaboration.
2. Reactions and evolving norms
The mathematical community has responded to LLM-generated results by formulating publication norms centered on disclosure, prior-work checking, and formalization. However, raw formalizations often are not prepared for reuse in mathlib, leaving canonization largely to humans.
- Mathematical research communities formulated responses because LLMs increasingly perform activities traditionally central to research mathematics.
- The Leiden Declaration recommends disclosing LLM use, checking references to prior work, and providing formalizations when feasible and appropriate.
- LLM-produced formalizations often cannot be incorporated directly into mathlib because they do not follow conventions designed to facilitate reuse.
- Canonization is the process of turning raw formalizations into useful additions to mathlib, and humans currently perform almost all of it.
3. Demand on authors: explanations
The paper argues that LLM-obtained mathematical results should include human-written explanations. Human authors must correct LLMs’ uneven treatment of routine and innovative reasoning and add significance, connections, and future directions.
- LLM-obtained mathematical results should be accompanied by human-written explanations to facilitate and enlarge mathematical understanding.
- LLMs may omit relevant prior work and explain routine derivations extensively while glossing over innovative steps.
- Human mathematicians should rebalance explanations pedagogically by summarizing lengthy calculations, giving conceptual accounts, or adding suggestive figures.
- Because LLM-produced proofs often contain subtle mistakes, human authors must understand the arguments and accept responsibility for published correctness.
- Human experts can explain significance, connect results to other developments, and suggest future research directions, so reporters should provide these elements.
4. Demand on authors: formalizations
The paper argues that mathematicians reporting LLM-obtained work should provide formalizations so definitions, theorems, and proofs can be checked automatically. Formalization improves checkability but does not guarantee correctness, while canonization is desirable but not demanded because it requires specialized knowledge.
- LLM-supplied proofs can be subtly wrong, making formalization a responsibility for mathematicians reporting LLM-obtained work.
- Formalizations enable automatic checking of definitions, theorems, and proofs, but they may contain subtle errors or fail to match the informal presentation precisely.
- Formalized proofs are easier to check and more likely to be correct than complicated, lengthy, and novel informal arguments, despite lacking absolute certainty.
- Canonized formalizations following mathlib conventions could be incorporated more easily and accelerate the library’s growth.
- The paper does not demand canonization because producing it requires specialized knowledge.
5. Demand on authors: prompts and harnesses
Authors should disclose the precise LLM version, prompts, and harness used for LLM-produced mathematics, both to prevent prompting from becoming secret knowledge and to enable meaningful repetition despite nondeterminism.
- Disclosure requirements: Reports should specify the precise LLM version, prompts, and harness used to produce mathematical results.Several reports omit these details, including by referring only to an “internal model.”
- Transparency: Publishing prompts helps prevent the art of prompting from becoming secret knowledge and lets others learn how mathematics was discovered.The paper argues that transparency should cover discovery methods as well as mathematical explanations.
- Transparency: The cycle double cover proof illustrates the value of publishing a complete prompt, including parallel independent approaches and adversarial cross-checking.The LLM version was nevertheless not revealed.
- Reproducibility: Even with full setup details, LLM outputs remain nondeterministic, so repetition and output comparison are more realistic goals than complete reproducibility.The paper compares this situation with chemical experiments, where chance remains despite detailed setup reporting.
6. Objections and rationale
The paper defends stronger disclosure and review demands for LLM-produced mathematics as protection against low-quality automated work and as part of maximizing human understanding.
- Objections: Authors of LLM-produced work may regard these requirements as unfair because comparable demands are not normally imposed on other mathematicians.The paper responds that LLM-produced work warrants a higher burden of proof.
- Rationale: A higher burden of proof is presented as a defense of refereeing and publishing against quickly produced, automatically generated work of low quality.The rationale is also tied to the goal of maximizing all aspects of human understanding.