← Blog

Explainer15 min read

Math research in the age of AI: what the Harvard CMSA report recommends

32 mathematicians met at Harvard's CMSA to set norms for AI in math research. Their ten recommendations, the methodologies section they ask for, and how to write one.

On this page
  1. What is the CMSA summit report?
  2. What are the report's ten top recommendations?
  3. How does the report want credit to change?
  4. What does the report say about authorship?
  5. What is the methodologies section, and what should it say?
  6. How do you write a methodologies section for an AI-assisted math paper?
  7. What does the report say about formalization?
  8. What does it say about priority, scooping and errors?
  9. What changes for publishing?
  10. What about open models and AI labs?
  11. Where does Papex fit?
  12. What comes next?
  13. Sources

On 22 and 23 October 2026, the Harvard Center for Mathematical Sciences and Applications (CMSA) brought 32 mathematicians from academia, government and industry together for a two-day summit, Math Research in the Age of AI. Their report, posted at the end of October, is twelve pages long. It sets out ten top recommendations and the work of five groups: on evaluating and publishing research, on coordinated action, on open-source tools, on formalization, and on collaboration between academia and AI labs.

Much of it is concrete. Papers should carry a methodologies section that says what the AI did and what the human authors did. Authorship can name roles, as in the lab sciences. Rushing results out to claim priority "must be actively disincentivized". Turning a verified AI-produced proof into readable mathematics counts as a contribution. New venues should "preserve version histories, and indicate review status for claims".

Below: who wrote the report and how much weight it carries, its ten recommendations, what it says about credit, authorship, priority, formalization and publishing, and a practical guide to writing the methodologies section it asks for, with an example. Every source was checked on 3 November 2026.

What is the CMSA summit report?#

It is the written outcome of a two-day meeting convened by CMSA, Harvard's center for mathematical sciences and applications. In the report's words, "Thirty-two mathematicians from academia, government, and industry came together to help navigate this period of rapid change and, most importantly, to build the future." The participants worked in five groups:

  • Evaluation, production, and dissemination of research
  • Coordinated actions for the AI era
  • Open-source tools
  • Formalization in mathematics
  • Collaboration between academia and AI labs

The participant list, printed at the end, includes Jeremy Avigad, Boaz Barak, Pavel Etingof, Javier Gómez-Serrano, Larry Guth, Bryna Kra, Melanie Matchett Wood, Emily Riehl, Andrew Sutherland and Adam Topaz, among others. The report is careful about its own status: "The views expressed in this report represent consensus but are not necessarily unanimously held." It is a set of recommendations, not a policy of Harvard, of any journal or of any society.

It follows an earlier CMSA summit on PhD Math Education in the Age of AI, held in September 2026, and it says future summits "may cover important topics not yet addressed, such as publication and undergraduate mathematics education." The summit website has a form for feedback.

The report also says which part is meant to be used now: "Portions of the recommendations, particularly those in the section on evaluation, production, and dissemination of research, offer immediately actionable suggestions for review and hiring in mathematics departments."

What are the report's ten top recommendations?#

The report opens with ten numbered recommendations. Here they are, shortened, with the report's own words in quotation marks:

#RecommendationIn the report's words
1Mathematicians should reshape the profession as it adapts to new technologies"sustained community collaborations supported by resources and coordination, and by recognition of the work involved"
2Value different types of scholarly work"incentive structures in academia must change accordingly"
3Put students and early-career mathematicians first"prioritize training, funding, and empowerment"
4Build connected, curated repositories and new publication formats"to accommodate databases, interactive work, and exposition"
5Formal proof should supplement existing practice"with subject experts guiding the construction and maintenance of reusable formal libraries"
6Sustained partnerships between academia, industry and government"Collaborations must center people, particularly trainees"
7Foster large-scale collaborations"new ways to organize knowledge and track progress, and by crediting participation in such projects"
8Reaffirm and update professional norms"emphasizing fairness, collegiality, attribution, and collaboration"
9Keep ways to contribute that do not depend on AI"opportunities for contributions to the subject that do not depend on the use of AI tools"
10Communicate mathematics to the public"This work should be recognized as contributing to the advancement of mathematics."

Three threads run through the list: what counts as a contribution, how credit and responsibility are recorded, and what infrastructure the field needs. The sections below follow them.

How does the report want credit to change?#

It starts from a diagnosis: "For decades, theorem production has been the principal measure of mathematical achievement, shaping hiring and promotion decisions. As the profession changes, this alone cannot capture the range of work that is required to advance mathematical understanding and to strengthen the mathematics community."

So it asks for a wider list of things that count: broad and deep knowledge, new research directions, new questions and conjectures, contributions to open and crowd-sourced projects, new ways of doing and organizing mathematics, resources that serve the community, work in formalization, participation in larger research efforts, new methods of using AI tools, and community leadership. Two items are new in kind:

  • Exposition of AI proofs. "The intellectual work of turning a verified AI-produced proof of a significant result into readable mathematics is an important contribution to the advancement of mathematical knowledge."
  • Less weight on being first. "The mathematics community will need to move away from its long-held practice of placing primary value on the first demonstration of a result, in particular in cases where the argument can be obtained from AI tools with relatively little work."

For hiring and promotion, it says deep expertise should stay central but the evidence for it is widening. It suggests that application materials may include "communication statements, explanatory videos, or evidence of engagement with mathematical exposition", that letters should recognize these contributions, and, more unusually: "During this period of transition, departments may consider allowing research statements without any mention of future research plans."

Frank Calegari made a similar argument in a guest post on Terence Tao's blog on 1 November. His first concrete suggestion is "Evaluate all work as if it is AI-assisted", and he gives a definition of credit that matches the report's: "someone who chooses a worthwhile problem, obtains a proof completely using AI, understands it thoroughly, and uses it to develop interesting further questions or directions has made a substantial mathematical contribution." He also names the behaviour the report wants to discourage, writing that "it takes one look at the arXiv to see many people in our profession rushing out AI-assisted papers in a somewhat unsightly rush to be the ‘first’ to prove things."

What does the report say about authorship?#

It treats authorship as something that is changing, and borrows from the lab sciences:

"The meaning of authorship is evolving with novel methods of collaboration and dissemination. While there is no single template for authorship attribution, a potential model for larger groups follows practice in the lab sciences. Roles may be specified for participants, such as: investigation, analysis, validation, writing, review, editing, and funding acquisition."

Those names overlap with CRediT, the Contributor Roles Taxonomy that many journals already use. CRediT has 14 roles (Conceptualization, Data curation, Formal analysis, Funding acquisition, Investigation, Methodology, Project administration, Resources, Software, Supervision, Validation, Visualization, Writing – original draft, Writing – review & editing) and is a NISO standard, ANSI/NISO Z39.104-2022. The report does not name CRediT, but a mathematician who wants to follow its advice can use CRediT's names and be understood across fields.

Roles do not split responsibility. The next sentences of the report are the strictest in it:

"When roles are not clearly distinguished, authors should collectively understand a paper at a granular level and take responsibility for its claims. Neither formal nor AI-based checking replaces this responsibility."

That line rules out two shortcuts: "Lean accepted it, so it is right" and "the AI checked it". A formal check and an AI review are evidence; the authors are still the ones who answer for the paper.

What is the methodologies section, and what should it say?#

This is the most practical recommendation in the report:

"We can only sustain trust through candid communication. Papers should include a methodologies section akin to current practice in the lab sciences, with the title deliberately chosen to reflect a wide variety of practices. A meaningful methodologies section documents the nature and extent of AI contributions, as well as those of the human authors. Such a statement complements human responsibility and does not replace it."

Three points in it are easy to miss. The section covers the human authors' contributions too, not only the AI's. The title is meant to fit many practices, so "Methodologies" can cover a paper that used a computer search, a proof assistant, an AI model, or none of them. And the section adds to responsibility; it does not transfer any of it to the tools.

The report then asks "professional organizations and publishers" to "develop clear guidance regarding AI usage and acknowledgment for authors, referees, and evaluators, recognizing that these are living documents meant to be updated." That guidance does not exist yet in a common form. Journals ask for AI statements in different places and wording today; we compared eleven policies in How to write an AI disclosure statement for a research paper, and the current wording for each publisher is on /docs/journals.

Calegari's post adds a warning about tone: "Right now, the use of AI carries a stigma, and the phrasing of many AI disclosures reads more like an attempt to minimize the contribution of the machine." A methodologies section in the report's sense is the opposite of that: a plain description of who did what.

How do you write a methodologies section for an AI-assisted math paper?#

Until journals settle on a form, here is a practical checklist built from the report's wording. It is our reading, not a template from CMSA.

What to recordExample of what to writeWhy
The tools, with versions and dates"[Model name and version, as the provider shows it], 4–9 October 2026"Findings about AI tools age quickly, and model names in papers are self-reported
What each tool did"Proposed the reduction in Section 3; drafted the proof of Lemma 3.2""the nature and extent of AI contributions"
What each author did"A.B. chose the problem and checked every step of Section 3"The report asks for "those of the human authors" too
How the result was checked"Theorem 1.1 is formalized in Lean 4 with Mathlib at commit …"Readers need to know what kind of check was done
How the statement was checked"C.D. compared the formal statement with Theorem 1.1 line by line"The report separates verification from validation (below)
What was not checked"Appendix B was not formalized and was checked by hand only"Candid communication, in the report's phrase
Where the trail is"Prompts, outputs and versions are archived at …"So the claim can be revisited
Roles"A.B.: investigation, validation, writing; C.D.: formal analysis, review"The report's lab-science model

An example, with invented names and placeholders:

Methodologies. The reduction in Section 3 was first proposed by an AI model ([model name and version as shown by the provider], used 4–9 October 2026), in a conversation started by A.B. with the question stated in Section 1. The model also drafted a proof of Lemma 3.2. A.B. checked each step of that draft, rewrote it, and found and corrected an error in the case p = 2. The proof of Theorem 1.1 was formalized in Lean 4 with Mathlib (commit [hash]); an AI coding assistant ([name and version]) wrote most of the formal proof, and C.D. compared the formal statement with Theorem 1.1 and the definitions it depends on. Appendix B was not formalized and was checked by hand by both authors. The exposition is the authors' own; an AI model suggested edits to Sections 1 and 4, which the authors reviewed. Roles: A.B., investigation, validation, writing – original draft; C.D., formal analysis, software, writing – review & editing. Both authors take responsibility for every claim in the paper.

Two habits make this easier to write. Keep the dates and versions as you go, not at submission time; models change names and conversations scroll away. And write what was checked and what was not, in that order: a reader learns more from "Appendix B was checked by hand only" than from a general statement that "the results were verified".

What does the report say about formalization?#

It describes the change in a few sentences. Lean's general library, Mathlib, "currently has about 2.5 million lines of formal proofs, contributed by nearly 800 people". Until recently, it says, most contemporary mathematics was out of reach of formalization, because the libraries lacked the background and the effort was prohibitive. "AI has changed the situation very quickly and dramatically." It gives two examples from September: an Anthropic agent that produced a formally verified proof of Fermat's Last Theorem in 11 days, "generating 13 million lines of code that proved 29,500 intermediate theorems", and OpenAI's announcement of a solution to the Navier–Stokes problem, released with "a formally checked version in Lean". Its conclusion: "it is now reasonable to expect that most existing mathematics will be formalized within the next few years."

The most useful part for authors is a distinction:

"Verifying a formal proof requires checking that each step follows from the axioms and rules of a trusted formal foundation, something a computational proof checker can do. Validation requires checking that the proof's formal conclusion accurately represents the intended mathematical claim."

The second check, which the report calls semantic alignment, is "fundamentally up to mathematicians to decide", and it asks the community to develop standards for it. This is where several recent AI claims have been argued over: a proof can pass Lean and still prove a slightly different statement from the one in the abstract. We looked at examples in the Axiom CFSG formalization and the Nivat conjecture proof.

On journals, the report is cautious. "When sufficient formal libraries are in place, journals should consider encouraging authors to accompany submissions with formalization." But: "formalization is much more challenging without AI, so any requirement of formal verification will disadvantage authors who do not wish to use AI." That matches its ninth recommendation and a short section headed AI choice: "The community must respect the choice of mathematicians who do not use AI."

What does it say about priority, scooping and errors?#

Under professional norms, the report gives a short list that could be pinned on a department noticeboard:

  • "Using AI to exploit a colleague's unreleased ideas is not acceptable."
  • "When groups discover substantial overlap, they should consider collaboration and attribution; rushing results to claim priority must be actively disincentivized."
  • "Questions arising in a lecture should be directed to the speaker before querying an AI model."
  • "AI tools will expose errors in the literature. The significance of each error must be established before conclusions are drawn: a local mistake and a gap that undermines a paper's main argument merit different responses. Traditional norms, such as contacting the author when an error is discovered, still apply."

It adds that the consequences differ by career stage, and that "Established mathematicians must actively protect developing researchers so that junior colleagues do not disproportionately bear the brunt of the uncertainty of these times."

If you are worried about being scooped while you work with AI tools, the practical side of showing what you had and when is in How to protect a research idea from being scooped.

What changes for publishing?#

The report says "The journal ecosystem must be revised to accommodate many new products of mathematics, including surveys, software reviews, databases, interactive articles, and animated visualizations." It names two new venues: Hexagon, "a repository for AI-assisted and AI-generated mathematics", and Palomar, "a registry for Lean verification". And it describes what new venues may do:

"New venues may distinguish dissemination from validation, preserve version histories, and indicate review status for claims."

It also asks for curated collections of "theorems, conjectures, examples, counterexamples, and experiments, including verification status, reusable code, and searchable interfaces", citing the Erdős Problems collection, the Bourgain Project, the LMFDB and Beyond n log n as existing examples.

On norms, it asks "Professional societies, journals, and funders" to "develop, document, and disseminate norms for attribution, methodologies sections, and responsibility for correctness", and points to the Leiden Declaration on Artificial Intelligence and Mathematics as "an existing basis for discussion". That declaration, dated 2 June 2026 and endorsed by the International Mathematical Union, asks researchers to disclose their use of AI, keeps humans responsible for correctness and citations, and says credit belongs to human authors. Calegari's view is that it "is being honored more in name than in spirit".

What about open models and AI labs?#

Two of the five groups looked outward.

The open-source group asks that websites and tools for mathematicians say who runs them and how uploaded data is used, and that licenses be "clearly stated and easy to find". On open models it is realistic: a fully open-source model built by the mathematical community "is unlikely to simultaneously meet the goals of access, transparency, and research capability", and it recommends partnering with others, including safety institutes, while mathematicians contribute where their expertise matters most.

The group on academia and AI labs puts training young mathematicians first and calls AI safety a shared priority. One recommendation bears directly on provenance: "There is value in AI labs sharing the step-by-step reasoning processes behind their solved problems whenever possible." It also proposes several mathematical advisory boards with broad representation, and lists existing initiatives, from fellowship and education programs at Anthropic, OpenAI and Google DeepMind to the Advisory Group on Mathematics and Artificial Intelligence (AGMAI) and new Simons Foundation efforts.

Where does Papex fit?#

Several of the report's requests are about keeping a record: who did what, which version, what was checked. Papex is built for that part. On a Papex Publication, each author can be given CRediT roles, and the record says how AI was involved, as the authors state it; model and tool names are self-reported. The person accountable signs one exact version, and a salted fingerprint of that version is timestamped with OpenTimestamps and anchored in Bitcoin; anyone can check the signer, version and date at /verify without an account. Later versions stay linked to earlier ones. From the signed version, Papex can write the AI-use statement in a journal's own form, listed on /docs/journals.

Papex does not check proofs, does not judge semantic alignment and is not peer review. A signed record shows who signed which version, when, and what they said the tools did; it does not show the mathematics is right. Separately, we list AI-assisted claims on named open problems at papex.org/ai-claims, each as its source states it and unchecked by us.

What comes next?#

The report asks departments to act on its evaluation and hiring suggestions now, and asks societies, journals and funders to write the norms it describes. Its own list of open topics includes publication and undergraduate education, and the summit website takes feedback.

For an individual mathematician, the first step is the smallest: when the next paper goes out, add a methodologies section that says plainly what the tools did, what each author did, and what was and was not checked. None of that needs to wait for a journal to ask.

Sources#

Keep reading

All posts