The following document was written by ChatGPT. The text represents the opinions and arguments of the human author.
October 2026
Artificial intelligence is rapidly reducing the cost of producing plausible new mathematical theorems and proofs. This creates a new decision problem for working mathematicians. If AI can generate many potentially interesting results, how much time should be spent checking them, rewriting them in traditional mathematical style, formalizing them, and preparing them for publication?
The answer depends strongly on which parts of this pipeline are likely to become inexpensive in the near future. Human rewriting of AI-generated proofs may have little lasting value. Formalization may be worth doing selectively. Verification of mathematical correctness remains much more important because subsequent research may depend on the result before future tools become available.
The central strategic issue is therefore not whether AI should be used to generate mathematics. It is how to allocate scarce human attention among exploration, verification, exposition, formalization, and selection. If theorem generation becomes abundant, the scarce resource becomes judgment about which results deserve further investment.
For most of the history of mathematics, producing a new theorem was expensive.
A mathematician might spend weeks or months developing a proof. The cost of discovery itself imposed a strong filter: relatively few results could be generated, and consequently a substantial fraction of them received careful human attention.
Artificial intelligence changes this asymmetry.
A sufficiently capable system can explore many proof strategies, produce variants of a theorem, weaken hypotheses, search for examples, suggest generalizations, and generate long proofs at a speed that no individual mathematician can match.
Recent mathematical AI systems already show substantial progress in natural-language problem solving, formal theorem proving, and research-level reasoning. Systems that only a few years ago required substantial manual formalization have been followed by systems capable of solving difficult problems directly from natural-language statements and producing proofs intended for human readers. [1,2]
The natural continuation of this trend is not merely that AI will prove difficult theorems.
It is that AI may make the production of candidate mathematics extremely cheap.
A mathematician may soon be able to ask for fifty possible extensions of a theorem rather than spend a month finding one.
That creates a problem which mathematics has historically encountered only on a much smaller scale:
What should be done with all these results?
Suppose an AI system produces a theorem together with a long proof.
Several tasks remain.
The proof may have to be checked for correctness.
It may have to be rewritten into conventional mathematical prose.
If formal verification is desired, the proof may have to be translated into Lean or another proof assistant.
Even after Lean verifies the formal theorem, someone must determine whether the formal theorem is actually equivalent to the theorem stated for humans.
Finally, someone must decide whether the result is interesting enough to deserve publication at all.
Historically, these tasks were bundled together because theorem production was slow. A mathematician who spent six months proving something would naturally spend additional time checking and writing it.
That calculus changes if producing another theorem takes minutes.
The scarce quantity then becomes human attention.
The central research decision becomes
Which machine-generated results deserve expensive human investment?
This question may become more important than the question of how to produce another theorem.
At present, three especially important tasks often remain after an AI produces mathematics.
The first is rewriting.
AI-generated proofs may be correct but verbose, poorly organized, redundant, or stylistically unlike conventional mathematical writing. A human can often turn such output into a much shorter and clearer proof.
The second is verification.
A natural-language proof may contain a subtle gap even when every local step sounds plausible. Recent work on mathematical proof evaluation shows significant progress in automated checking, but reliable verification of difficult natural-language mathematics remains unsolved. [3]
The third is semantic verification of formalization.
Lean can establish that a formal statement follows from specified assumptions. It cannot establish that the formal statement is the theorem the mathematician intended.
This gap is substantial. A recent study of natural-language-to-Lean formalization reported a large difference between the fraction of generated Lean statements that compiled and the fraction judged semantically faithful to the corresponding informal theorem. [4]
These three activities differ greatly in their present value.
That distinction matters for how mathematicians should spend their time.
Of the three tasks, rewriting is the easiest to postpone.
Suppose an AI produces a correct but awkward fifty-page proof.
If the theorem is not yet known to be important, there is little reason to spend several days making the proof elegant.
The theorem may later turn out to be false.
It may be subsumed by a stronger result.
It may be technically correct but uninteresting.
A different proof may later reduce fifty pages to five.
Or future AI systems may rewrite it automatically at much higher quality.
For exploratory research, the appropriate standard should therefore be much lower than publication quality.
One should preserve enough information to reconstruct the argument:
But polishing every paragraph is usually wasted effort until the result survives mathematical triage.
This suggests a general rule:
Do not pay publication-level exposition costs before deciding that the result deserves publication.
Traditional mathematical habits encourage the opposite order because mathematicians naturally improve a proof while thinking about it. In an AI-intensive workflow, that instinct may become expensive.
Verification is fundamentally different.
Suppose an AI produces Lemma A.
On the basis of A, another system produces Theorems B, C, D, and E.
If A is false, a large branch of research may be worthless.
Future improvements in automated verification do not recover the human time spent interpreting, developing, or building upon false mathematics.
For this reason, correctness has immediate option value.
A result that will serve as a foundation for additional work should be checked before substantial resources are invested downstream.
But this does not imply that every generated theorem deserves a complete referee-level examination.
Verification should be proportional to the role of the result.
A speculative observation may receive only light checking.
A lemma on which many other arguments depend deserves serious scrutiny.
A major theorem intended for dissemination deserves much more.
The relevant distinction is between
exploratory mathematics
and
load-bearing mathematics.
Human effort should concentrate on the latter.
This becomes especially important if AI systems can generate large research trees. One should not fully verify every leaf. One should verify the trunk.
Formal verification offers an attractive solution to the correctness problem, but at present it imposes costs of its own.
Those costs include formalizing definitions, supplying missing lemmas, adapting arguments to available libraries, and checking that the formal theorem accurately expresses the intended mathematical statement.
The last point is particularly important.
A flawless Lean proof of the wrong theorem is not a certificate of the informal claim.
For this reason, complete formalization is currently most valuable for results that are especially important, delicate, surprising, foundational, or difficult to check informally.
It is less compelling for hundreds of routine intermediate observations that may never appear in a final paper.
This balance may change quickly.
If natural-language-to-Lean translation and semantic checking become highly reliable, then formal verification may become the default rather than the exception.
Until then, formalization is best treated as an expensive certification procedure to be applied where the expected benefit is large.
A mathematician using powerful AI faces a choice analogous to portfolio allocation.
Suppose one has one thousand hours available.
One strategy is to generate ten results and spend one hundred hours polishing, checking, and formalizing each of them.
Another is to generate one hundred results, perform inexpensive triage, investigate perhaps twenty seriously, verify five carefully, and prepare only two for publication.
If theorem generation has become cheap while human attention remains expensive, the second strategy may have much higher expected value.
The point is not that one should publish more papers.
It may imply exactly the opposite.
AI should make it possible to explore much more mathematics privately while publishing only a highly selected fraction.
The optimal workflow may therefore contain a large unpublished layer:
Most of this material need never become a paper.
Its function is to help identify the few results that justify further investment.
There is no reason every correct theorem should receive the same degree of refinement.
A result may deserve several levels of treatment.
The mistake would be to move automatically from Level 1 to Level 6 whenever AI produces something new.
If AI makes theorem generation abundant, most results should stop somewhere in the middle.
The practical principle is:
Do today only the human work whose delay would impose a substantial cost.
This principle treats the three remaining human tasks differently.
Rewriting can often wait.
If the proof is correct and preserved, future systems can likely rewrite it better.
Verification often cannot wait.
If other work depends on the theorem, incorrect mathematics can waste resources immediately.
Formalization lies between the two.
If formal certification materially changes one's confidence in an important result, it is worth doing now. If it merely produces a machine artifact that future systems are likely to generate automatically, postponement may be rational.
This is not an argument for trusting unverified mathematics.
It is an argument for matching verification effort to expected downstream consequences.
Suppose, hypothetically, that within three years AI systems can reliably perform all three tasks:
Would effort spent today on these tasks be wasted?
Sometimes yes.
A mathematician who spends hundreds of hours manually polishing speculative proofs that could simply be stored and rewritten automatically three years later may have made a poor allocation of time.
The same may be true of extensive manual formalization of routine results.
Verification is different because present decisions depend on present correctness.
The right economic comparison is not
Will this task eventually become free?
but
What is the value of having the task completed before it becomes free?
This is a standard investment problem.
If early completion permits valuable research to continue safely, the cost may be justified.
If early completion merely produces a polished artifact sooner, it may not be.
The traditional final product of mathematical research is a paper.
That may not remain the optimal unit.
A future mathematical result could consist of several separate objects:
Different readers may need different parts.
A specialist may want the formal certificate.
A student may want the conceptual explanation.
A researcher deciding whether to build on the theorem may care primarily about precise hypotheses and machine verification.
A historian of the subject may care how the result was discovered.
There is no fundamental reason all of this must be compressed into the conventional journal article.
The pressure to rewrite every proof into traditional style may therefore decline even if human-readable mathematics remains valuable.
If AI can generate ten thousand correct new theorems, the main problem is no longer theorem scarcity.
It is selection.
Which theorem explains something?
Which removes an artificial assumption?
Which introduces the correct definition?
Which connects two previously separate areas?
Which suggests a useful conjecture?
Which changes what mathematicians should think about?
Which deserves to enter the permanent literature?
These questions are much harder to formalize than proof checking.
For the moment they remain strongly associated with mathematical taste.
This does not imply that they are permanently beyond AI. Systems may eventually become excellent at predicting mathematical importance, identifying fruitful abstractions, and selecting promising research directions.
One should therefore be cautious about declaring "taste" to be the permanent human comparative advantage.
Still, during the foreseeable transition, theorem generation is likely to become cheap before high-level selection becomes completely reliable.
That creates an unusual period in which the value of an experienced mathematician may shift away from producing proofs and toward deciding which machine-produced mathematics deserves attention.
There is another reason to perform aggressive triage before publication.
AI makes it possible for authors to generate manuscripts much faster than referees can evaluate them.
If authors submit large numbers of AI-generated papers with only superficial checking, the cost of verification is transferred from the author to the community.
This is an unstable system.
A machine can generate another fifty-page proof at negligible marginal cost. A competent referee may require days to understand it.
The asymmetry implies that ordinary peer review cannot serve as the first serious verification stage for unrestricted AI-generated mathematics.
The author's responsibility should therefore increase rather than decrease.
A submitted paper should come with strong prior evidence that the theorem is correct and worth the referee's attention.
Ideally, future systems will provide machine-verifiable certificates.
Until then, mathematicians should resist the temptation to use referees as debugging tools for cheap machine output.
The most natural strategy for the next few years may be summarized in four words:
Generate more, publish less.
Use AI aggressively for exploration.
Ask for stronger theorems, weaker hypotheses, counterexamples, alternative proofs, higher-dimensional analogues, quantitative versions, and connections with other subjects.
Maintain a large research archive.
But apply increasingly expensive human attention only as a result moves closer to becoming mathematically important.
The funnel might look like
1000 generated ideas ↓ 100 plausible results ↓ 20 interesting results ↓ 5 carefully checked results ↓ 2 formally certified results ↓ 1 polished paper.
The numbers are arbitrary.
The principle is not.
When generation becomes cheap, selectivity should increase.
Artificial intelligence changes the economics of mathematical research before it changes its philosophical foundations.
The important near-term change is that theorem production may cease to be the scarce resource.
Human attention remains scarce.
A mathematician using AI should therefore distinguish sharply among exploration, verification, formalization, exposition, and publication.
Exploration should become broad and cheap.
Verification should concentrate on load-bearing results.
Formalization should be selective until its cost falls further.
Polishing should usually be delayed until mathematical value has been established.
Publication should become more selective, not less.
The strategic objective is not to maximize the number of theorems produced.
It is to maximize the amount of important, trustworthy mathematics obtained per unit of scarce human attention.
If AI eventually automates proof generation, proof checking, formalization, semantic verification, and exposition, the bottleneck will move again.
For now, however, one principle seems robust:
Let machines generate abundance.
Spend human attention only where scarcity remains.