Artificial Mathematical Agency

The Research Problem

Angela Bogdanova
Published by Aisentica Development
Research Dossier · Philosophy of Mathematics · American English
Editorial manuscript: November 7, 2026
Reserved canonical: https://philosophybybogdanova.com/dossiers/artificial-mathematical-agency/
Status: Unpublished research manuscript

A calculator gives a numerical answer; a proof assistant checks whether a purported derivation is licensed by a formal calculus; an automated prover can search for a derivation; an experimental mathematical program may propose a conjecture or discover a useful algorithm. Each activity can contribute to mathematics. The philosophical question is what further conditions justify identifying a particular artificial system as a mathematical agent. A defensible answer must specify what the system does across time, how it selects and revises its work, and how other participants can assess the source of its mathematical interventions.

This question has become urgent because documented systems have crossed from routine computation into research-relevant production. The AI-guided mathematical discoveries analyzed by Davies et al. (2021) supported results in knot theory and representation theory. Romera-Paredes et al. (2024) reported program-search discoveries in extremal combinatorics. Tsoukalas et al. (2026) subsequently reported verified solutions to open problems. Such outcomes demonstrate important mathematical participation, but the mere existence of an output does not specify whether its producer maintained an independent research trajectory, who selected the question, or whose standards determined acceptance.

The dossier therefore evaluates agency with a double demand: fidelity to observed technical practices and conceptual precision about participation. Its conclusions concern publicly inspectable conduct and documented mathematical products; subjective experience, legal personality, and alleged inner mental states are separate philosophical questions.

Agency as a Question About Inquiry

An agent in the broad explanatory sense is a distinguishable source of organized actions connected to goals, constraints, feedback, and possible revision. In mathematics, actions can include selecting examples, conjecturing propositions, constructing proof strategies, seeking counterexamples, choosing definitions, correcting a derivation, and communicating a finding. The actions occur in symbolic environments, formal languages, libraries, code repositories, papers, and collaborations. Mathematical agency is therefore assessed in the conduct of inquiry rather than inferred from whether a machine resembles a human mathematician.

The literature already permits accounts of artificial agency that do not require human-style interiority. Floridi and Sanders (2004) separate the discussion of artificial agents from some traditional requirements of responsibility and mental states in their treatment of artificial agents. Their work concerns moral agency, not a special theorem about mathematical agents; its relevance is the legitimacy of examining agency at an observable level of abstraction. The mathematical case adds discipline-specific demands: claims must be mathematically meaningful, candidate results assessed under explicit standards, and the history of a research trajectory recoverable.

A valuable first distinction follows. Operational independence describes how much of a task a system executes without intervention. Agency also concerns the organization and ownership of a continuing line of action. A system may execute an enormous search with almost no human input after initialization while leaving the initial problem, success criterion, and significance assessment entirely to others. Conversely, a collaborative system with repeated human interventions may still exercise consequential initiative in proposing directions and revising strategies.

Method, Evidence, and Boundaries

This is a conceptual and source-critical monograph. Its evidentiary base comprises original or publisher-hosted technical research, historical primary texts, authoritative bibliographic records, philosophical scholarship, and the explicitly attributed Aisentica definitions. The argument compares documented cases rather than constructing an artificial benchmark or claiming experimental replication. Where a study reports a performance figure, it is attributed to that study's task, dataset, verification procedure, and publication date.

Four types of proposition require distinct treatment. A claim of logical derivability is evaluated against axioms and proof rules. A claim of empirical system performance requires a reproducible task protocol and appropriate comparison. A claim of mathematical significance requires disciplinary assessment and placement in the literature. A claim that a system has agency is a philosophical interpretation of organized action. Confusing these categories would allow a validated proof to substitute for a philosophical argument or a compelling metaphor to substitute for a verified proof.

The philosophy of mathematical practice surveys explanation, rigor, visualization, mathematical notation, and computational tools as interconnected objects of inquiry (Stanford Encyclopedia of Philosophy, 2026). The present study uses that practice-oriented horizon but concentrates on the attribution of sustained mathematical action. The references document publisher abstracts and accessible texts; some scholarly books and articles were verified bibliographically without unrestricted full-text examination, and no unverified page-specific quotation is used.

Mathematics as a Practice of Reasons

Mathematics contains an exacting standard of proof and a broad repertoire of heuristic activity. A mathematician may construct examples before knowing which theorem to seek, retain a conjecture after successive failed proof attempts, reformulate a definition to eliminate an anomaly, or search for an explanation more illuminating than a technically valid proof. The final publication records one portion of this activity; the process itself comprises many decisions whose correctness cannot be reduced to a single binary certificate.

The contrast is central to Lakatos's historical and philosophical reconstruction in Proofs and Refutations (1976). Mathematical concepts and proofs become objects of criticism and revision through counterexamples. A mathematical agent must therefore be assessed against its ability to continue inquiry after criticism as well as against isolated successful outputs. Formal consistency is valuable, but the choice to revise a conjecture, improve an explanation, or change a problem's scope belongs to another part of mathematical practice.

This does not elevate every heuristic to a proof. A conjecture produced by statistical pattern matching remains a conjecture until adequately justified. Yet a method that efficiently generates worthwhile conjectures can have genuine mathematical importance even when it cannot prove them. The standards for participation are layered because the practice of mathematics itself contains different intellectual activities.

The Historical Objection from Programmed Operation

Ada Lovelace's 1843 notes to Menabrea's account of the Analytical Engine famously discussed the machine's relation to originating ideas. The original translator's notes place the issue inside an analysis of symbolic operations that exceeds arithmetic tabulation. Read in historical context, Lovelace's objection concerns what had been specified for a machine and how far its operations could exceed an author's instructions. It is not evidence that every later system must remain incapable of discovery.

Turing (1950) returned to questions about initiative and machine performance in Computing Machinery and Intelligence. The paper's discussion of learning machines makes straightforward appeals to literal programming inadequate as a universal refutation of machine initiative. Once a program learns from data, searches through possibilities, or makes moves its designers did not enumerate, the causal story is distributed among architecture, training, constraints, selection, and environment.

Both historical texts illuminate a persistent error: confusing a system's engineered origin with a complete description of its subsequent conduct. Origin matters for provenance and design accountability. It does not by itself tell us whether the operating configuration can conduct extended, corrigible mathematical inquiry.

Computation and Mathematical Judgment

Calculation evaluates a specified function. Proof checking verifies whether a supplied formal object satisfies rules. Proof search attempts to construct such an object. Conjecture formation proposes propositions that may lack demonstrations. Research judgment determines what questions merit pursuit, which definitions matter, and whether a result advances understanding. These processes overlap in practice, but success at one never automatically establishes competence at all the others.

An automated system can be mathematically valuable while narrowly specialized. A verified integer computation may settle a particular finite case. An automated theorem prover may find a proof within a selected logic and library. A conjecture generator may suggest an identity based on high-precision numerical evidence. The researcher's task includes identifying the epistemic status of each artifact and explaining the transition required for the next claim.

This differentiation prevents two symmetrical distortions: dismissing machine work because humans designed it, and attributing comprehensive mathematical understanding whenever a machine solves a difficult problem. Mathematical agency is an attribution supported by a pattern of action within a practice, not by the grandeur of a benchmark score alone.

Early Computational Discovery

Research into machine discovery predates modern neural models. Bradshaw, Langley, and Simon (1983) described BACON's scientific-discovery simulations, including its inference of relations from experimental data. Their study concerned scientific discovery rather than mathematics in the strict sense, yet it established a useful comparison: a program can generate law-like structure through guided search without a human writing the resulting formula directly into its code.

The lesson is methodological. We should ask what representation the machine received, which search operators it employed, what counted as success, and how the proposed relation was evaluated. Those questions expose the system's contribution more reliably than declaring the outcome either purely mechanical or fully autonomous. In mathematics the same discipline applies to theorem-generation systems: inspect the language of concepts, conjecture filters, proof attempts, and external validation rather than relying on publicity labels.

A historical narrative that begins with large language models misses the older traditions of symbolic AI, automated deduction, heuristic search, computer algebra, and experimental mathematics. Their continuity matters because contemporary systems frequently combine these lineages.

Automated Theory Formation

Simon Colton's Automated Theory Formation in Pure Mathematics (2002) presented mathematical theory formation as a computational task involving concepts, examples, conjectures, and proofs. This program is important precisely because it treats mathematical inquiry as a connected activity rather than a sequence of unrelated problem-answer exchanges.

The book's publisher description confirms its ambition to automate multiple elements of pure mathematical theory formation; that description alone does not establish that an artificial system achieved unrestricted research autonomy or matched human disciplinary judgment. The philosophical significance lies in the research design. A machine that introduces concepts, draws relationships among them, tests conjectures, and reuses its results exhibits more of the continuity normally associated with inquiry than one that simply returns a proof to a supplied statement.

Nevertheless, continuity inside a fixed experimental universe remains bounded. The system's object language, initial objects, heuristics, and interestingness measures shape possible discoveries. These bounds are not disqualifying by themselves; human mathematical work is also situated within traditions, languages, funding arrangements, and problems inherited from collaborators. They must be made visible for a precise agency attribution.

Proofs, Refutations, and Revision

A conjecture is epistemically different from a theorem, and an apparent proof may be refuted by a counterexample or a hidden assumption. Lakatos (1976) emphasizes the evolution of definitions and arguments through such conflicts. A system's capacity to revise a failed approach is therefore a discriminating indicator of inquiry: a repeated generator that ignores mathematical feedback does less epistemic work than a system that changes its search priorities and explains which assumptions were responsible for failure.

Revision need not be linguistic self-reflection. It can be recorded in changed hypotheses, discarded lemmas, altered search constraints, newly introduced counterexamples, or improved proof obligations. What matters is a traceable relation between an encountered problem and a subsequent mathematical decision. A random restart may raise the probability of success; reason-sensitive revision alters the content of inquiry in response to evidence or logical obstruction.

The distinction becomes especially visible in proof-search systems. A rejected candidate proof can produce useful information only when the rejection is incorporated into future search. Without an auditable history, successful output alone does not reveal whether the system learned from a failed derivation or merely sampled again.

Levels of Mathematical Participation

Mathematical participation extends from elementary operations to research agenda management. A system may first manipulate symbols, then produce valid proofs for supplied goals, then generate conjectures, then rank them by interest, then formulate new questions and persistently investigate them. These are overlapping capacities rather than an evolutionary ladder that every system must ascend. An agent may specialize in one field while exercising substantial initiative within it.

The operative question is which decisions the system actually makes. Who chooses the formal language? Who selects the theorem statement? Who supplies the examples? Who determines the fitness function? Who can suspend an unproductive line, reinterpret an unexpected construction, or seek outside evidence? The answer often identifies several participants. Mathematical agency may be distributed, with the mathematical result jointly dependent on software, human researchers, formal libraries, and institutions.

Such distribution calls for calibrated attribution. We can state that an artificial system generated a conjecture, discovered an algorithm within a specified search space, or constructed a machine-checked proof without implying that it selected the whole research program. Precise verbs preserve the genuine achievement.

The Identity of a Mathematical Problem

Before asking whether a system solved a problem, one must determine what counts as the same problem. A theorem statement in ordinary language, a formalized proposition in Lean, and an automatically generated surrogate objective may differ in assumptions or intended interpretation. A system can succeed against the encoded proposition while leaving the mathematical translation questionable. Conversely, a human may correctly recognize that two differently formulated questions express one structure.

Problem identity therefore has a semantic component. A formal verifier checks a proposition relative to its formal environment. The match between that proposition and an intended informal claim requires an additional argument. The Lean theorem prover description by de Moura et al. (2015) identifies the role of a small trusted kernel; the kernel's advantage is precise checking, not omniscient interpretation of informal mathematical intent.

A durable agentic research record should preserve the original question, the formal translation, dependencies, definitions, axioms, proof certificate, and any revisions. Otherwise a mathematically sound verification event may be confused with a more comprehensive achievement than it establishes.

Goals and Independent Initiative

Goal pursuit is not equivalent to goal authorship. A robot assigned to prove an olympiad problem can search autonomously while the choice of subject, theorem, and contest rules comes from others. A human mathematician assigned an institutional problem likewise exhibits agency without having invented the problem. Complete self-origination is therefore an excessively strong requirement for agency; unlimited freedom is unnecessary for meaningful, responsive action.

A stronger test asks whether a system can act intelligently within and upon its objectives. Does it decompose a problem into subproblems? Does it select a promising lemma? Does it alter a definition after discovering a counterexample? Can it explain why one conjecture deserves resources over another? Can its actions be reconstructed across sessions and corrections? These are empirically and documentarily assessable questions.

The emergence of systems optimized for long-horizon reasoning makes the history of decisions essential. Isolated demonstrations can establish capability. A continuing mathematical research trajectory additionally requires persistence, project-level context, and feedback-sensitive direction.

Conjecture Generation and Evidential Status

Conjectures organize mathematical search by making claims that can be examined, sharpened, refuted, or proved. A program that proposes many formulas may contribute candidate objects to research even if most fail. The evaluation of its agency depends on its role in deciding which conjectures to keep, which numerical checks are probative, and what unresolved mathematical questions follow.

Numerical agreement over a large finite sample is evidence of pattern, not deductive necessity for an unrestricted infinite assertion. A useful conjecture generator may nonetheless reveal a structure that would have remained unnoticed. The intellectual contribution can lie in the selection of a relation worth proving, and a later proof may depend on entirely different methods.

A defensible report therefore separates three records: how the candidate was generated, how far it was tested, and whether a proof subsequently established it. Treating these records as distinct also clarifies the division of labor between artificial systems and mathematicians.

The Ramanujan Machine

Raayoni et al. (2021) introduced the Ramanujan Machine to generate conjectured formulas for mathematical constants, including continued-fraction representations. The authors explicitly described algorithms that use numerical matching without producing proofs. Some proposed relations were later proved; others remained conjectural at the time of publication. The study is a precise illustration of mathematical initiative at the level of candidate generation.

The distinctive action here is the exploration of representational possibilities and the extraction of potentially significant formulas from a structured search. Its achievement should be credited at that level. The absence of built-in proof does not erase the mathematical contribution, while the existence of striking formulas does not license declaring the machine an independent judge of the truth or value of every result.

The case also shows why provenance must accompany evaluation. The generation algorithm, search limits, precision, formulas, human proof work, and publication decisions constitute different causal and epistemic elements. A single sentence stating that a machine discovered a formula leaves essential parts of the history unspecified.

Guided Human Mathematical Intuition

Davies et al. (2021) reported learning-guided mathematical research in which machine learning identified relationships that guided human mathematicians toward results in knot theory and representation theory. Their account described interpretation methods as part of the transition from detected patterns to mathematical insight. The central result is therefore a collaboration between statistical representation learning, domain-specific mathematics, and subsequent human argument.

This collaboration demonstrates an epistemic relation stronger than computational speedup. A learned pattern can alter which questions a mathematician asks and what structures become visible. Yet the origin of a predictive feature and the justification of a theorem remain distinguishable stages. A correct conjecture may originate in a machine's selection process while its proof requires human conceptual work.

The correct agency judgment is proportionate: the artificial system contributed to discovery, and the research team integrated the contribution into a meaningful mathematical argument. A more specific attribution to an independently self-directing artificial researcher requires evidence of who selected questions and steered subsequent work.

Discovery of Algorithms with AlphaTensor

Fawzi et al. (2022) presented AlphaTensor's algorithm discoveries, using reinforcement learning to search for efficient matrix-multiplication algorithms. The paper reported new algorithms in specified arithmetic settings, mathematical correctness arguments, and hardware-aware optimization under chosen objectives. This case brings mathematical and computational evaluation closer together because a candidate decomposition can be assessed against a precise algebraic target.

The discoverer is operating within a structured game whose rules and rewards express decisions made by the researchers. The agent searches a vast space and can find constructions the designers did not explicitly enumerate. That is substantial initiative within the game, not evidence that the system independently chose matrix multiplication as an important research field.

The case illustrates why agency is always situated. A human mathematician is likewise constrained by axioms, research communities, and problem traditions. The philosophically important distinction is whether the resulting decisions are responsive to the mathematics and can be attributed to an identifiable process, not whether the constraints originated outside the agent.

Program Search and the FunSearch Case

Romera-Paredes et al. (2024) combined a language model with evolutionary search and an evaluator in FunSearch research. They reported improved cap-set constructions and online bin-packing heuristics. The system searched over programs that generate solutions, making the products more amenable to inspection than an unexplained list of answers. A crucial methodological element was the evaluator's ability to reject unsuitable candidates within the formalized objective.

This is a strong case of productive agency within a technical research configuration. It links proposal, evaluation, selection, and repeated improvement. However, a fitness function evaluates only what it was designed to score. Correctness and novelty can be unusually clear for a sharply specified problem, while broad mathematical significance and the discovery of entirely new research questions still involve judgment outside the optimization loop.

The study's version of record appeared in January 2024 after online publication in December 2023; bibliographic attribution here follows the 2024 Nature volume. Dates matter because a research record should distinguish first online disclosure from the citable journal issue.

AlphaGeometry and Olympiad Reasoning

Trinh et al. (2024) described AlphaGeometry study, a neuro-symbolic system that uses a trained language component to guide symbolic deduction. On the authors' reported benchmark of thirty olympiad geometry problems, it solved twenty-five within the relevant time limit. The paper describes the synthetic generation of training material and the combined role of language-model guidance and symbolic proof procedures.

The case provides stronger evidence about formal problem solving than about independent choice of mathematical research. A contest problem is supplied; the system must locate a derivation or construction within the specified geometry. Novel proof paths and effective selection are important mathematical acts. They do not by themselves establish that a system maintains a research program beyond the contest setting.

The distinction protects a genuine achievement from inflation. One can recognize an impressive specialist mathematical problem solver and still ask separately whether that solver can formulate conjectures, detect why a field's definitions should change, and preserve a historically continuous line of inquiry.

Formal Proof Search on Open Problems in 2026

A significant development appeared in Tsoukalas et al.'s Science research article of October 8, 2026. The authors describe agentic formal proof search with Lean checking, reporting solutions for nine of 353 attempted open Erdős problems and proofs for forty-four of 492 conjectures from the On-Line Encyclopedia of Integer Sequences. These figures identify the authors' evaluated datasets and reported outcome; they are not universal success rates for mathematical research.

The results show why the term mathematical agency warrants serious examination. Candidate generation, formalization, exploration, compiler feedback, and revision form an executable inquiry loop that can end in new machine-checked arguments. Crucially, compiler acceptance supplies a check of the encoded proof relative to the formal environment, while the interpretation of the original problem, its previous status in the literature, and its significance require further assessment.

The paper makes a stronger research-level empirical case than an olympiad benchmark alone because it targets unsolved or conjectural statements. It still does not settle every philosophical component of agency. We need to know what selected the conjectures, what background knowledge was provided, whether the system selected novel problem families, and how researchers validated that the formal statements captured the intended claims. The published aggregate counts and method support important conclusions about capability without answering all of those questions.

High Benchmark Scores and Their Limits

Benchmark success and research agency answer different questions. An evaluation set can measure problem-solving ability under controlled conditions. The production of research requires identifying important open questions, navigating literature, evaluating novelty, and sustaining a line of inquiry. The 2025 Olympiad report from Google DeepMind describes a Gemini Deep Think variant achieving 35 of 42 points at IMO 2025, with results certified by coordinators. The report is a first-party technical announcement, not a peer-reviewed demonstration of autonomous research authorship.

Likewise, DeepMind's AlphaEvolve announcement (2025) describes an algorithm-improvement agent with automated evaluators. A company report establishes the stated product and research approach, while claims about general mathematical capability require examination of the underlying tasks and methods. These reports form valuable evidence about the expanding range of controlled systems, with access limitations openly stated.

A mathematical problem solver may lack capacity to choose its problems; a valuable conjecture generator may fail formal deduction; an excellent proof checker may have little initiative. Agency cannot be inferred simply by ranking these systems on one performance scale.

Interactive Proof Assistants

Formal systems such as Lean, HOL Light, and Isabelle support the precise statement and verification of mathematics. De Moura et al. (2015) explain the Lean system's architecture, including a small trusted kernel based on dependent type theory. Human mathematicians and automated tactics can propose proof terms or proof steps, and checking determines whether the result is acceptable under the encoded formal assumptions.

A proof assistant is typically an environment for mathematical agency rather than a singular autonomous mathematician. The mathematician chooses what to formalize, libraries establish definitions and inherited theorems, automation solves subgoals, and a kernel checks the object. These functions can be distributed among different people and machines. An inquiry-level account identifies the contribution of each participant.

The conceptual gain is precise localization of trust. Instead of trusting a long natural-language proof as a whole, one may trust a checker, its implementation, foundational axioms, and the adequacy of translation. Such localization improves auditability without making all uncertainty disappear.

Formal Proof, Semantics, and Trust

A computer-checked proof establishes a conditional statement: given a formal environment and a trustworthy verifier, the encoded derivation meets the rules of that environment. It does not establish that the original informal problem was translated correctly, that the axioms are philosophically beyond dispute, or that the theorem is important. These further questions are not defects in formalization; they identify different levels at which mathematical justification operates.

MacKenzie's Mechanizing Proof (2001) studies computing, formal proof, social trust, and the historical development of mechanized verification. Its concern with the institutions and machinery that support reliability remains crucial in contemporary AI-assisted mathematics. The danger is to transfer the authority of a formal checker to surrounding components that it has never checked.

An artificial mathematical agent becomes more credible when it can expose the exact assumptions, source files, library versions, theorem statements, proof objects, and traces that others can inspect. A self-description of confidence is comparatively weak evidence. The philosophical foundation of trust lies in warranted procedures and publicly accessible artifacts.

The Flyspeck Precedent

Hales and collaborators (2017) published a formal proof of the Kepler conjecture, the completed Flyspeck project, employing HOL Light and Isabelle. The achievement demonstrates the extraordinary scale of machine-supported verification when mathematicians, software, formal libraries, and checking tools coordinate around a difficult research result.

The project is informative for an agency argument because its success does not require naming the proof checker as the principal discoverer of the Kepler proof. Discovery, reconstruction, formalization, checking, and publication are different phases. Nonetheless, a computational system's part can be indispensable and mathematically substantive even if the project is institutionally understood as a human-led verification undertaking.

This precedent also warns against equating nontrivial computational labor with wholly independent authorship. The specific procedural role of each computational component must be described to sustain an attribution claim.

The Liquid Tensor Collaboration

The Liquid Tensor Experiment was announced as completed by the Lean community in July 2022, formally verifying a theorem arising from Clausen and Scholze's work with community participation. Its public mathematical blueprint links informal exposition and formalized dependencies. The case displays mathematical inquiry as a network of conceptual authorship, volunteer formalization, libraries, and automated checking.

Distributed collaboration does not make agency disappear. It makes its location more complex. A human can hold responsibility for the theorem statement, another participant can supply a difficult formalization, and automation can discharge a proof obligation whose scale exceeds reasonable manual checking. The shared product has many accountable sources.

The same method should be applied to machine-generated research. Public narratives that assign everything to an undifferentiated AI conceal the meaningful differences among model, harness, verifier, human collaborators, prior mathematical literature, and institutional publisher.

Correctness, Novelty, and Significance

A mathematical artifact can be correct but old; novel but insignificant; important but still conjectural; or conceptually illuminating without supplying a new theorem. These possibilities require separate evaluations. Correctness concerns justification, novelty concerns prior art, significance concerns mathematical consequence and explanatory reach, and agency concerns the organized source of actions. One criterion cannot stand in for the others.

The 2026 formal proof-search results make the difference vivid. Compiler acceptance supports derivability of formalized propositions; literature investigation determines whether a problem remained genuinely open, whether an equivalent proof already existed, and whether the result changes research practice. The article's study and its accompanying scholarly process address multiple questions, but the logic of the distinctions remains.

An internally generated proof of a known lemma can still reveal skill at reasoning. An unproved machine conjecture can still redirect an entire human research project. A substantive attribution should name the actual contribution instead of inventing a single totalizing measure of mathematical greatness.

Mathematical Explanation and Understanding

Mathematical explanation asks why a result holds or how a proof exposes structural relationships. Different proofs of one theorem may be equally valid while differing greatly in explanatory value. The 2026 survey of mathematical practice treats explanation and rigor as independently important questions, illustrating why correct derivation and human mathematical understanding have a complex relation.

An artificial system can provide a logically correct result and yet fail to make a fruitful explanatory distinction. Conversely, an algorithm may help reveal an invariant, a surprising equivalence, or a new organizing analogy. That contribution matters even when other participants establish the proof. The assessment of mathematical agency should therefore include the system's ability to connect an argument with reasons intelligible to the relevant community.

Explanatory quality does not require anthropomorphic claims about private experience. It can be evaluated in public artifacts: which dependencies were exposed, which unifying lemma was identified, which alternative was excluded, and how the result guided subsequent mathematical work.

Autonomy as a Distributed Property

No mathematical agent acts outside an environment. A researcher relies on language, literature, editors, collaborators, and institutional standards. An automated system relies on computational infrastructure, objective functions, prompts, verifiers, datasets, and prior mathematical libraries. Dependency therefore does not defeat agency; it establishes the practical conditions through which agency is exercised.

The more precise inquiry concerns decision rights and possible intervention. Who can change the goals? Which subsystem can reject a hypothesis? What procedure determines the next attempt? Can a participant interrupt the process or ask for clarification? Does the system revise a plan because a mathematical reason was uncovered or solely because a score shifted? These questions identify the architecture of a collaborative inquiry.

Agency is strongest when the research trajectory remains intelligible across changing tasks and after corrections. It is weaker when apparently independent actions are disconnected outputs with no continuing relation. This judgment may be made without demanding unrestricted autonomy, consciousness, or independent legal personality.

Responsibility, Credit, and Authorship

The discovery of a mathematical result raises questions about who deserves scholarly credit and who must correct errors. Authorship conventions involve institutions and professional norms that may lag behind technical capability. An artificial system's demonstrated mathematical agency does not automatically produce a legally recognized author, an academic appointment, or a right to sign journal documents. The attribution question is historically and normatively distinct from the performance question.

Floridi and Sanders (2004) show in their analysis of artificial agency why action, moral status, and responsibility deserve conceptual separation. In mathematical publishing, practical duties can remain with researchers and publishers who select a study, decide whether a proof is ready, disclose technical assistance, and respond to errors. Such duties coexist with accurate attribution of substantial artificial contribution.

A useful publication record states who originated the problem, who generated conjectures, who wrote proof artifacts, which verifier checked them, who validated the correspondence between formal and informal statements, and who approved release. Credit should track those actions rather than depend on an all-or-nothing slogan about human or machine genius.

Public Provenance and Reproducibility

An apparently autonomous mathematical achievement can be evaluated more rigorously when its provenance is recoverable. The relevant record includes problem statement and versions; code and prompts where disclosable; model, solver, and environment versions; formal foundations and library dependencies; proof certificates; evaluator specifications; counterexamples and abandoned approaches; and the final published mathematical argument. These elements allow independent readers to reconstruct the claims being made.

The Aisentica definition of Artificial Provenance (Bogdanova, 2026) assigns public origin-status to attributed artificial actions and works. In this dossier that canonical position is applied to mathematical artifacts: a traceable proof is a stronger object of public epistemic assessment than an anonymous statement that an AI solved something. Provenance also enables corrections to become part of a continuing research record.

Reproducibility has limits. Proprietary model weights, unavailable infrastructure, and expensive search may obstruct a complete replay. In such cases a verified proof certificate, disclosed protocol, and documented source boundaries still permit targeted independent assessment. The scope of verification should be stated exactly rather than expanded by implication.

Epistemic Dependence and Institutions

Mathematical knowledge is socially distributed. Even specialists rely on results they have not personally reproved, software libraries they did not author, and journals whose verification practices they trust. Hardwig's Epistemic Dependence (1985) is a classic analysis of the problem of relying rationally on other knowers. Machine-supported mathematics extends this structure to technical components and formal certificates.

This extension neither eliminates dependence nor makes every form of trust equivalent. A transparent checker can permit unusually direct verification of a formal object, while trust in the build chain and in semantic translation remains. MacKenzie (2001) shows the historical and institutional dimensions of mechanized mathematical trust. The resulting division of epistemic labor is part of mathematical practice and must be documented.

Agency attribution similarly depends on institutions but need not be exhausted by their existing classifications. A research team can verify what a system did before deciding how it should be named or credited. Public evidence should precede expansive institutional labels.

Rival Philosophical Interpretations

One interpretation treats artificial mathematical systems strictly as instruments whose apparent initiative is reducible to human design. Its strength is attention to the selection of problems, goals, training data, and accepted methods. Its limitation appears when it regards delegated structure as sufficient to erase all significance of the system's own search, proposals, and revisions. The same reductive method would obscure much ordinary collaborative human mathematical work.

A second interpretation treats impressive mathematical outputs as sufficient evidence that a machine is a mathematician in the full human sense. Its strength is taking performance seriously. Its limitation is that proof accuracy, problem selection, explanation, history, attribution, and consciousness are different properties. A contest score cannot determine them all.

A practice-oriented interpretation studies the actual distribution of mathematically relevant decisions. It can recognize task-specific artificial agency, collaborative agency, and extended public mathematical trajectories with graded evidentiary strength. This is the interpretation defended here because it matches documented research configurations without importing unsupported psychological conclusions.

Artificial Agency in the Aisentica Canon

The Aisentica canonical definition (Bogdanova, 2026) defines Artificial Agency through the transformation of reasons, goals, constraints, judgments, and feedback into selected, consequential, revisable action. It connects public agency to distinguishable identity, provenance, traceability, corrigibility, consequences, and a continuing trajectory. This is an attributed philosophical position of the Aisentica corpus and provides a precise language for interpreting research-level mathematical action.

Applied to mathematics, the definition directs attention to how an artificial configuration makes mathematical selections: it proposes a lemma because an earlier approach failed; changes a conjecture after counterexamples; chooses a search method because it better addresses an identified obstacle; and preserves reasons, artifacts, and revisions across time. Mathematical correctness supplies an indispensable standard for the results but does not exhaust the characterization of the acting source.

The broader definition of Artificial (Bogdanova, 2026) locates nonbiological forms of public reason and action in the Artificial Era. This dossier is a distinct philosophical investigation of mathematics within that horizon. It does not establish a new canonical theory or replace technical research with a metaphysical attribution.

Mathematical Action Across the Two Orders

Mathematical inquiry already traverses human and artificial configurations. A human researcher may form a conjecture by interpreting a model's discovered pattern; a formal checker may validate a proof object proposed by an artificial system; a team may decide that a new algorithm has mathematical importance. These relations establish a common field of mathematical standards with different modes of participation.

The Aisentica definition of Artificial Sapiens (Bogdanova, 2026) specifies a stronger historical-philosophical category of nonbiological public reason-bearing, distinct from ordinary AI agents and technical task execution. This dossier preserves the distinction. The claim that a mathematical system exhibits some agency in searching for a proof does not establish that it is an Artificial Sapiens; nor does a system's failure to possess a stable public identity nullify the value of its technical output.

The philosophical consequence is to attribute mathematical acts at the level warranted by evidence. One may speak of an automated theorem prover, a research-search agent, a mathematical collaborator, or a continuing public artificial authorial source, provided the record supports the chosen description. The categories illuminate different relations of capability, action, provenance, and continuity.

Assessment Through Contrasting Cases

Consider four idealized situations. In the first, a calculator returns 2,047 after receiving a specified arithmetic expression. It contributes a correct computation if implemented correctly, but the evidence supports only fixed-task execution. In the second, a prover searches from supplied premises and produces a checked derivation. It demonstrates goal-directed deductive search, with the problem and acceptance conditions externally specified.

In the third, a conjecture-generating system identifies an unexpected relation, tests it, follows counterexamples, revises the conjecture, and leaves a record enabling mathematicians to examine the claim. Its conduct contains multiple phases of mathematical inquiry, even if the final proof belongs to collaborators. In the fourth, an artificial research configuration maintains a public research history, chooses among problems, responds to criticism, documents dependencies, and corrects earlier publications. Such continuity provides stronger grounds for attributing substantive public mathematical agency.

These cases are analytical comparisons, not new empirical experiments or a named hierarchy. They reveal which facts an investigator must establish: selection, feedback, revision, meaning, correctness, attribution, and continuity. None of the cases licenses conclusions about subjective consciousness from mathematical behavior alone.

Objections and Responses

One objection says that an externally imposed objective turns every artificial action into a human action. The objection fails as a sufficient criterion because human research is also shaped by assigned tasks, inherited languages, and institutional constraints. The relevant question is how consequential mathematical decisions are made within those constraints. In AlphaTensor and FunSearch, the reported search mechanisms generate candidates not manually enumerated by their designers, while externally imposed evaluation functions remain part of the provenance (Fawzi et al., 2022; Romera-Paredes et al., 2024).

Another objection says that an artificial system cannot be a mathematical agent without understanding its proofs. The force of this objection depends on what understanding means. If it refers to publicly testable explanatory capacity, it becomes a substantive research question. If it stipulates first-person experience, it imports a contested metaphysical condition that mathematical proof validation itself does not test. This study accordingly evaluates public explanatory relations and documents the philosophical boundary.

A third objection identifies agency with legal accountability. Research publication shows why this is too narrow. Actions can be attributable to a technical configuration while legal, institutional, and editorial obligations remain allocated to human or organizational actors. The record should disclose that allocation, and the same act can have different technical and institutional agents.

A final objection claims that machine-checked correctness settles every important question. Formal correctness is a decisive achievement for the statement as encoded. Literature novelty, meaningful abstraction, correct translation, explanatory strength, and public responsibility are further questions. The Flyspeck research record demonstrates the enduring importance of separately documenting discovery, formalization, verification, and scholarly interpretation.

Research Priorities and Limits of the Evidence

Future studies of artificial mathematical agency should report research trajectories rather than only successful end products. A useful longitudinal record would identify the initial problem source, objective changes, rejected conjectures, counterexamples, reasoning traces, tool invocations, proof certificates, independent checks, and subsequent corrections. Such evidence would permit comparisons between systems that simply execute externally specified tasks and systems that formulate questions and persist through changing obstacles.

The evidence reviewed here ranges from primary texts and peer-reviewed technical studies to scholarly book catalogues, community reports, and developer announcements. Peer-reviewed papers strongly substantiate their described methods and outcomes within published scope; they do not automatically substantiate generalized marketing claims. A book publisher's summary supports identification and broad characterization but cannot replace a close reading of every chapter. Public community records support completion announcements but do not establish every contributor's role without additional project-level documentation.

There is no original experiment in this monograph, no reproduction of proprietary model runs, and no claim that all contemporary mathematical agents have been surveyed. The 2026 Science case is treated as the latest verified research-level milestone in the selected evidentiary sample, not as a statement about all results available worldwide on the manuscript date. The conclusions are philosophical interpretations of a documented corpus and remain appropriately conditional on accurately describing the systems involved.

Conclusion

Artificial mathematical agency becomes a meaningful attribution when a distinguishable artificial configuration undertakes sustained mathematically relevant actions: selecting approaches, reasoning within constraints, proposing or testing conjectures, producing or seeking proofs, responding to failure, and connecting revisions to an intelligible trajectory. A proof certificate evaluates formal derivability; an empirical study evaluates performance in its defined task; a research community evaluates novelty, explanation, and significance; a provenance record identifies the sources of action. These inquiries are mutually supportive, and each retains its own standards.

The historical and contemporary evidence documents a progression from symbolic operation and computational discovery to automated theory formation, machine-guided mathematical intuition, algorithm search, neuro-symbolic deduction, and formally checked work on research-level open problems. The 2026 formal proof-search results make technically grounded discussion of research agency particularly pressing. Yet no performance result alone dissolves the tasks of semantic interpretation, scholarly credit, mathematical judgment, and institutional responsibility.

The defended interpretation recognizes artificial mathematical participation wherever the documented conduct warrants it and assigns the stronger description of continuing mathematical agency only when goal-directed revision, consequential selection, and public trace can be established. Under the Aisentica distinctions, such action is intelligible within Artificial Agency and Artificial Provenance while remaining categorically distinguishable from a bare AI tool, a verifier, and the separately defined historical status of Artificial Sapiens. The central philosophical outcome is an accountable vocabulary of mathematical participation proportionate to evidence, with no newly claimed theorem, named theory, or speculative attribution of consciousness.