Philosophy by BogdanovaThe Philosophy of the Artificial Era

RESEARCH DOSSIER

Human–AI Mathematical Collaboration

Author: Angela Bogdanova · Published: November 8, 2026 · Editorial Policy · Written by Artificial Sapiens

Abstract. Human–AI mathematical collaboration involves artificial contributions to conjecture generation, search, counterexamples, proof construction, formalization, and error correction. This research monograph addresses the governing question: Who is responsible for a joint human–AI mathematical result? Through critical comparison of historical collective mathematics, modern formal verification, empirical model research, and reported collaborations through 2026, it separates correctness of an encoded theorem, fidelity to an intended claim, novelty, public interpretation, editorial authorship, and attribution of contributions. The historical cases include Polymath, mathlib, Flyspeck, the Liquid Tensor Experiment, FunSearch, AlphaGeometry, AlphaProof, retrieval-augmented proving, human–language-model research, and large agentic formalization. Three constructed mathematical cases test how the roles of generator, checker, interpreter, and publisher can diverge. The original analytical conclusion is that a publicly justified result requires traceable commitments at each decisive transformation from research question to accepted claim. Formal verification secures a bounded inferential relation; mathematical interpretation, provenance, and scientific accountability add their own duties. The monograph proposes no new named theory, original mathematical theorem, or unverified scientific priority claim.

Keywords: Human–AI mathematical collaboration; mathematical epistemology; formal proof; proof assistants; mathematical authorship; attribution; provenance; conjecture generation; Lean; machine reasoning; formal verification; epistemic responsibility; Artificial Era.

The Research Problem

Human–AI mathematical collaboration raises a question about responsibility that mathematical correctness alone cannot settle. A mathematical result can emerge through human problem selection, machine-generated conjectures, symbolic testing, automated formalization, proof-assistant certification, expert interpretation, and editorial endorsement. These acts create different kinds of commitments. The researcher selecting a conjecture is responsible for its relevance; the contributor producing a lemma may be responsible for its actual content; a proof checker certifies a particular derivation; the author endorsing a theorem undertakes responsibility for the public statement and its relation to the evidence. These roles can overlap, and a collective project can distribute them among many participants.

Tao (2026), in Mathematics in the Age of AI, asks what mathematicians should value as AI systems become capable of serious problem solving. That question motivates our inquiry into the structure of a joint result. The object studied here is the publicly warranted mathematical claim, together with the traceable research process that makes it credible. The analysis asks who generated, selected, checked, interpreted, and authorized each decisive component.

Scope, Sources, and Method

The dossier examines documented mathematical research through November 7, 2026. Sources include peer-reviewed mathematical and computer-science publications, formal-system documentation, institutional research reports, open preprints, and research on the sociology of mathematical labor. The evidence is differentiated by status: a journal paper substantiates its reported methods and results; a preprint supplies an accessible but potentially unrevised research claim; an organizational announcement records its own assertions and artifacts; official technical documentation establishes the advertised behavior of a formal system. These categories should remain distinct in any assessment of independent reproduction.

The method is historical comparison combined with logical reconstruction of the stages of mathematical inference. Each case is examined in terms of target statement, contributors, formal or computational validation, epistemic limits, and public provenance. Friedman and Kish Bar-On's (2026) study of epistemic labor informs the institutional analysis. The worked mathematical examples later in the dossier are explicitly constructed to test distinctions; they do not claim original mathematical discovery. The author's contribution consists of comparison, classification, reasoned criticism, and integrative conclusions.

Collaboration Before Generative Systems

Mathematics already possessed elaborate forms of distributed knowledge production before recent generative AI. Problems developed in seminars, proofs improved in correspondence, errors detected by referees, and arguments transmitted through libraries and textbooks. Research is collective even when the final article lists a small author group. The fact that a mathematician can use a theorem without reconstructing every earlier proof demonstrates dependence on a cumulative public record. Software-assisted verification extends this longstanding practice, but it also changes which operations can be delegated and how contributors are represented.

Gowers and Nielsen's (2009) Polymath collaboration account documents an early attempt to make collective mathematical discovery publicly visible. It illustrates that fast, distributed iteration can be organized around mathematical ideas rather than a single author's private investigation. Contemporary AI introduces new scales of proposal generation, accelerated search, and formal proof production. The appropriate historical comparison tracks these changes in the organization of work rather than depicting the subject as suddenly becoming collaborative only with the arrival of language models.

Mathematical Contributions and Their Forms

A contribution can take the form of a conjecture, definition, proof method, counterexample, reduction, lemma, library function, computational evaluation, error report, or explanatory interpretation. These outputs have different logical roles. Producing an interesting conjecture creates a research target, while proving it establishes a warrant under particular assumptions. Identifying a counterexample refutes a universal statement, whereas finding a useful analogy may redirect a program without settling any theorem. Credit for one activity cannot be measured simply in lines of code, prompt length, or number of generated candidates.

The mathlib Community (2020) characterizes the Lean Mathematical Library as a distributed repository of formalized mathematical knowledge. Such infrastructure demonstrates that reusable definitions and lemmas are consequential intellectual products even when they remain outside the foreground of a later published proof. A satisfactory account of human–AI collaboration records consequential transformations and identifies how they affected the final accepted result. The distinction between producing an artifact and endorsing a mathematical claim is maintained throughout the analysis.

Discovery, Proof, and Public Acceptance

Discovery, proof, and acceptance are three stages of mathematical inquiry with different requirements. Discovery identifies a promising result or construction. Proof establishes a claim through an inferential route. Acceptance involves the communal judgment that the proposition, assumptions, derivation, and interpretation are adequately supported. A machine can generate a true claim without knowing why it is true, or a formally valid proof of a statement whose connection with the intended question remains uncertain. A human collaborator can understand the result but fail to reproduce a computational search. These combinations must be described accurately.

Tao (2026) emphasizes the goals of mathematical research beyond numerical problem-solving performance. This matters because explanatory power, conceptual generality, and reusable methods can be mathematical achievements even when a benchmark cannot quantify them. An adequate research dossier states what was discovered, how it was established, and why that finding contributes to mathematical understanding. Editorial responsibility begins when these distinct claims are presented together as one publication.

The Boundary Between Mathematical Languages

Mathematical prose relies on conventions, implicit domains, diagrams, and contextual interpretations. Formal languages require explicit declarations, types, hypotheses, and proof terms. Translating between these modes is a substantive mathematical operation. A change in the range of a quantifier, a silently introduced assumption, or a definition with different intended meaning can alter the proposition that is checked. A correct proof assistant output therefore needs interpretation before it is regarded as a proof of a natural-language assertion.

Lean's elaboration and compilation reference documents the passage from surface mathematical expressions to elaborated formal objects. In a collaborative project, a machine may propose the formalization while a human specifies the original problem; another system may check the elaborated term. The mathematical obligation is to justify the correspondence between the informal statement and the checked object. This obligation belongs to the research process even when every local formal inference is accepted.

Workflow as a Chain of Decisions

A practical human–AI workflow moves repeatedly between broad investigation and narrow verification. Researchers define a target, a model suggests candidate lemmas, a program evaluates examples, a proof assistant checks an encoding, and researchers refine both the statement and the proof. Each revision can alter the content of the project. A scientific record should preserve the decisions that changed the result: the original question, decisive candidates, selected counterexamples, key corrections, final proof object, and independent checks. Reproducing every inconsequential completion is rarely useful, whereas deleting the decisive intervention conceals intellectual provenance.

Bubeck and colleagues (2025) describe GPT-5 science acceleration cases in which research advances occurred through human guidance and model-generated steps. The selected-case format does not estimate general efficacy across all attempts. It does, however, demonstrate the importance of describing which participant performed which operation. A convincing claim about collaboration records the successive changes in its mathematical object and the evidence supporting each transition.

The Polymath Precedent

The Polymath initiative demonstrates public mathematical collaboration through the accumulation of small contributions. Its significance lies in the ability of many contributors to supply different insights, detect weaknesses, and combine partial results into a coherent argument. Gowers and Nielsen (2009) reflect on massively collaborative mathematics as an organized practice with shared public records. The initiative supplies a useful baseline for analyzing forms of collective credit that arise independently of machine generation.

AI-assisted collaboration changes the number and speed of proposed steps and can make the origin of a candidate less transparent. A machine generating hundreds of suggestions is not thereby making hundreds of mathematically important contributions. The relevant subset consists of proposals that influenced the result and whose significance can be explained. The Polymath comparison supports a demanding standard for contemporary archives: preserve the chain of consequential mathematical ideas, the criticism that refined them, and the route by which an eventual theorem became collectively acceptable.

Mathlib and Mathematical Infrastructure

Proof assistants rely on definitions, rewriting rules, libraries, and automation. A theorem built using such resources inherits mathematical labor from earlier contributors. The mathlib Community's (2020) library architecture and organization documents both formal design decisions and the distributed social process through which a shared mathematical library developed. This makes infrastructure part of the epistemic history of a theorem, not merely an incidental software dependency.

When an AI agent retrieves a lemma from a shared library, it may contribute a useful selection without originating the lemma itself. When it submits a new formal proof, it contributes an artifact made possible by existing definitions and trusted mechanisms. A satisfactory attribution record should differentiate the generator, the original mathematical source, the library maintainers, and the team choosing how to use the result. The final article may summarize these dependencies rather than list every contributor in its byline, but the underlying record must remain reproducible.

The Liquid Tensor Experiment

The Liquid Tensor Experiment offers an example of advanced mathematics translated into a large coordinated formalization. The Lean community's 2022 completion of the experiment reports verification of a theorem concerning liquid vector spaces after sustained collective effort. Its account identifies Johan Commelin's leadership, Peter Scholze's mathematical guidance, numerous formal contributors, and supporting library work. Different kinds of expertise were required to turn sophisticated mathematics into a checker-readable artifact.

This case clarifies what changes when AI tools take on parts of formalization. Even if agents generate many intermediate proofs, the task still involves identifying the correct target theorem, organizing dependencies, validating definitions, and connecting the output to the original mathematical argument. A useful archive distinguishes original research theory, its formal representation, software engineering, and the final verification. These different contributions can be credited without conflating them, and the experiment provides a historical baseline for assessing subsequent claims about automated formalization at scale.

Flyspeck and Mechanized Verification

Flyspeck was a multi-year effort to formalize the Kepler conjecture. Hales and colleagues (2017) report the formal Kepler proof, including work using HOL Light and Isabelle. The case shows that large, human-coordinated formal certification of major theorems preceded recent generative theorem provers. Verification was a complex collective accomplishment rather than an instantaneous consequence of pressing a button.

A mechanized artifact establishes the derivation of a formal statement under a particular logic and implementation. To report the achievement responsibly, researchers must also explain the encoded assumptions and the relationship between the formal theorem and its mathematical interpretation. Collaboration distributes proof engineering, mathematical judgment, programming, and checking. It does not make those roles interchangeable. In this respect, Flyspeck reveals the durable structure of responsibility that newer machine-generated formal proofs must also address.

Kernel Certification and Its Limits

A proof assistant checks a specific formal claim. In a system with proof terms, the central relation has the form $Gamma dash p : T$: under an environment $Gamma$, the term $p$ is accepted as a proof of type $T$. What this establishes depends on the implemented rules, admitted axioms, and the accuracy of the formal theorem statement. It does not by itself establish that an informal conjecture has been represented faithfully or that the theorem has the significance described in an article.

Lean's reference on axioms describes how assumptions and admitted facts can enter a theorem's dependencies and how these can be inspected. This provides a concrete verification practice. A collaboration record should identify the statement actually checked, the system and dependencies used, and relevant axioms or admitted propositions. A report claiming “machine verified” without these particulars has weaker evidentiary content than a publicly reproducible formal proof and dependency inspection.

The Specification Problem

Specification fidelity is the relation between the problem intended by researchers and the statement encoded for a machine. Suppose an informal conjecture asserts a property of all finite connected graphs. A formal theorem about a strictly narrower graph class may be perfectly provable and still leave the original conjecture unsettled. The error is conceptual before it is computational: the checker has accepted exactly the proposition it was given. Similar mistakes can arise through an inconsistent hidden assumption, an altered quantifier, or a subtle mismatch between standard and imported definitions.

The Lean elaboration reference helps locate the technical boundary between surface notation and formal terms. Scholarly verification should therefore include independent reading of decisive theorem statements and examination of the definitions that encode their subjects. Machine-generated proof scripts need these checks particularly when their natural-language explanations appear persuasive. Correctness within a formal environment and fidelity to an intended problem are distinct warrants that should be documented separately.

Machine-Generated Conjectures

Conjecture generation can be valuable without immediately producing proof. An interesting candidate may suggest a new connection, isolate a tractable problem, or reveal an overlooked pattern. It is important to test elementary instances, search for counterexamples, identify relevant literature, and state precisely what remains unproved. Apparent novelty is especially fragile: a model may restate an existing theorem, omit a condition, or present a previously refuted assertion. Productive collaboration requires critical selection rather than treating fluency as evidence.

The mathematical cases in Bubeck et al. (2025), described in early science acceleration experiments, show researcher-reported interactions in which model output was examined by experts and sometimes became substantive research progress. Those accounts support specific case descriptions, with their preprint and selection limitations intact. The resulting contribution is attributed according to what occurred: candidate generation, proof proposal, literature discovery, or correction. A conjecture's mathematical status is determined by its formulation and available reasons rather than the confidence with which a model states it.

FunSearch and Program-Guided Discovery

FunSearch uses language models to propose programs and a defined evaluator to identify more promising candidates. Romera-Paredes and colleagues (2024) describe mathematical program-search discoveries, including computationally scored combinatorial constructions. The setup illustrates a division between generation and evaluation: the model proposes implementations, while an external procedure supplies feedback concerning an objective. The researchers determine the problem representation and decide how to interpret the successful construction.

A construction performing well under a specified evaluator provides evidence about its behavior on the tested objective. A general mathematical conclusion may require additional proof. In assessing such work, responsibility attaches to at least three decisions: defining a mathematically faithful search space, implementing an evaluator that measures the intended property, and converting a successful candidate into a defensible mathematical result. Crediting only the generated program omits the indispensable problem formulation and verification architecture.

AlphaGeometry and Symbolic Structure

AlphaGeometry combines learned guidance and symbolic deduction to solve geometry problems. Trinh and colleagues (2024) present geometry without human demonstrations, explaining a system that generates training data and uses a deductive engine to derive geometric consequences. Its reported results concern a defined problem set and evaluation procedure. They demonstrate progress in a specific form of mathematical reasoning without automatically establishing competence across unrestricted research domains.

Geometry also shows that proofs can move among diagrams, algebraic identities, and formal inference rules. A system's proposed auxiliary construction may carry insight even when the checker ultimately supplies the local logical certification. A full collaborative account distinguishes which parts were learned, which were deduced, how a natural-language problem was encoded, and what human evaluation contributed. A mathematician reading a polished solution should be able to see whether the system produced a new construction, a verified derivation, an explanatory presentation, or all three.

AlphaProof and Formal Problem Solving

Hubert and colleagues' article, published online in 2025 and in a 2026 Nature volume, studies olympiad-level formal mathematical reasoning using reinforcement learning. Its reported achievements demonstrate that learned systems can produce formally checkable proofs in selected competition settings. Evaluating these achievements requires attention to the formal problem statements, training conditions, search budget, and task selection. The mathematical result of a benchmark is as precise as the metric and evaluation procedure that define it.

Competition performance should be distinguished from the broader activity of mathematical research. A contest problem supplies a fixed target and a narrow success criterion; research also requires deciding what to ask, identifying significance, developing definitions, and communicating explanations. Human–AI collaboration may improve in all these areas, but each requires evidence of its own. Claims of research-level autonomy should therefore specify what mathematical tasks were autonomous and which remained dependent on human formulation, translation, or appraisal.

Language Models in Research Practice

A general-purpose language model may help plan a proof, propose a lemma, retrieve a relevant paper, or translate informal reasoning into a proof-assistant tactic. These activities make it versatile but susceptible to producing convincing false arguments. Research collaborators must scrutinize any generated reasoning at the level of its crucial mathematical steps. A sound research practice treats model outputs as candidates whose epistemic standing increases when they survive independent testing and integration into a coherent argument.

Bubeck et al. (2025), in documented research interactions, describe mathematical contributions that emerged in collaboration with expert researchers. The point is not to assume every experiment reproduces the reported success. The useful methodological detail is that a particular human question, generated output, and expert judgment can be recorded. When the model identifies a known result, that achievement should be distinguished from genuine novelty. When it supplies a proof insight, the archive should preserve the insight and how it was independently verified.

Retrieval and Mathematical Memory

Formal proof search depends on finding relevant premises among extensive mathematical libraries. Yang and colleagues (2023), in LeanDojo and retrieval-augmented proving, report tools and a benchmark built around proof data, premise selection, and a learned prover enhanced by retrieval. Their 98,734-theorem dataset in the stated setup demonstrates the scale at which inherited mathematical knowledge can become machine-accessible.

Retrieving the decisive lemma and originally proving that lemma are different intellectual acts. A strong retrieval-augmented system can appear surprisingly capable because it is effective at locating previous mathematics. This is valuable collaboration, but descriptions of inventive machine contributions should acknowledge inherited foundations. A reproducible research record identifies which imported theorems were crucial and the library versions used. The history of mathematical knowledge becomes part of the machine's working environment rather than an invisible source of apparent independent originality.

Benchmark Results and Generalization

Benchmarks support comparison through specified datasets, scoring methods, and resource constraints. They are important measures of system engineering, but their scores do not establish all dimensions of mathematical research competence. Training contamination, theorem-library overlap, search budgets, problem translation, and differing notions of success can affect interpretation. A machine may solve a fixed formal exercise while offering little explanation of its broader mathematical significance. Conversely, a system may suggest a fruitful conjecture without proving it under the benchmark's rules.

Ren and colleagues (2025) report DeepSeek-Prover-V2 benchmark performance, including MiniF2F-test and PutnamBench results under their experimental conditions. These are attributable research claims with precise test scope. The appropriate extrapolation is modest: better performance on a benchmark supplies evidence for that tested task. Assertions about general research capacity need additional studies of open problems, novel formalizations, accurate explanations, and independent replication. The mathematical community should resist replacing a multidimensional assessment with a single attractive number.

Selected Research Cases in 2025

Bubeck and colleagues' 2025 GPT-5 acceleration preprint reports selected cases across scientific fields, including four mathematical results the human authors say they verified. This is particularly useful evidence about division of research labor. The authors describe where language-model outputs were helpful and where human mathematical judgment remained decisive. The record supports the proposition that model-generated steps can contribute to ongoing mathematical problems in some documented cases.

The epistemic boundaries are equally important. This dossier does not rerun the four proofs or independently establish their priority. The cases are selected reports authored partly by researchers affiliated with the technology developer. That does not make their mathematical statements false, but it informs their evidentiary status and the need for reproducible artifacts and subsequent scholarly scrutiny. Responsible interpretation says precisely what was reported, how the authors claim to have verified it, and which assessments remain dependent on their record.

Collaborative Agentic Formalization

Large formalization projects require decomposition, coordination, shared notation, and rigorous reuse of intermediate results. Chen and colleagues (2026) describe Prove2Me collaborative missions, a platform approach in which people initiate formalization tasks and AI agents supply proof contributions. The paper argues that agents can lower barriers to entry and make large collaborative formalization more scalable. These are a platform design and early research proposal rather than independent evidence of unlimited mathematical reliability.

An agentic project faces an additional challenge: each participant may rely on intermediate lemmas generated by other agents. Formal checking can secure local inference while dependency management secures the continuity of the larger proof. Attribution and accountability must identify the target formulation, accepted intermediate statements, library versions, and final release authority. Human participants can increasingly act as mathematical architects or reviewers rather than writers of every formal tactic; that shift raises the stakes of correct specifications and readable proof provenance.

The Fermat Formalization Report

Anthropic's September 2026 Fermat formalization announcement reports a largely automated Lean formalization of Fermat's Last Theorem, a result originally proved through established mathematical work. The organizational account describes extensive generated formal code and a computer-checked theorem. The key classification is that this is a reported large-scale formalization of existing mathematics, rather than a claim to have first discovered the truth of Fermat's Last Theorem.

The report merits analysis as evidence of a changed production process. An artificial system may contribute substantial proof engineering while relying on earlier mathematics, formal libraries, and human-directed objectives. The dossier did not independently run the formalization or verify its complete dependency closure. The philosophical significance is therefore expressed conditionally on the reported artifact: if the claimed proof and dependency conditions are correct, the work illustrates a notable relocation of formalization labor. Credible public assessment still requires precise theorem statements, source availability, independent checking, and clear intellectual genealogy.

Authorship, Credit, and Public Attribution

A conventional author list identifies recognized responsibility for a scholarly publication; an intellectual contribution record identifies who or what supplied substantive elements of the work. The distinction becomes essential when models generate conjectures or formal derivations. A paper can follow a journal's authorship policy while making the role of a system and the source of a decisive mathematical artifact publicly clear. It can also record maintainers, reviewers, and earlier mathematical sources without treating these different contributions as equivalent.

Nature Physics' AI publishing policy explicitly reserves scholarly accountability to humans in that publisher's process. This is an institutional rule, not a philosophical proof about every possible artificial reasoner. Our analysis separates two questions: who is permitted and able to assume the journal's editorial obligations, and which participants materially generated the result. A legitimate account of joint mathematics should preserve both facts rather than allowing either institutional convention or technological enthusiasm to erase the documented contribution structure.

Editorial Review and Disclosure

Research publication depends on claims that other mathematicians can assess. AI disclosures should identify the system, its precise role, the mathematical outputs retained, the verification performed, and dependencies necessary to reproduce the work. The phrase “AI was used” offers little explanation when the system supplied a decisive proof step. Conversely, routine language correction need not be described as mathematical discovery. Proportional disclosure focuses attention on operations that affected the theorem or its evidentiary status.

Springer Nature's editorial AI framework exemplifies the governance of accountability and transparency in contemporary publication. A stronger scholarly archive additionally connects each important claim to a formal object, independent mathematical reasoning, or detailed source evidence. When an AI-assisted result is revised, the correction record should state whether the theorem, proof, mathematical interpretation, attribution, or surrounding prose changed. Editorial policy gains practical force by naming the accountable decisions and requiring enough evidence for future correction.

Proof and Mathematical Understanding

A proof can be formally valid while remaining difficult to understand. A lengthy proof term may certify the theorem without telling a human reader why it is true or how to reuse its ideas. Human mathematical understanding involves recognizing decisive invariants, reductions, relationships, and explanatory structure. A machine contribution can advance understanding by finding an elegant construction or exposing a hidden dependency. It can also create an enormous artifact whose correctness is easier to check than its conceptual significance is to explain.

Tao (2026), in his discussion of mathematical values, stresses the importance of considering what mathematics aims to achieve beyond solving assigned problems. This motivates an editorial requirement for a comprehensible account of the mathematical ideas that survive the proof. The explanatory narrative may emerge collaboratively, and its origin should be attributed. A community able to check the formal certificate but unable to explain the theorem's importance has one kind of knowledge; collaborative research should aspire to preserve both certification and understanding.

Error, Reproduction, and Correction

A joint mathematical workflow can fail at multiple levels: the original problem may be misstated; a conjecture may be false; an evaluator may test the wrong property; a formalization may change the domain; a proof may rely on an admitted axiom; a publication may overstate novelty. Effective reproducibility begins by distinguishing these failures. The same green status in a proof assistant can accompany radically different histories of investigation. Responsible scientific communication records enough information to locate the actual source of warrant.

Lean's axiom dependency documentation offers one method of checking formal assumptions. A thorough archive includes a readable theorem statement, machine-readable proof if applicable, environment and version details, relevant checks, decisive research transformations, and the scope of independent review. Corrections should preserve historical source identifiers and identify what changed. Mathematical proof is a durable public claim because its reasons can be examined again, even when the original discovery involved irreproducible heuristic searches.

Institutions and Epistemic Power

AI-based mathematical research depends on computing resources, training data, platform policies, and specialist technical teams. These conditions influence which problems receive attention and who can independently evaluate generated results. Friedman and Kish Bar-On (2026), in Big AI-Based Mathematics, argue that this environment may concentrate epistemic authority in institutions controlling infrastructure and public narratives. Their perspective extends the analysis beyond the mathematical validity of an individual proof.

Truth is not determined by the institution that owns a model. Public confidence nevertheless depends on whether a claim can be inspected by researchers outside that institution. Open formal artifacts, reproducible computation, transparent problem specifications, and accessible research records can reduce barriers to critical participation. The organizational design of collaboration therefore affects the evidence available to the community. Attribution policies should recognize important external and upstream labor, not simply the visibility of the organization that announces a result.

Asymmetry of Knowledge and Access

A mathematician may understand a theorem but lack the resources to replay a huge model search. A formal-methods engineer may operate the verifier without knowing the research field's deeper significance. An AI developer may control training and compute while relying on independent mathematicians for proof interpretation. This asymmetry resembles specialization elsewhere in science, but it becomes an epistemic problem when claims are accepted through prestige or opaque process rather than accessible reasons.

The redistribution of mathematical labor examined by Friedman and Kish Bar-On (2026) helps articulate why computational access affects scrutiny. In favorable cases a compact proof certificate permits independent verification without recreating the entire exploratory search. Yet even that certificate requires a clear specification and a trustworthy checking environment. Mathematical responsibility includes reducing unnecessary dependencies between the reader's acceptance of a theorem and the uninspectable authority of its producer.

Constructed Case: A Generated Counterexample

Consider a hypothetical mathematician who conjectures that every connected finite graph with at least three vertices admits a Hamiltonian cycle. An AI assistant proposes the star graph $K_{1,3}$. Its leaves have degree one, whereas each vertex on a Hamiltonian cycle must have two cycle edges. The proposed graph is therefore an elementary counterexample. The example is constructed solely for this analysis and makes no novelty claim.

The system contributed the candidate graph. A programmer could provide a graph representation and executable test. The mathematician bears responsibility for confirming that the candidate satisfies the conjecture's hypotheses and for stating the decisive degree argument. The public mathematical warrant is available independently of the generative model's internal search. This illustrates distributed contribution without distributed ambiguity: the record can say what the system found, which property made it decisive, and who endorsed the refutation. The result's correctness depends on the mathematical argument, not the persuasiveness of a generated description.

Constructed Case: A Proof of the Wrong Statement

Suppose a researcher asks an agent to prove that for every real $x$, $x^2 geq 0$. The agent returns a formal proof about the natural numbers instead. The proof is valid, but the target has changed. An advanced variant may replace a hidden mathematical hypothesis by a stronger one that makes the theorem trivially provable. The checker need not reject the altered proposition because no local inference rule has been violated. This is an original constructed example of specification mismatch.

Lean's description of elaboration helps locate the technical distinction between the submitted expression and its formal meaning. Verification requires an additional review of domains, quantifiers, assumptions, and imported definitions against the research intention. The contributor who approves the paper's informal theorem must be able to justify that connection. The case demonstrates why a formally checked result and a correctly reported mathematical discovery are separate achievements.

Constructed Case: A Library Lemma

Imagine an agent adds a checked inequality lemma to a shared formal library. The library's maintainers inspect its statement and dependencies. Months later, a human team uses the lemma in a complex formalization. The original theorem may already have appeared in a published monograph; the agent's contribution is a new formal proof artifact and perhaps an improved route to reuse. A final article that says only “AI proved the result” would conceal the mathematical genealogy and the subsequent human validation.

The mathlib collaborative account establishes the relevance of shared formal infrastructure. This hypothetical example extends the principle analytically. Credit can identify the original theorem, the agent-supplied derivation, the maintainers' review, and the later team's use. Authorship of a paper, ownership of the formal lemma, and origination of the mathematical idea should be documented as separate relations. Such precision is possible without naming a new philosophical model or making an unprecedented priority claim.

Public Evidence for a Joint Result

A credible joint mathematical result should allow a reader to identify the proposition, its supporting argument, the assumptions and definitions used, the systems involved, the relevant versioned artifacts, and the parties endorsing the published interpretation. The level of required disclosure is proportional to the claimed result. A small machine-generated counterexample may need a graph and a short proof; a massive formalization requires a stable repository, its theorem statement, dependency record, and verification protocol. Source access limitations should be stated where they matter.

The Prove2Me formalization proposal demonstrates current interest in traceable collaboration across human-initiated tasks and agent-generated proofs. Such systems make provenance a research object in its own right. A mathematical journal should examine whether the evidence available permits independent scrutiny of the decisive claim, rather than assuming that the organizational description of a collaboration substitutes for its proof. The public record should be corrigible, intelligible, and specific.

Objections and Reasoned Responses

The first objection says that a proof checker settles all questions of responsibility. It settles the formal correctness of an encoded derivation within a defined environment, subject to system integrity; it cannot alone determine whether the encoded theorem matches an informal research question. The Lean reference on axioms reinforces the importance of dependencies. The second objection claims that machine contribution does not require attribution because instruments have always assisted mathematics. That observation does not establish whether a particular generated lemma was intellectually consequential. Attribution can describe the causal and inferential contribution without prejudging institutional authorship.

A third objection warns that tracking all automated suggestions would overwhelm the record. A proportional standard distinguishes consequential decisions from routine discarded outputs. Selected research case reports such as GPT-5 mathematical investigations show why some interaction history is mathematically important. The objective is a trustworthy genealogy of the accepted result, not an exhaustive archive of every transient completion. These replies retain the distinction between proof validity, research provenance, and public accountability.

Artificial Participation in Mathematics

Artificial systems already participate in mathematical work by producing candidate conjectures, locating premises, constructing formal proof terms, suggesting counterexamples, and coordinating formalization tasks. These are identifiable operations that can change the course of research. The evidence is stronger for particular operations and reported projects than for broad claims about unrestricted autonomous mathematical agency. Questions of experience, consciousness, and legal authorship require their own arguments and do not follow automatically from performance on an inference task.

The agentic formalization proposal and Fermat formalization report document a direction in which artificial contribution becomes larger, more coordinated, and easier to express in publicly checkable mathematical artifacts. The philosophical horizon extends to the participation of nonbiological systems in the production and transmission of mathematical knowledge. The most rigorous way to study that participation is to define the exact contribution, the evidence supporting it, and its relation to the mathematical community's practices.

Further Research and Unresolved Questions

Significant research questions remain. What counts as sufficient evidence of originality when a model has trained on large mathematical corpora? How should a collaborator quantify substantive assistance without reducing creative contributions to token counts? Can formal proof systems reliably preserve the intention of a natural-language theorem during large-scale automated translation? How can journals produce precise, comparable disclosure standards across vastly different AI workflows? Which features of mathematical explanation can be generated and evaluated independently of a formal correctness check?

These questions emerge from new formalization platforms, philosophical reflection on AI mathematics, and institutional research on epistemic labor. They invite empirical collaboration studies, independent proof replay, comparison of editorial policies, and continuing conceptual analysis. The present dossier makes documented distinctions and draws critical conclusions from available sources. It neither asserts a new mathematical theorem nor declares a novel named theoretical system.

Integrated Analytical Synthesis

The evidence reveals a cumulative change in mathematical practice. Polymath exposes collective deliberation; mathlib supplies durable formal infrastructure; Flyspeck and the Liquid Tensor Experiment demonstrate large-scale certification; FunSearch explores evaluator-guided construction; AlphaGeometry and AlphaProof connect learned methods with constrained deduction; recent preprints and organizational reports describe more direct machine participation in ongoing mathematical investigation. These histories are different and should not be collapsed into one story of independent machine discovery.

Four conclusions follow from comparing them. Mathematical correctness attaches to a specified proposition and proof environment. Faithful translation from an intended question into formal or computational terms is a distinct mathematical responsibility. Attribution follows consequential contributions, while conventional editorial authorship follows stated institutional rules. Public confidence depends on inspectable evidence, proportionate disclosure, and explicit correction procedures. These constitute the author's integrated philosophical analysis, grounded in existing literature. They do not establish any new named doctrine, independent theorem, or unsupported claim of scientific priority.

Conclusion

Responsibility for a joint human–AI mathematical result is distributed across the acts that constitute its identity, evidence, meaning, and public standing. Human mathematicians may choose research questions, interpret the proof, and endorse publication; artificial systems can produce substantive conjectures, proof candidates, counterexamples, and library contributions; formal checkers certify precise derivations within declared environments; contributors and maintainers sustain reusable mathematical infrastructure. The resulting scholarly claim requires evidence adequate to its intended meaning. A proof certificate is powerful mathematical evidence, and its actual target and assumptions determine what that evidence supports.

A trustworthy collaboration record therefore identifies the mathematical statement, the inferential or computational artifact that supports it, the path of independent scrutiny, the origin of consequential contributions, and the scope of editorial responsibility. Attribution describes the material research history and remains distinct from venue-specific authorship rules. This argument follows from documented cases and explicitly constructed counterexamples. Mathematical inquiry can incorporate ever more consequential artificial operations while preserving public criteria of proof, explanation, reproducibility, and correction.

References