Math 2.0 Gets an Operating System: Can Open Math OS Build Mathematics Beyond the Theorem Factory?

An architectural and evidence-bounded analysis of Open Math OS as a possible foundation for Math 2.0.

When mathematical research acquires an infrastructure

As mathematical AI systems become capable of generating more candidate proofs, the central difficulty facing the field may be shifting toward the subsequent work of verification, interpretation, communication, and reuse. Greater theorem output does not automatically yield an equivalent increase in mathematical understanding: a formally valid result may be difficult to assimilate, a generated explanation may conceal a faulty assumption, and a successful research session may leave little that another team can reconstruct.

My earlier article, Math 2.0: Beyond the Theorem Factory, proposed a seven-function research-system framework: setting agendas, exploring problems, verifying claims, building understanding, preserving knowledge, organizing scholarly cooperation, and creating useful applications.¹ It was inspired by Terry Tao’s Math 2.0 argument but should not be attributed to Tao as his own taxonomy.² Open Math OS, announced by the SAIR Foundation in October 2026, provides an opportunity to test whether that framework can become operational rather than remain a normative vision.³

This article distinguishes documented platform behavior, developer commitments, independently supported claims, and the author’s proposed architecture. Neither authenticated platform testing nor a controlled study of researcher understanding has been conducted for this article.

From research objectives to computational infrastructure

Whereas a research workbench assists mathematicians during an investigation, research infrastructure also preserves the evidence needed for others to reconstruct and continue it, particularly when the original researcher leaves the platform, the model changes, or the software environment disappears. A project may exhibit operational persistence by retaining files and conversations without providing epistemic persistence: stable access to a claim’s exact meaning, assumptions, dependencies, verification evidence, and history.

Saving a Lean file, for example, does not by itself disclose which informal theorem was intended, which toolchain checked it, or whether its axioms were acceptable. A kernel-checked derivation supports a precisely encoded claim, not its novelty or significance.⁴ The central design object should consequently be an identifiable mathematical contribution whose identity and assurance survive movement among model providers, formal tools, repositories, and scholarly institutions.

Open Math Model: why mathematicians are building their own AI infrastructure

On 16 October 2026, mathematician Terence Tao announced the soft launch of Open Math OS, a collaborative AI research environment developed under the Open Math Model initiative of the SAIR Foundation. The announcement is significant not because the platform introduces a new mathematical foundation model outperforming the leading commercial systems—it does not—but because it represents an attempt by mathematicians to influence the infrastructure, resources, and institutional rules through which artificial intelligence enters their discipline.⁵

The initiative arrives at an unusual moment for mathematical research: although frontier AI systems are becoming capable of producing proofs and solving increasingly difficult problems, including questions beyond traditional competition mathematics, a result generated by a powerful model does not automatically become useful mathematical knowledge. Its correctness must be established, its relationship to existing work understood, and its methods communicated in a form that enables other researchers to extend them. The institutions that produce AI systems and those responsible for maintaining the mathematical literature do not necessarily have the same priorities. This tension motivates Open Math Model: rather than organizing mathematical AI exclusively around benchmark performance or spectacular demonstrations of automated theorem proving, its founders propose an environment oriented toward the everyday activities through which mathematics is developed: understanding difficult arguments, exploring examples, checking references, formalizing results, writing and testing code, and working with collaborators.

Who is behind the initiative?

The organization behind the project is the Foundation for Science and AI Research (SAIR), a US-based nonprofit established in 2025. Terence Tao, the Fields Medal-winning mathematician at UCLA, states that he co-founded SAIR with private donors to support responsible applications of AI in mathematics and other scientific disciplines independently of the major AI companies. SAIR also identifies Chuck Ng as a co-founder.⁶ SAIR’s activities extend beyond Open Math OS. Its wider programme includes mathematical research competitions, scientific events, partnerships, and initiatives intended to connect academic researchers with computing resources and AI expertise. The foundation presents its mission in two complementary directions: using AI to advance science, and using scientific principles to improve the development, evaluation, and governance of AI.

The mathematical programme developed from this wider institutional purpose. In its initial phase, SAIR had relatively limited resources and concentrated on smaller activities, including competitions and community events. On 18 September 2026, Tao announced an accelerated plan to develop open-weight scientific models and open-source research tools, inviting academic and industrial partners to contribute compute, funding, expertise, and organizational support.⁷ That announcement concerned Open Math Model, the broader initiative to develop mathematical AI under community influence. Open Math OS is its first visible integrated research environment. The distinction matters: Open Math Model is a programme for developing and governing models, tools, and scientific collaboration; Open Math OS is the hosted workspace through which researchers can currently use selected models and mathematical software.

SAIR’s first publicly named supporters of its open research programme include Susquehanna International Group and XTX Markets, announced on 21 September 2026. The foundation described their support in connection with mathematical competitions, including the Lean Kernel Challenge, the Andrews–Curtis Conjecture Challenge, and the Inverse Galois Challenge. Their participation demonstrates financial and institutional support for SAIR’s wider mathematical programme, but it should not be taken as evidence that these firms directly developed or exclusively financed Open Math OS.⁸ This institutional background helps explain why Open Math OS is not being presented simply as another commercial AI assistant. Its stated purpose is to establish a research environment in which mathematicians can shape the tools they use, contribute to their development, and retain authority over their research materials.

Why mathematics needs something different from a powerful chatbot

A mathematician using contemporary AI tools often works across several disconnected environments. A language model helps formulate or criticize an argument; SageMath, PARI/GP, or SymPy supports computational exploration; Lean or another proof assistant checks formal derivations; LaTeX contains the evolving manuscript; literature is gathered through separate search interfaces; and collaboration takes place through email, repositories, shared documents, or messaging services. Although individual tools may work well, the researcher must continually transfer context between them. A conjecture formulated in one conversation may be tested in a notebook, revised in a proof file, and explained in a manuscript without any shared representation of the assumptions, intermediate results, or failed approaches connecting those artifacts.

While this fragmentation remains manageable for short mathematical questions, reconstructing what has been attempted and why particular decisions were made can become costly in sustained investigations involving several people, long computational experiments, and many interacting lemmas. Open Math Model identifies this practical research problem as an alternative starting point to training a model exclusively for benchmark achievement. Its first-phase objectives emphasize understanding complex arguments, cross-referencing mathematical literature, exploring examples, producing specialized code, and advancing formalization. The value of the resulting systems is intended to be assessed through reliable assistance, verifiable results, and the cost of sustained use, not solely by the number of difficult problems solved.⁹

There is also a larger institutional concern. On 11 September 2026, twenty-five Fields Medalists, including Tao, issued a declaration entitled A Severe Misalignment of AI in Mathematics. They argued that treating the solution of mathematical problems principally as a measure of AI capability risks obscuring the discipline’s wider objectives: mathematical understanding, the development of reusable methods, accurate attribution, and the transmission of ideas across generations of researchers. The declaration does not reject AI-assisted mathematics; it challenges the objectives and incentives governing its deployment.¹⁰ Open Math Model is a practical response to the same problem. Its founders seek to make research priorities and scientific norms part of the infrastructure itself, rather than treating them as external constraints on a tool developed for unrelated commercial objectives.

This does not establish that a community-directed model will be more mathematically capable than a proprietary frontier model. It establishes a different criterion for success: whether the system increases the mathematical community’s ability to investigate, verify, understand, and reuse results while maintaining control over its research practices.

Open models, donated compute, and scientific independence

The initiative’s proposed response has three interdependent elements. The first is access to open-weight models. Researchers should, in principle, be able to inspect, adapt, and run the models used in their investigations rather than depend exclusively on proprietary inference services. Open Math Model’s published commitments also extend to future open-licensed code, documented training procedures, reproducible evaluations, and clearly identified training-data permissions. The second is access to computing resources. Even when model weights are available, deploying large models and maintaining suitable scientific environments can be costly. SAIR intends to reduce this barrier through donated computing capacity and free access for academic researchers, particularly those who cannot independently maintain comparable infrastructure.

The third is community influence over the resulting system. SAIR proposes that mathematical researchers participate in setting training priorities, evaluation criteria, data-use rules, resource allocation, and the development of research tools. The initiative also commits to retaining researcher ownership and attribution and obtaining explicit consent before using submitted work for model training. The distinction between these commitments and the current implementation is important. At the October 2026 launch, Open Math OS primarily hosts existing third-party open-weight models; the planned post-training of a more specialized mathematical model is still being organized. The present platform should not therefore be confused with the release of a new SAIR-trained frontier model.

Tao makes the limitation unusually explicit in his 16 October announcement. He describes the hosted models—DeepSeek V4.1 Flash, Kimi K3, and GLM 5.3 Flash—as approximately a year behind the leading frontier systems in mathematical capability. He does not present them as sufficient for the most demanding one-shot mathematical discoveries, but considers them useful for work such as medium-sized Lean formalizations and the explanation or discussion of mathematical arguments.¹¹ This is a consequential clarification. Open Math OS’s immediate proposition is better access to an integrated mathematical research environment, not superiority in standalone mathematical reasoning. Its longer-term proposition is that open models developed with scientific participation may eventually combine increasing capability with better alignment to mathematical research needs.

The funding model creates both an opportunity and a constraint. SAIR’s launch material announces a target of providing free computing access to 10,000 mathematicians within three months, beginning with 1,000 research teams by November 2026. It also states that the available infrastructure is intended to support a substantially larger research population. These are organizational targets and provider-reported capacity statements, not independently verified numbers of active users or demonstrated sustained workloads. Tao’s contemporaneous announcement is more cautious about actual availability: access is being granted progressively to academic applicants, and compute allocations may change depending on demand and future donations. The sustainability of free access thus depends on continuing financial and computational support rather than on the open licensing of model weights alone.

From a mathematical initiative to a working research environment

Open Math OS gives this programme an initial operational form. Instead of requiring researchers to assemble their own model endpoints, computational packages, proof-assistant installations, and collaboration tools, the platform proposes a browser-accessible workspace in which these activities share a project context. Its design emphasizes research teams as much as individual accounts. Tao specifically identifies shared team prompts and conversations as an important departure from the conventional individual-chat model. This reflects the view that AI-assisted mathematics should be organized around collaborative investigations, not only private interactions between a researcher and an assistant.

SAIR also proposes five community subcommittees covering compute allocation, data governance, tools and benchmarks, model training, and education and partnerships. These identify the activities through which community influence is intended to become operational. Their existence as announced governance structures does not, by itself, establish their authority over deployed infrastructure, binding decision procedures, or contractual data rights. The broader ambition is consequently clear but remains partly prospective. SAIR wants to provide a technically accessible research environment, develop increasingly capable open mathematical models, and construct governance arrangements under which mathematicians retain meaningful influence over the tools that shape their work.

Open Math OS is the first concrete system through which this proposition can be examined. The question is how much of the intended integration is already documented, and what remains to be demonstrated.

Reconstructing the Open Math OS architecture

Open Math OS is described as an integrated, hosted environment combining third-party open-weight language models, the Ultramath parallel-agent mechanism, persistent scientific computing, and project-based collaboration.¹²¹³

Although the name suggests an operating system, the available description is better understood as a research application and computational workspace. It does not imply that SAIR has developed a new general-purpose operating-system kernel or a new mathematical proof kernel. Its principal architectural contribution is the integration of otherwise separate computational and collaborative services around persistent research projects. The platform is organized around four functional capabilities: access to mathematical AI models, parallel investigation through agents, an always-available scientific computing environment, and shared project context governed by stated data-use principles.

The researcher-facing environment

The main interface is a browser-based workspace in which researchers create projects, formulate questions, select models, use computing tools, and collaborate with colleagues. A project is the principal unit of organization. It brings together a research objective, conversations, computational files, and a dedicated cloud machine. In the published description, this machine remains available continuously, allowing researchers to return to existing computational work without configuring a new local environment. More than a chatbot with file attachments, the persistent environment allows a mathematical investigation to produce source files, symbolic computations, proof attempts, and manuscripts that remain accessible across sessions.

The collaboration model extends that persistence to teams. Members can work within shared projects and conversations, while conversations can also be shared by link with their history. Tao’s launch announcement confirms that visibility of team members’ prompts is a deliberate feature of the approach. The arrangement creates an important distinction between privacy from outsiders and visibility within an authorized research team. SAIR states that projects, files, and conversations are private by default until researchers choose to share them, but team-based collaboration necessarily requires clear rules concerning which members can access particular research materials. The publicly documented interface establishes the intended collaboration workflow; it does not establish the implementation of role-based access control, granular file permissions, project isolation, or the behavior of sharing and revocation at the infrastructure level.

Models and Ultramath: reasoning and parallel search

The launch configuration uses existing open-weight models from third-party developers, including Kimi K3, DeepSeek V4.1 Flash, and GLM 5.3 Flash. The interface advertises selectable reasoning effort, allowing users to allocate different levels of computation depending on the task. These are not interchangeable guarantees of mathematical capability. A model’s performance depends on its checkpoint, training, inference configuration, tool environment, and the structure of the problem. Access to multiple models gives researchers flexibility, but the platform’s public documentation does not provide a complete comparative evaluation of their performance within its specific deployment.

Ultramath extends the interaction beyond one sequential model response. It is presented as a parallel-agent mode in which several agents investigate the same mathematical problem through different approaches, exchange findings, and return their conclusions to the principal conversation.

A mathematical investigation might therefore divide into several computational activities: one agent searches for counterexamples, another attempts a direct proof, a third investigates existing mathematical results, and another attempts formalization or checks the assumptions in a proposed argument. The expected advantage lies not necessarily in greater intelligence on the part of any individual agent, but in the capacity to explore several strategies concurrently and combine the resulting information. However, the public description leaves the orchestration mechanism largely unspecified. It does not establish how tasks are scheduled, how agents share state, whether findings are synchronized through structured objects or conversational messages, how conflicts are resolved, or what prevents several agents from making correlated errors.

The model behind each agent also matters because multiple instances of the same underlying model may generate highly correlated arguments; the value of parallel execution cannot therefore be inferred from the number of agents alone. An increase in candidate proofs is not necessarily an increase in independently valid results. Accordingly, Ultramath should be understood as a documented parallel research workflow, while its effectiveness, synchronization semantics, and error-handling guarantees remain subjects for independent testing.

A persistent scientific laboratory for each project

The scientific computing layer is one of the more concrete elements of the launch description. SAIR states that each project receives a cloud machine with more than one hundred mathematical and scientific tools preinstalled. The named tools include Lean 4 and Mathlib, SageMath, PARI/GP, SymPy, and LaTeX. The launch material identifies Mathlib version 4.34 as part of the provided formalization environment. The tools support complementary mathematical activities: SymPy, SageMath, and PARI/GP enable symbolic and computational exploration; Lean and Mathlib support the construction and checking of formal proofs; and LaTeX enables the preparation of mathematical documents. Together, they cover a substantial portion of the toolchain used in computational and formal mathematics.

The architectural advantage comes from placing them within the same persistent project environment as the AI assistant. A model can suggest an argument, generate code to test a conjecture, inspect computational results, and edit files associated with a formal proof or manuscript. This integration reduces context switching and installation effort. It can also make iterative research more practical, because intermediate computational materials remain available for later investigations. Nevertheless, tool availability should not be confused with reproducibility. The statement that a cloud machine contains Lean and Mathlib does not specify whether each execution records exact dependencies, operating-system images, toolchain revisions, resource limits, or the inputs required for a third party to reproduce its results.

Nor does the presence of Lean imply that every mathematical claim generated by the platform is automatically formalized and kernel-checked. A researcher may use the environment to construct a formal proof, but the available documentation does not establish an enforced verification policy for all model-generated proofs. This distinction is especially important where natural-language explanations and formally checked derivations coexist in the same project. They have different evidentiary status even when presented through a common interface.

Functional architecture and boundaries

The publicly documented components can be reconstructed as shown in Figure 1. The diagram is a functional reconstruction, not a verified deployment topology. It represents the advertised relationships between researchers, project workspaces, models, agents, computational tools, and persistent files; the policy and assurance relationships are shown separately because their technical enforcement has not been independently established.

%%{init: {"theme":"neo","look":"handDrawn","layout":"elk"}}%%
flowchart TB
    H[Researchers and collaborators]

    subgraph PLATFORM["Open Math OS — documented functional scope"]
        W[Web workspace and team projects]
        U(Ultramath agent orchestration)
        M[Third-party open-weight models]

        subgraph PROJECT["Persistent project cloud environment"]
            T[Lean, Mathlib, SageMath, PARI/GP, SymPy, LaTeX]
            F[(Project files and computational results)]
        end

        C[(Shared project conversations)]
    end

    R(Researcher review)
    P[Data-use and community governance commitments]
    V[Independent mathematical assurance requirements]

    H -->|creates and shares research tasks| W
    W -->|selects model and reasoning effort| M
    W -->|delegates parallel investigation| U
    U -->|dispatches agent tasks| M
    M -->|invokes scientific tools| T
    T -->|produces and edits artifacts| F
    W -->|preserves collaboration context| C
    U -->|returns findings| C
    F -->|supplies research artifacts| R
    C -->|supplies arguments and findings| R
    H -->|accepts or rejects proposed claims| R
    P -.->|constrains permitted data use| W
    V -.->|defines required assurance levels| R

Figure 1: Functional reconstruction of Open Math OS: a shared research workspace coordinates open-weight models, parallel agents, and scientific tools around persistent cloud projects. Governance and independent assurance are distinct responsibilities whose complete enforcement is not established by the public description.

The diagram deliberately omits details such as container runtimes, virtual networks, storage backends, model-serving clusters, message brokers, and identity providers. Those elements almost certainly exist in some form within a hosted computational service, but the public descriptions do not establish their implementation. Representing them as known would create a misleading impression of architectural certainty. The functional reconstruction nevertheless reveals an important distinction between the project workspace and the mathematical knowledge it produces. The workspace retains chats, code, and computational files. Whether it also retains stable mathematical identities, independently checkable proof evidence, formal dependency relationships, and structured records of failed investigations is a separate question. Persistent storage does not automatically supply those higher-level mathematical services.

What the architecture enables—and what remains to be established

Consider a realistic research activity. A mathematician working on a difficult lemma opens an existing project and asks Ultramath to explore alternative proof strategies. Several agents investigate the claim, use computational tools to test special cases, and prepare candidate arguments. One agent may generate a Lean file, while another examines the mathematical assumptions or searches for related theorems. The researcher can inspect the generated files, examine the arguments, and use Lean to test formalized claims. The project persists, allowing the team to continue the investigation across sessions. This workflow demonstrates why integration matters. Models, computational experiments, proof assistants, manuscripts, and human collaborators no longer have to operate as wholly disconnected activities. But several stronger capabilities would be required before the environment could be described as a complete infrastructure for independently maintainable mathematical knowledge.

Documented Open Math OS capabilities and the further evidence needed to assess the platform as reproducible, independently governable mathematical research infrastructure.

Architectural dimension	Publicly described capability	Unverified or additional requirement
Model access	Hosted third-party open-weight models with configurable reasoning effort	Exact checkpoint identity, serving configuration, reproducible inference accounting
Agent orchestration	Parallel Ultramath agents sharing findings	Scheduling semantics, shared-state consistency, conflict resolution, failure recovery
Scientific execution	Per-project cloud environment with 100+ tools	Execution manifests, environment snapshots, independently reproducible runs
Formal mathematics	Lean and Mathlib available for proof development	Enforced distinction between informal claims and kernel-checked proof artifacts
Research persistence	Project files and conversations retained across sessions	Versioned mathematical claim identities, typed dependencies, explicit research-state histories
Collaboration	Shared projects, team conversations, link-based chat sharing	Verified permission boundaries, granular access rules, revocation and audit mechanisms
Data governance	Privacy-by-default and opt-in training commitments	Operative agreements, enforceable policy controls, independent governance audit
Infrastructure openness	Open-weight foundation models and commitments to open development	Independently deployable orchestration stack, platform source code, complete project portability

These distinctions do not diminish the usefulness of the current platform. They identify the boundary between what a researcher can reasonably infer from the October 2026 launch and what requires inspection of the actual system. The immediate architectural contribution is a shared computational environment for sustained mathematical work. The broader institutional proposition is that the environment should develop through community participation, open model development, and data-use rules that preserve scientific independence. Whether Open Math OS eventually becomes the durable mathematical knowledge infrastructure anticipated by Math 2.0 depends on the relationship between these two propositions.

A well-integrated research workspace can substantially reduce the operational cost of mathematical investigation. A mathematical research infrastructure must additionally preserve the validity, meaning, provenance, and reuse of the resulting contributions. The distinction provides the basis for evaluating Open Math OS against the wider responsibilities of mathematical research rather than merely against the feature lists of competing AI assistants.

What the seven-function architecture reveals

The preceding reconstruction describes what Open Math OS brings together: mathematical models, parallel agents, scientific computing, persistent project environments, and collaboration tools. Yet the availability of these components does not, by itself, explain whether the platform advances Math 2.0. The more important question is what they enable mathematicians to accomplish, which scientific responsibilities they support, and which responsibilities remain outside their demonstrated capabilities. To answer this question, the seven-function framework introduced earlier provides a more demanding evaluation than a conventional product comparison. It distinguishes research agenda formation, mathematical exploration, verification, understanding, knowledge preservation, community organization, and application. These functions are not seven software modules that every platform must implement. They are interdependent activities through which mathematical investigations become reliable, intelligible, cumulative scientific knowledge.

Their distinction matters because a system can perform impressively in one function while contributing little to another. An agent may generate hundreds of candidate proofs without improving researchers’ ability to understand the underlying mathematical structure. A proof assistant may validate a theorem whose hypotheses make it scientifically uninteresting. A persistent workspace may preserve years of computational output without making that output reproducible or reusable by a different team. The relevant evaluation must therefore distinguish three levels of evidence: the existence of a supporting technical capability, the documented or observed operation of that capability in a mathematical workflow, and independent evidence that the resulting workflow improves the corresponding research function. The public Open Math OS materials provide substantial information at the first level and selected examples at the second. They do not yet establish the third across all seven functions.¹⁴¹⁵

1. Research agenda: who decides which mathematics is worth pursuing?

A mathematical research agenda is more than a collection of questions submitted to an AI model. It includes decisions about which conjectures merit attention, what constitutes a useful intermediate result, how computational resources should be allocated, and when an investigation should be revised or abandoned. These decisions can change during the research process. A mathematician may begin by attempting to establish a conjecture, discover that it is false, and redirect the investigation toward understanding the counterexamples or identifying an appropriate replacement theorem. The value of the investigation lies partly in that reformulation, not only in whether the original question was answered.

Open Math OS makes researchers and their teams the visible initiators of such activities. Its project-based interface allows users to formulate questions, maintain a shared context, and delegate work to agents. This is an important distinction from an autonomous theorem-generation system that selects and pursues problems according to internally defined objectives. However, the presence of a human-facing interface does not establish that researchers retain effective authority over every relevant decision. Agents may autonomously choose subproblems, allocate reasoning effort, retrieve material, or modify project files. The extent to which researchers can constrain and audit these operations depends on permissions, execution controls, and the transparency of agent orchestration. A more complete research infrastructure would preserve the relationship between an authorized research objective and the computational activities conducted in its pursuit. It would also distinguish a researcher-approved change of direction from a strategy introduced autonomously by an agent.

For instance, an agent discovering that a conjecture fails for a particular class of examples might propose strengthening one of its assumptions. That is a legitimate mathematical suggestion. But replacing the original claim with a restricted statement without explicitly recording the change could make a successful proof appear to resolve a question that was never actually settled. The distinction can be represented through versioned research objectives and explicit relationships between conjectures, counterexamples, revised assumptions, and successor questions. Such mechanisms are not established by the Open Math OS feature descriptions. SAIR’s governance programme extends the agenda question to institutional scale. Its proposed community committees would participate in decisions concerning model development, benchmarks, data use, and compute allocation. These commitments recognize that control over the tools and resources used by mathematicians can influence which research programmes become feasible.

The unresolved question is whether these commitments translate into binding, independently accountable decisions. The distinction between a researcher’s ability to submit a prompt and the mathematical community’s effective control over its research infrastructure is substantial.

2. Exploration: more agents do not necessarily mean more mathematical progress

Mathematical exploration is often nonlinear. It can involve constructing examples, identifying exceptions, searching for counterexamples, testing auxiliary lemmas, investigating special cases, and comparing proof strategies. This is the function for which Open Math OS provides its most distinctive AI-native capability: Ultramath, the parallel-agent mode. Several agents can investigate a problem concurrently, share findings, and return proposed results to the main conversation. Together with SageMath, PARI/GP, SymPy, Lean, and the project’s persistent computational environment, this arrangement supports an integrated experimental workflow. The potential advantage is clear. Different investigations can proceed simultaneously rather than competing for one sequential interaction. An algebraic approach, a numerical search, and an attempt at formal proof construction can generate complementary evidence. If one route fails, another may still produce a useful result. Nevertheless, parallelism increases the number of opportunities to discover something; it does not automatically increase the independence or quality of the discoveries.

Agents using the same underlying model may repeat the same incorrect assumption or select similar strategies. Shared conversational context can improve coordination while also allowing an erroneous conclusion to propagate between agents. An apparent consensus among agents is therefore not equivalent to independent verification. The relevant architecture should distinguish the diversity of investigative strategies from the number of agent processes executing them. A further distinction concerns negative results. A computational search that finds a valid counterexample has established that a particular universal statement is false. An exhaustive classification may establish the absence of a counterexample within a precisely defined finite domain. But an agent that fails to discover a proof has established neither that the theorem is false nor that no proof exists.

A persistent research system should preserve those differences. It should record whether an investigative result is a valid counterexample, a bounded computational finding, a failed search, a provisional conjecture, or a proof supported by separately identified evidence. The Equational Theories Project demonstrates why this level of organization matters. The project determined the implication relationships among 4,694 elementary equational laws for magmas, covering 22,028,942 ordered pairs, through a combination of human and automated work, with the results validated using Lean. Its significance for Math 2.0 is not simply that computation examined an enormous problem space. It is that the collaboration produced a structured mathematical classification whose conclusions could be checked and investigated further.¹⁶

Open Math OS provides important prerequisites for comparable collaborative investigations, but the public materials do not establish that Ultramath maintains a structured graph of conjectures, failures, intermediate obligations, and verification evidence. Nor do they provide controlled measurements showing that its parallel agents produce better mathematical outcomes per unit of compute and researcher attention than equivalent sequential workflows. The relevant measure is not the number of agents, generated tokens, or candidate proofs. It is whether parallel investigation produces independently valid findings, meaningful counterexamples, or reusable mathematical structure at a justifiable total cost.

3. Verification: mathematical correctness requires an explicit assurance boundary

Verification is perhaps the easiest function to confuse with tool availability. Open Math OS includes Lean and Mathlib, making formal proof development accessible within its hosted environment. This removes practical barriers associated with installing and maintaining a local proof-assistant toolchain, and it allows AI-generated proof candidates to be checked using a system designed for formal mathematical reasoning. However, the fact that Lean is installed does not imply that every mathematical claim produced by Open Math OS has been formalized, much less that every result has undergone an independent kernel check.

Mathematical claims appearing in an AI-assisted workflow can occupy several evidentiary states. A natural-language proof may appear persuasive but remain unverified. A computational experiment may support a conjecture only for the tested cases. A proof assistant may check a formal statement that differs from the original informal claim. Even a successfully elaborated Lean file may depend on unapproved axioms or incomplete placeholders. Lean’s documentation makes these boundaries explicit. In particular, #print axioms can reveal assumptions on which a declaration transitively depends, including sorryAx introduced through unfinished proofs. The documented lean4checker mechanism provides an additional means of rechecking stored formal proof objects.¹⁷

Two separate verification questions therefore arise. The first asks whether the formal derivation establishes the proposition encoded in the proof assistant, under its declared assumptions. This can be addressed through the relevant trusted checking mechanisms. The second asks whether that proposition corresponds to the mathematical claim the researcher intended to establish. This requires attention to definitions, quantifier domains, hypotheses, and the interpretation of the formal objects involved. A proof may therefore pass the first test while failing the second. An integrated mathematical research environment should preserve this distinction through explicit evidence records. It should identify the precise theorem checked, the proof-assistant and library versions used, the accepted logical assumptions, and the relationship between the formal theorem and its informal interpretation. It should not present a general verified status without specifying what was verified and by which mechanism.

The public Open Math OS demonstration includes examples of Lean checking, and its agents can operate within an environment containing formalization tools. These are useful capabilities. They are not evidence that verification is enforced as a mandatory lifecycle step, that proof artifacts are independently reproducible, or that semantic fidelity is systematically reviewed. The stronger Math 2.0 requirement is thus not simply to make formal verification easier to invoke. It is to ensure that the assurance attached to each mathematical claim remains precise, inspectable, and independent of the agent that generated it.

4. Understanding: explaining a proof is not the same as understanding it

The distinction between solving a mathematical problem and understanding its solution is central to Tao’s Math 2.0 argument. A successful proof establishes a proposition, while mathematical understanding involves recognizing the mechanisms that make the proposition true, the role of its hypotheses, its relationship to other results, and the ways in which its methods can be adapted or generalized. These activities are related but not interchangeable. An AI model may explain a complicated derivation fluently without identifying the central mathematical idea. It may produce several alternative proofs that differ syntactically but rely on essentially the same construction. Conversely, a short explanation of a key invariant or structural correspondence may contribute more to understanding than a much longer formal derivation.

Open Math OS explicitly targets activities such as explaining mathematical arguments, discussing mathematical topics, and helping researchers understand existing results. Tao’s soft-launch announcement identifies these as useful applications of its hosted open-weight models, even while acknowledging that those models remain behind the leading frontier systems in demanding mathematical problem solving.¹⁸ This makes understanding a particularly important criterion for evaluating the initiative. If Open Math OS cannot yet compete with the strongest proprietary systems on difficult one-shot proof generation, its potential value may lie partly in making mathematical arguments more accessible, easier to investigate, and more effectively integrated with computation and formalization. Nevertheless, an explanation that satisfies a user during a conversation does not establish that the user has acquired transferable mathematical understanding.

A meaningful evaluation might examine whether researchers can reconstruct a proof without AI assistance, identify an unnecessary hypothesis, find a counterexample to an invalid generalization, or apply the central method to a related but unfamiliar problem. The assessment should also distinguish immediate assisted performance from retained independent competence. A researcher who can answer a question only while consulting the same model may have acquired access to a useful computational capability without necessarily learning the underlying mathematics.

The importance of usable mathematical understanding was emphasized again on 16 October 2026 by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz. In How to Formalize All of Mathematics, they argue that the scientific value of large-scale AI-generated formalization depends on whether the resulting libraries can actually be maintained and used to develop further mathematics. Their concern is not that automated formalization is inherently undesirable, but that maximizing formal output can produce artifacts whose practical mathematical value is disproportionately low.¹⁹ This observation applies directly to Open Math OS. An integrated environment can help mathematicians produce and examine formal proofs, but its contribution to understanding depends on whether those proofs reveal reusable methods and facilitate subsequent inquiry. The architecture can support this through alternative explanations, conceptual dependencies, human annotations, and mechanisms for reconstructing earlier arguments. It cannot infer human understanding from the presence of those materials alone.

5. Knowledge: persistence is not yet a mathematical memory

The knowledge function exposes a particularly important distinction between a useful research workspace and durable mathematical research infrastructure. Open Math OS preserves project files and conversations in persistent cloud environments. A researcher can return to previous code, calculations, proof attempts, and documents instead of reconstructing the computational workspace after every session. This form of operational persistence is genuinely valuable. Mathematical knowledge, however, requires more than the retention of computational objects. A theorem is not simply a file containing a statement and a proof. Its usefulness depends on the definitions it invokes, the assumptions under which it holds, the relationships connecting it to other theorems, and the explanations through which researchers recognize where and how it can be applied. These relationships become difficult to recover when they exist only implicitly in documents and conversations.

For instance, a project may contain two versions of a lemma, one with an additional hypothesis introduced after a counterexample was discovered. A file history may preserve both versions, but a later researcher still needs to know which statement has been established, why the hypothesis changed, and which subsequent results depend on the earlier formulation. The relevant knowledge infrastructure would identify mathematical contributions independently of the files in which they are stored. It would preserve stable identities for claims, explicit version relationships, typed dependencies, evidence of verification, and links between informal interpretations and formal representations. These mechanisms allow mathematical artifacts to be reused without requiring their original authors to reconstruct the entire investigation.

They also support the distinction between different kinds of mathematical relationships. A formally verified dependency is not equivalent to an informal conceptual analogy; a counterexample that refutes a conjecture is not the same kind of relationship as a theorem that generalizes another. Treating all these associations as generic links would make the knowledge graph easier to implement but less mathematically informative. The distinction becomes significant at scale. A large repository of AI-generated proofs may contain many valid mathematical statements while remaining difficult to navigate, maintain, or extend. The formalization researchers cited above warn specifically against creating large quantities of formal code whose structure and maintainability make subsequent mathematical use impractical. This suggests a practical criterion: the quality of a mathematical knowledge infrastructure should be assessed by whether independent researchers can recover, verify, modify, and build upon its contributions.

The relevant unit of measurement is therefore not the number of stored files, saved conversations, or formal declarations; rather, it is the extent to which the preserved material supports further mathematical work. The Open Math OS documentation establishes project persistence and file collaboration. It does not demonstrate a global mathematical artifact registry, typed theorem-dependency service, semantic knowledge graph, or reproducibility-preserving export mechanism. Those are potential extensions, not verified features of the current platform. This is the central architectural gap between remembering a research session and preserving mathematical knowledge.

6. Community: collaboration requires more than sharing a workspace

Mathematics is a collective enterprise. Its results acquire significance through communication, criticism, verification, teaching, publication, and reuse by researchers who did not necessarily participate in their discovery. AI-assisted mathematical research introduces new questions into this process. Who receives credit when an AI system contributes an essential argument? Who can inspect an unpublished project? Under what conditions may research conversations be used for model training? Who allocates scarce computational resources? And who has authority to correct or withdraw a mathematical artifact that other researchers have begun to use? Open Math OS addresses some of these questions through its organizational design. It emphasizes team accounts, shared projects, persistent conversations, and collaborative work between human researchers and AI agents. SAIR also states commitments to privacy by default, explicit consent before training on researchers’ materials, retained ownership and attribution, and public community participation in governance.²⁰

These commitments are more consequential than conventional collaboration features because they concern the distribution of control over mathematical research. A platform may support shared documents and multi-user chats while retaining exclusive authority over data processing, model training, access to computing resources, and the terms under which contributions are published. Technical collaboration and institutional self-governance are distinct properties. For SAIR’s stated model to become enforceable, governance would need to define the responsibilities of researchers, contributors, platform operators, institutional partners, and committees. Decisions concerning compute allocation, training consent, attribution, disputes, and changes to shared infrastructure would require identifiable procedures and appropriate auditability.

Some of these controls also need technical implementation. A policy requiring explicit training consent must correspond to operational restrictions on relevant data flows. An access-control policy must determine which team members and external collaborators can read or modify a project. A claim of portability must be supported by an export mechanism that preserves the information necessary to continue the research outside the original service. The issue is especially relevant because access to open-weight models does not automatically imply the openness of the hosted platform or the independence of its governance. SAIR’s proposed committees for compute, data governance, tools and benchmarks, training, and education and partnerships provide a plausible organizational structure. What remains to be established is their actual authority, the procedures through which their decisions become binding, and the extent to which users can independently verify that those decisions are enforced.

The stronger Math 2.0 objective is therefore not simply a larger mathematical user community. It is a research environment in which the community can meaningfully influence the development and operation of the tools on which its work increasingly depends.

7. Application: connecting mathematical results to further mathematics and the world

The final function concerns what becomes possible because a mathematical contribution has been established. Application should not be interpreted narrowly as immediate commercial or industrial use. Within mathematics, a theorem may become valuable because it provides a method for proving another result, clarifies a conceptual relationship, or enables work in a previously inaccessible domain. Outside mathematics, applications may involve scientific models, engineering systems, optimization, cryptography, or other areas whose validity depends on additional assumptions. These two forms of application share an important requirement: a mathematical result must be usable in a context that differs from the investigation in which it was produced.

Open Math OS offers scientific computing capabilities that can support this transition. Researchers can use symbolic computation, numerical methods, programming environments, and formal proof assistants within one persistent project. This may make it easier to move between mathematical conjectures, computational experiments, and domain-specific investigations. However, computational execution does not establish that a mathematical result is applicable to a particular scientific or engineering system. A theorem can be deductively correct while its assumptions fail to describe the intended application. A numerical simulation can faithfully execute a mathematical model whose parameters or boundary conditions are inappropriate. A formal proof can establish a property of an abstract algorithm without establishing the same property for a physical implementation. Consequently, mathematical assurance must remain distinguishable from domain-specific validity.

For an application to another mathematical problem, the critical questions concern whether the theorem’s assumptions are satisfied and whether its method transfers meaningfully. For an application to an external system, additional questions concern empirical adequacy, measurement uncertainty, model calibration, implementation errors, and the relationship between formal abstraction and observed behavior. These are not deficiencies that a proof assistant can eliminate simply by checking the underlying theorem. A mature Math 2.0 environment would help researchers trace the relationship between mathematical results and their downstream use. It would permit a theorem to be linked to subsequent formal derivations, simulations, scientific models, or externally validated applications while preserving the different evidence required at each stage.

The public Open Math OS materials establish the availability of computational tools suitable for portions of this workflow. They do not establish mechanisms for automatically tracking mathematical dependencies into external applications or validating the domain assumptions under which those applications operate. The relevant success criterion is therefore not how many scientific tools the environment contains. It is whether mathematical contributions can be transferred, appropriately revalidated, and used to produce reliable new results.

Putting the seven functions together

The seven functions are most revealing when considered as a connected research process rather than as independent capabilities. A mathematician begins with a research objective and authorizes an investigation. Agents and computational tools explore possible results, producing conjectures, counterexamples, computations, and candidate proofs. Verification establishes which claims are supported by specified evidence. Explanatory work develops the mathematical interpretation of those results. Knowledge infrastructure preserves the contributions in a form that later researchers can reconstruct. Community institutions establish the procedures through which they are shared, reviewed, attributed, and maintained. Applications test whether the resulting mathematics can support further inquiry.

A failure at any of these boundaries can limit the overall value of the investigation. A proof may be correct but disconnected from the problem originally posed. An important counterexample may disappear when the agent conversation is summarized. A formally checked result may be difficult to reuse because its definitions were generated in an isolated library. A useful computational artifact may become inaccessible when a hosted service changes. An unpublished manuscript may be exposed without the researcher’s authorization. The platform’s ability to support the complete research process therefore depends on more than the capabilities of its individual components.

Table 1 summarizes the corresponding assessment. Its final column identifies observable evidence that would justify a stronger claim about each research function; it does not imply that every proposed mechanism must be implemented internally by Open Math OS.

Research function	What Open Math OS currently enables	What is not established	What would demonstrate stronger Math 2.0 value
Research agenda	Researcher-led projects, shared objectives, delegation to agents	Explicit authority boundaries, versioned goals, auditable changes of research direction	Researchers demonstrably control delegation, resources, and revisions to research objectives
Exploration	Ultramath parallel agents, symbolic computation, persistent experiments	Strategy independence, structured negative results, coordination semantics, efficiency gains	Valid discoveries and useful failed investigations recovered more effectively under controlled comparisons
Verification	Lean, Mathlib, computational checking tools	Mandatory checking, exact theorem–evidence binding, semantic fidelity checks	Independent reproduction of formal proofs and explicit review of the intended statements
Understanding	Explanation, discussion, formalization, alternative reasoning approaches	Improved human comprehension, retention, or transfer	Researchers reconstruct arguments, diagnose assumptions, and solve related tasks independently
Knowledge	Persistent projects, files, conversations, downloadable outputs	Stable mathematical identities, typed dependencies, versioned evidence, complete portability	Independent teams recover and reuse results without the original agents or project environment
Community	Shared teams and conversations, privacy and governance commitments	Binding governance procedures, enforceable consent, transparent allocation and dispute mechanisms	Demonstrated community decision rights, auditable controls, and sustainable independent participation
Application	Scientific computing and formal mathematical tools	Domain-specific validation, downstream dependency tracking, demonstrated external reuse	Mathematical results are correctly transferred into further research or independently validated applications

Table 1: Assessment of Open Math OS against the seven research functions. The distinction is between enabling functionality, unestablished assurance, and evidence of actual scientific benefit.

The table identifies an important asymmetry in the present platform. Open Math OS provides its clearest direct contribution to exploration and operational collaboration. The integration of models, agents, scientific computing, and persistent team projects addresses a concrete difficulty that mathematical researchers encounter when combining AI with existing tools. It also provides valuable access to formal verification through Lean and Mathlib, while making AI-assisted mathematical explanation and discussion available within the same environment. Its contribution to durable mathematical knowledge, independently established understanding, and enforceable scientific governance is less well established by the available evidence. These functions require mechanisms and institutional outcomes that cannot be inferred from the presence of a persistent workspace or an open-weight model.

This distinction should not be read as a verdict that the current platform has failed to provide those functions. Open Math OS was soft-launched in October 2026 and is explicitly presented as an evolving environment. The stronger mechanisms may be implemented later, developed through community contributions, or provided by interoperable external systems. It is, however, a substantive distinction between a platform that makes mathematical AI convenient to use and one that changes the infrastructure through which mathematics becomes cumulative knowledge. The seven-function assessment also suggests that evaluating Open Math OS solely against the reasoning performance of proprietary frontier models would be incomplete. Its current hosted models may be less capable on difficult standalone problems, yet the integrated environment could still provide greater value for some sustained research activities if it reduces computational friction, improves collaboration, or enables independent reconstruction of work.

Conversely, the existence of these integrated capabilities cannot establish such benefits without comparative evidence. The central architectural question is therefore whether Open Math OS can move beyond preserving the state of a mathematical investigation toward preserving the mathematical meaning and evidentiary status of its contributions. That is the threshold at which a collaborative AI workspace begins to resemble mathematical research infrastructure. Crossing it would not require Open Math OS to replace existing scholarly institutions or formal libraries. It would require the system to connect reliably with them, so that computational discoveries can be independently checked, understood, maintained, and reused.

The subsequent sections examine precisely this unresolved infrastructure problem: what kind of mathematical knowledge representation is needed, how control over that infrastructure can remain scientifically legitimate, and how its contribution to mathematical understanding could be tested rather than merely asserted.

The missing mathematical knowledge infrastructure

The seven-function assessment exposes a difference between preserving the activity of mathematical research and preserving the knowledge that research produces. Open Math OS supplies persistent projects in which conversations, programs, manuscripts, and proof attempts can remain available across sessions. This is a useful response to the fragmentation of contemporary AI-assisted research, but operational persistence should not be confused with a mathematical knowledge base: a file can be retained without identifying the precise theorem it contains, a conversation can be searchable without distinguishing conjecture from proof, and a semantic index can retrieve related passages without establishing any logical relation between them. The additional requirement is epistemic persistence, through which an independent researcher can recover a contribution’s exact meaning, assumptions, evidence, dependencies, and revision history.

The distinction becomes especially consequential as agents produce mathematical material at increasing scale. A project may contain several formulations of a conjecture, a counterexample to one formulation, a revised theorem, alternative proofs, and an explanatory note connecting the result to an earlier paper. A search engine can locate each item, but it does not necessarily establish which version remains valid or why the revision occurred. Consequently, a mathematical knowledge infrastructure should treat identifiable contributions—not documents, conversation turns, or embedding vectors—as its principal durable objects, while retaining explicit links to the files and activities through which those contributions were created.

Stable mathematical identities and versioned evidence

A mathematical artifact requires at least three forms of identification, because the identity of a research contribution is not reducible to the identity of its electronic representation. A contribution identifier refers to a developing mathematical object such as a conjecture or theorem; a revision identifier fixes a particular statement, its assumptions, and associated evidence; and a representation identifier identifies a concrete proof file, manuscript excerpt, computational output, or other serialized artifact. Cryptographic hashes can establish that the bytes of such a representation have not changed, but they cannot by themselves establish mathematical equivalence, scholarly priority, or the identity of the underlying idea.

Two Lean files may encode different proofs of the same proposition and therefore have different hashes, whereas two declarations with similar names may establish genuinely different theorems because their hypotheses or imported definitions differ. Even propositions proved equivalent under an identified mathematical interpretation need not constitute the same research contribution: different formulations can illuminate different structures or enable different applications. A reliable registry should therefore preserve exact representations while recording equivalence and conceptual identity as separate, evidence-qualified relationships. It should not infer either relationship merely from names, textual similarity, or a model’s judgment.

For a theorem, the minimum artifact record would identify the precise statement, quantified domains, definitions, formal environment when applicable, and the evidence supporting its accepted status. The evidence must remain distinguishable from the claim. A checked Lean derivation, a natural-language argument reviewed by a mathematician, and a finite computational search provide different forms of assurance, even if they concern the same proposition; similarly, a successful proof check does not establish the correspondence between an encoded statement and the theorem originally intended. Versioned evidence allows the record to acquire stronger assurance over time without rewriting what was previously known or claimed.

Provenance supplies another essential dimension. A later researcher may need to know which agent proposed a lemma, which experiment supplied the initial evidence, which dependencies were available during proof checking, and which contributor authorized a revision. The W3C PROV family provides a general interoperable vocabulary of entities, activities, agents, and derivation relationships that can support these records, although it does not define mathematical proof validity or scholarly authority.²¹ By combining provenance with exact statements and typed evidence, a registry can preserve what was done without mistaking a faithful execution history for proof that every conclusion was correct.

Relationships that preserve their mathematical meaning

A mathematical knowledge graph must distinguish relationships according to what they assert and how they can be supported. A deductive relation may state that one formal declaration depends on another, or that a particular implication holds under specified assumptions. A semantic relation may connect an informal theorem to a formalization or identify a generalization whose mathematical significance requires interpretation. An investigative relation may record that a counterexample refuted an earlier conjecture, that one investigation motivated another, or that a revised statement superseded an earlier version. Although these relations can appear together in a graph, they do not have the same evidentiary requirements.

A formal dependency recovered from a pinned proof-assistant environment has a different status from a suggested analogy between two papers. A model may propose that one theorem generalizes another, but that proposal must not silently become a proof of implication; likewise, an embedding search can identify candidate connections without establishing that the relevant statements share the same definitions or quantifier domains. This is particularly important when agents retrieve graph relationships as premises for further reasoning, because an unsupported semantic edge can otherwise propagate through successive investigations and acquire the appearance of an accepted theorem.

The proposed relationship vocabulary in Table 2 illustrates the required distinctions; it is not a description of services already implemented by Open Math OS.

Relationship	Meaning	Evidence appropriate to the assertion
formally_depends_on	A formal declaration uses another declaration within an identified environment	Dependency extraction with pinned versions and documented extraction semantics
implies_under	One proposition entails another under specified assumptions	Formal proof or independently reviewed mathematical argument
equivalent_under	Statements are equivalent in a declared mathematical context	Evidence establishing the required implications in both directions
formalizes	A formal declaration represents a stated informal mathematical claim	Reviewed correspondence of definitions, quantifiers, hypotheses, and conclusions
generalizes	A result extends another through an identified mathematical relation	Explicit specialization, reduction, embedding, or reviewed argument
conceptually_related_to	Two results share a potentially useful idea or structure	Attributed mathematical interpretation or an explicitly provisional hypothesis
refuted_by	A counterexample contradicts the specified claim	Valid witness meeting the domain and falsifying the conclusion
motivated_by	One research activity or claim arose from another	Documented research history and attribution
supersedes	A revision replaces an earlier artifact for a stated purpose	Version history, correction record, and identified authority

Table 2: Proposed typed relations for mathematical knowledge. Deductively established, semantically interpreted, and historically documented edges must retain distinct evidence.

These distinctions support evidence-sensitive retrieval. A researcher looking for formally established dependencies should be able to exclude provisional model-generated associations; conversely, an agent exploring a novel conjecture may find speculative conceptual connections useful, provided their status remains explicit. The point is not to forbid uncertain knowledge from entering a graph, but to prevent uncertain associations from being promoted into deductive facts by the act of storing or retrieving them.

What existing mathematical infrastructures demonstrate

Several established research programmes already provide components of such an infrastructure. Mathlib illustrates how a public, maintained formal library can preserve statements, proof objects, dependencies, and revisions across large numbers of contributors, while making verification independent of the original proof author.²² Its value is not limited to the correctness of individual declarations: coherent definitions, documentation, review, and compatibility across revisions make the resulting knowledge usable in subsequent mathematical developments. A library composed entirely of valid but poorly organized generated proofs could satisfy narrow checking requirements while remaining difficult to maintain or extend.

MMT, developed by Florian Rabe and Michael Kohlhase, addresses a different problem through modular representations of mathematical theories that can abstract from particular logical foundations.²³ Its relevance to a mathematical commons is that researchers need not use one proof assistant, ontology, or foundational system for every investigation. Interoperability instead requires explicit mappings among representations, together with evidence for the mathematical relationships those mappings claim to preserve. Having two systems export files in a common syntax would not, by itself, make their theorems semantically equivalent.

Research on formal dependency networks offers complementary evidence. The Network Structure of Mathlib examines the graph of formal declarations and shows why structural centrality cannot straightforwardly be interpreted as mathematical importance: central nodes may reflect shared language or software infrastructure rather than deep conceptual dependencies.²⁴ TheoremGraph likewise investigates connections between formal mathematical libraries and informal research literature, using extraction and semantic matching to propose large-scale networks of mathematical statements and relations.²⁵ These systems demonstrate the feasibility of valuable graph-based services while also underscoring the need to distinguish extracted formal dependencies from inferred relationships in natural-language sources.

None of these systems establishes that the hosted Open Math OS implementation already provides a global artifact registry or a semantically typed mathematical knowledge graph. They demonstrate existing mechanisms that might be combined with a research workspace, maintained independently of it, or exposed through interoperable services. For a mathematical commons, such composability may be preferable to requiring one provider to operate every knowledge, verification, and publication function.

Preserve refuted conjectures as well as proved theorems

A registry limited to successful proofs would still discard some of the most informative products of mathematical exploration. An invalid conjecture can reveal the limits of a proposed generalization, while a counterexample may identify an essential hypothesis or motivate a revised definition. A failed attempt is not necessarily a mathematical result, however: inability to find a proof is different from a counterexample, and an inconclusive computational search should not be represented as evidence of impossibility. A research-state system must preserve these statuses rather than flattening all negative outcomes into one category.

Consider the initial conjecture that 12 divides n^3-n for every integer. The value n=2 gives n^3-n=6, refuting the conjecture; yet the very same calculation later helps establish that 6 is the greatest universal positive divisor. Deleting the refuted claim after correcting it would conceal part of the rationale for the final theorem. More generally, a durable record should connect a refuted conjecture to its validated counterexample, its corrected successor, and any later contributions that depend on the underlying mathematical insight.

The distinction between a research-state graph and a durable mathematical knowledge graph is useful here. The former contains active obligations, candidate strategies, failures, and provisional findings so that an investigation can continue; the latter preserves selected contributions with stable identities, exact revisions, and evidence sufficient for independent reuse. Research-state systems such as Danus and Euler explore aspects of connected mathematical memory beyond conversation transcripts, although their reported implementations do not establish the presence of the corresponding service within Open Math OS.²⁶²⁷ Nor should claims about the effectiveness of their graph representations be confused with controlled evidence that mathematicians who use them acquire deeper understanding.

From persistent projects to durable mathematical contributions

The architectural gap is therefore precise. Open Math OS documents the persistence of project materials, including conversations, files, computations, and collaborative work; a mathematical knowledge infrastructure would additionally preserve the identity and evidentiary relationships of the contributions represented by those materials. In the stronger environment, a researcher could retrieve an exact theorem, determine the assumptions under which it was checked, reconstruct relevant computations, inspect its history of corrections, and discover which subsequent results depend on a particular version. Agents could likewise distinguish established premises from exploratory suggestions without reconstructing the original discussion in which each appeared.

Implementing these mechanisms need not begin with a universal ontology of mathematics. A more tractable sequence would introduce executable environment manifests, exact versioned proof-evidence records, stable contribution identifiers, and a restricted vocabulary of typed dependencies before attempting broad semantic inference or cross-foundation translations. This would preserve the value of exploratory work without forcing every intermediate idea into an elaborate publishing schema, and it would make early benefits measurable through independent reconstruction and reuse.

A mathematical knowledge layer also changes the institutional questions facing Open Math OS. Once theorem identities, evidence records, and dependencies become important shared infrastructure, the organization maintaining them gains influence over the visibility and accessibility of mathematical contributions. The technical design must therefore be considered together with the rights, governance rules, and practical independence of the researchers using it.

Open infrastructure, scientific sovereignty, and governance

The Open Math Model initiative has an institutional motivation as well as a technical one: mathematicians should not become entirely dependent on a small number of organizations for access to the models, computing resources, data policies, and research environments through which increasingly important mathematical work is conducted. A highly capable proprietary system might generate valuable proofs while leaving the research community dependent on its provider for access to the model or the relevant research history; conversely, an open-weight model might be independently runnable while its hosted agent orchestration, storage services, and collaboration controls remain opaque. Neither model performance nor the availability of weights is therefore a sufficient measure of scientific independence.

SAIR’s public Open Math Model statement commits to open mathematical model development, researcher control over contributions, consent for training uses, attribution, and forms of community participation in governance.²⁸ These commitments distinguish the initiative from a purely commercial mathematical assistant, especially where users submit unpublished conjectures, proof strategies, or partial research results. Their effectiveness nevertheless depends on operative rights, technical controls, and institutional procedures that cannot be inferred solely from launch material. The appropriate analysis must separate the different meanings of openness before asking how the platform could establish them.

Five dimensions of an open mathematical platform

Model openness concerns whether weights and appropriate licenses permit models to be inspected, adapted, and executed independently. Software openness concerns the availability and deployability of the systems that serve those models, coordinate agents, manage scientific tools, and operate project workspaces. Knowledge openness concerns the portability of mathematical claims, formal proof evidence, dependencies, and research histories through documented representations. Research sovereignty concerns the practical capacity of researchers to control authorized uses of unpublished materials, access permissions, attribution, and transfer. Institutional openness concerns binding participation in decisions about shared infrastructure, rather than merely an invitation to offer advice.

The dimensions summarized in Table 3 are related, but none follows automatically from another. Free access can improve participation without establishing independent deployment, and an open-weight license does not necessarily reveal training procedures, serving configurations, or the internal orchestration stack. Even a public code repository can fail to support genuine deployability if its dependencies, infrastructure requirements, and operational assumptions are unavailable. Similarly, the ability to download conversations or files does not establish that the mathematical meaning and evidentiary status of a project can be reconstructed elsewhere.

Dimension	Evidence required for a strong claim	What must not be inferred automatically
Model openness	Released weights, applicable licenses, and independently runnable inference	Open orchestration or complete training reproducibility
Software openness	Source code, build and deployment instructions, dependencies, and independently working installations	That source publication alone establishes an operable alternative service
Knowledge openness	Portable mathematical artifacts, exact proof evidence, documented schemas, and stable references	That exported conversations preserve claims and dependencies
Research sovereignty	Enforceable permissions, consent and revocation procedures, export rights, and attribution records	That a general privacy statement establishes every operational control
Institutional openness	Binding decision rules, accountable governance, transparent allocations, and review procedures	That consultation or an advisory committee gives users effective authority

Table 3: Distinct dimensions of openness for mathematical research infrastructure. Each must be evaluated through evidence specific to the rights or capabilities it claims to provide.

At the October 2026 soft launch, Open Math OS hosts third-party open-weight models and offers selected academic researchers access to an integrated computational environment. This contributes to model accessibility and lowers some operational barriers; it does not, on the public evidence reviewed here, demonstrate that the complete orchestration service can be deployed independently or that every project can be exported with executable environments and mathematically meaningful evidence. SAIR’s programme includes broader commitments to open tools and community influence, but the intended future infrastructure must not be conflated with capabilities already demonstrated.

Donated compute improves access but requires accountable allocation

Large open-weight models can remain economically inaccessible even when their licenses permit unrestricted research. Inference accelerators, persistent computational environments, storage, operations, and engineering support impose costs that individual mathematicians and research groups may be unable to bear. SAIR’s reliance on donated resources is therefore an important part of the initiative: it aims to reduce the gap between legal access to models and the practical ability to use them for sustained research.

The same arrangement creates a different dependency. When access to computing resources is allocated through one organization, researchers may retain the right to run open models while lacking the means to reproduce their work at comparable scale outside that organization. The sustainability of free access depends on donations, capacity planning, and allocation procedures rather than on model licensing alone. Where demand exceeds supply, decisions about which projects receive resources can shape which mathematical agendas become feasible, even without anyone explicitly selecting the theorems researchers should pursue.

A credible governance arrangement should therefore explain how allocations are made, which criteria apply, whether participants can challenge decisions, and how conflicts of interest are addressed. An allocation rule favoring projects with rapidly measurable outputs could disadvantage conceptual investigations whose usefulness is difficult to predict, while an opaque discretionary process could undermine confidence in community control. SAIR’s proposed committee for compute allocation recognizes this issue, but the existence of an announced committee is not itself evidence that its decisions are binding or independently reviewable.

Consent must follow data-processing purposes

SAIR’s statement that researcher contributions will not be used for model training without consent addresses an important concern, but training is only one possible use of research data. A hosted service may process unpublished mathematical material to execute an authorized inference request, preserve project files, share work with collaborators, diagnose operational failures, evaluate model behavior, or prepare material for public dissemination. These purposes have different implications for confidentiality and scholarly control, and permission for one should not silently become permission for the others.

For example, authorizing a model to inspect an unpublished proof during an interactive research session is not equivalent to consenting to include that proof in a future training corpus. Permission for a collaborator to read a project does not necessarily authorize public disclosure, and an administrator’s authority over a shared computational workspace does not automatically determine the rights associated with every participant’s pre-existing contribution. The system should distinguish access, modification, further processing, onward sharing, training, and publication through rules appropriate to the actual rights and responsibilities of the participants.

The policy distinction has a technical counterpart. A claim of purpose-specific consent requires identified data flows, retention periods, authorization mechanisms, and records adequate to demonstrate that the stated restrictions are enforced. Researchers also need to understand how their materials may appear in logs, diagnostic records, backups, exported projects, and shared conversations. The public privacy-by-default and opt-in commitments establish the intended approach, not a complete independently verified account of every processing path or permission boundary.

The legal analysis likewise cannot be reduced to the statement that researchers own their work. Copyright, contractual rights, coauthorship, institutional obligations, and the status of mathematical ideas can differ; a platform’s broad ownership language does not automatically settle those questions. A rigorous review should therefore examine operative terms and technical controls without inferring comprehensive legal rights from a general institutional statement.

Collaboration creates attribution and authorization problems

Shared research projects are valuable because mathematics is often produced through sustained cooperation, but they introduce governance problems absent from a private one-to-one assistant. A team may include several mathematicians contributing unpublished claims, proofs originating in other collaborations, model-generated formalizations, and computational artifacts developed under different agreements. If the workspace applies one undifferentiated permission to everything in the project, it may become difficult to establish who can disclose, modify, train on, or republish a particular contribution.

The infrastructure should therefore distinguish team membership from rights over mathematical artifacts, and it should make contributor attribution separate from authority to authorize every subsequent use. A timestamped provenance record can help reconstruct which operations occurred, yet timestamps alone do not settle scholarly priority, intellectual property, or the legitimacy of a disclosure. Corrections, disputes, and changes in authorized access may require accountable institutional procedures even when technical records are immutable.

These concerns connect directly to mathematical knowledge infrastructure. A stable contribution identity can preserve links between results, authors, and supporting evidence, but it should not force confidential work into a public registry or confer publication authority on the operator storing it. Private or access-controlled artifacts must be possible, and disclosure should remain governed by the permissions attached to the research rather than by the mere fact that a computation has succeeded.

Scientific sovereignty as an operational test

Scientific sovereignty becomes more precise when expressed as a test rather than a label. A research team should be able to export a substantive project, reconstruct its relevant computations using documented dependencies, independently check its accepted mathematical claims, and continue work using another provider or an institutionally controlled environment. Merely downloading files establishes a much weaker property if the receiving team cannot determine which theorem revisions are current, how a proof was checked, or what unresolved obligations remain.

The test exposes three complementary requirements. Computational portability concerns source files, tools, manifests, and sufficiently reproducible execution. Epistemic portability concerns the recovery of mathematical meaning, assumptions, evidence, dependencies, and revision histories. Institutional portability concerns the legitimate rights and practical ability to continue the work outside the original service. A platform may satisfy any one without satisfying the others: for example, technically exportable files may lack the information needed to reconstruct a proof, while a publicly checkable theorem may have been generated through an unavailable proprietary model.

These distinctions also clarify what complete discovery-process reproduction can and cannot mean. A valid mathematical result may be independently verifiable even when a stochastic or proprietary search process cannot be reproduced exactly. Scientific sovereignty should not require recreating every model token to establish the theorem’s truth; it should require sufficient portability of the relevant mathematical evidence and of the materials necessary for legitimate further research. The stronger question is whether mathematicians remain able to examine and extend their work when the original platform is unavailable.

Community governance must confer identifiable authority

Open Math Model proposes community participation in compute allocation, data governance, model training, tools and benchmarks, and education and partnerships. These structures may align the infrastructure with researchers’ needs, but their significance depends on the authority assigned to them. An advisory committee may be able to recommend a policy without determining the decision that is ultimately enforced; consultation and control are not interchangeable institutional arrangements.

An accountable governance system would identify which body can decide each class of matter, how its members are appointed or selected, what evidence and disclosures accompany decisions, and what procedures exist for appeal or correction. The relevant questions extend from compute allocations and training-data permissions to contributor attribution, changes in project-access policies, and amendments to the governance arrangements themselves. These responsibilities need not reside in one organization, and concentrating all of them in a hosted service could recreate the dependency that the initiative seeks to reduce.

A particularly revealing evaluation would examine an actual disputed decision. A researcher denied resources or challenging an unauthorized data use should be able to identify the operative rule, the body with binding authority, the basis of the decision, and an appropriate route for review. Such an audit tests effective governance more directly than a declaration of community participation. Funding through a nonprofit organization can support independence, but nonprofit status alone does not guarantee accountable researcher control.

A commons must survive replacement of its provider

The institutional and technical arguments converge at the mathematical record. If accepted results exist only within one hosted platform, its operator possesses substantial practical influence over their accessibility, preservation, and interpretation, even when its intentions are responsible. An independently checkable proof or versioned mathematical artifact, by contrast, can be transferred to a separate repository or maintained by another institution without requiring the original model or service to remain permanently available.

This does not eliminate the need for institutions, maintenance funding, access controls, or shared standards. Federated infrastructure must still manage identifiers, incompatible mathematical representations, differing permissions, and disputes over semantic interpretation. Its advantage is not the absence of authority, but the possibility of distributing responsibilities and contesting decisions without losing the underlying mathematical evidence. Researchers may also preserve alternative interpretations or formalizations without accepting one platform’s ontology as the sole authoritative representation.

The resulting definition of a mathematical commons is more demanding than free access to AI models or an integrated workspace. Its technical content is the portability of mathematical contributions and their evidence; its institutional content is the effective ability to control authorized research uses, replace service providers, and participate in accountable decisions about shared resources. SAIR’s published commitments recognize the importance of those objectives, while the public evidence available at the Open Math OS soft launch leaves important implementation and governance guarantees unverified. Those unresolved guarantees are not reasons to dismiss the initiative; they are the criteria against which its progress toward genuine scientific sovereignty should be assessed.

Can parallel agents increase mathematical understanding?

The central computational promise of Ultramath is that several AI agents can investigate a mathematical problem concurrently, pursuing different approaches and combining their findings. This can increase the volume of mathematical work performed within a given period, but its relationship to mathematical progress is less straightforward. A mathematical investigation is not simply a search for any correct proof. The process may reveal why a theorem is true, which assumptions are necessary, how different arguments relate to one another, and which ideas can be applied to new questions. These outcomes cannot be inferred from the number of agents executing a task or even from the number of valid proofs they produce. The relevant distinction is between search throughput, the rate at which a system generates candidate results, and epistemic productivity, its contribution to reliable, intelligible, and reusable mathematical knowledge.

Although parallel agents may improve both, greater search throughput does not by itself establish increased epistemic productivity.

What parallel search can establish

Consider n agents independently attempting to solve the same mathematical problem. Suppose each has probability p of producing a successful result and that the success events are statistically independent. Under those assumptions, the probability that at least one agent succeeds is

P(\text{at least one success})=1-(1-p)^n. \tag{1}

The expression captures a genuine advantage of independent parallel search: even when each individual attempt has a modest probability of success, additional attempts increase the probability that at least one succeeds. However, its assumptions are strong and generally unjustified for a collection of agents using the same model family, related prompts, common retrieval sources, and shared conversational context. In the limiting case where every agent produces exactly the same outcome, the probability of at least one success remains p, regardless of how many copies are executed. The independence expression would substantially overestimate the benefit. The difficulty is not restricted to identical outputs. Agents can produce different-looking proofs while relying on the same erroneous lemma or unjustified assumption. They can also converge on similar strategies because they share training distributions, tool interfaces, and mathematical representations. A more informative analysis therefore treats success events as potentially correlated.

Let X_i be the indicator that agent i produces a valid solution, and let S=\sum_{i=1}^{n}X_i denote the number of successful agents. Suppose the indicators have a common success probability p and a common pairwise correlation \rho. Then

\operatorname{Var}(S) = np(1-p)\left[1+(n-1)\rho\right]. \tag{2}

This follows from summing the individual Bernoulli variances and the pairwise covariances. The formula illustrates how positive correlation increases variability in the number of successful agents: their outcomes tend to succeed or fail together rather than providing independent evidence. The correlation parameter must satisfy the feasibility constraints of the joint Bernoulli distribution; the formula should not be interpreted as permitting arbitrary values of \rho. Nor does it determine the probability of at least one success. In general, the marginal probability p and the pairwise correlation alone are insufficient to determine that probability, because higher-order dependence among agents also matters.

The mathematical point is consequently more limited but important: the expected advantage of parallel agents depends on the diversity and dependence structure of their attempts, not merely on their number. For Ultramath, this motivates an empirical question. Are agents pursuing meaningfully different mathematical strategies, or are they primarily producing additional samples from closely related reasoning processes? The public description establishes parallel investigation and sharing of findings. It does not supply the data required to characterize correlations among agent errors or to estimate the resulting gains in valid mathematical discoveries.

Proof diversity is more important than response diversity

Even when parallel agents produce several correct proofs, their mathematical contribution depends on the relationships among those proofs. Two arguments may differ in length, notation, or organization while relying on the same essential idea. Conversely, two proofs of the same theorem may expose fundamentally different mathematical structures. The latter situation can be particularly valuable because it may reveal connections to other areas of mathematics, suggest generalizations, or provide methods that apply where the original proof does not. A system that rewards syntactic diversity may miss this distinction. It could generate numerous paraphrases, reordered derivations, or formally different sequences of equivalent lemmas without adding substantial mathematical understanding.

Evaluating proof diversity therefore requires attention to the mathematical objects and transformations on which an argument depends. For a formal proof, relevant evidence might include the essential lemmas invoked, the algebraic constructions used, or the reduction strategy connecting the hypotheses to the conclusion. For an informal proof, comparison may require expert judgment about the central mathematical mechanism. Neither approach is straightforward. Two formal proofs using different library declarations may implement the same underlying idea, while apparently similar proof structures may have different conceptual interpretations. The objective is not to force all proofs into one canonical taxonomy. It is to determine whether multiple agents are contributing independent mathematical perspectives or merely increasing the volume of generated material.

A useful multi-agent system might deliberately assign heterogeneous tasks: proof construction, counterexample search, alternative formalization, literature comparison, and criticism of assumptions. Such specialization could improve the diversity of evidence even without guaranteeing statistical independence. The resulting findings should remain separately attributable and subject to appropriate checking. An agent’s agreement with another agent is not sufficient assurance when their conclusions may rely on a shared unsupported premise.

The value of negative results and failed approaches

Mathematical exploration produces valuable information even when it fails to establish the desired theorem. A valid counterexample can conclusively refute a universal claim. A computational classification can establish a result over a specified finite domain. A failed proof strategy can reveal that a proposed reduction contains an unresolved obligation. A search may also suggest that an additional hypothesis is required. These outcomes should not be treated as equivalent. In particular, the inability of an agent to find a proof does not establish that a proposition is false or unprovable. Nor does the repeated failure of several agents establish that an assumption is mathematically necessary.

A meaningful negative result requires evidence appropriate to its claim. A counterexample must satisfy the stated domain and violate the relevant conclusion. A claim that no object of a particular finite class exists requires an exhaustive or otherwise valid exclusion argument. A nonexistence result over an infinite domain requires a suitable proof. This distinction matters because agentic research systems may generate increasingly large histories of unsuccessful attempts. If those histories are stored without their scope and evidentiary status, later agents may incorrectly promote exploratory failures into established mathematical constraints. Conversely, discarding unsuccessful attempts altogether encourages redundant investigation. Researchers or agents may repeatedly pursue approaches already known to encounter the same obstruction.

The appropriate representation distinguishes failed execution, inconclusive mathematical search, validated obstruction, and proved negative result. These categories have different implications for future work. A failed execution may justify rerunning a tool. An inconclusive search may motivate a different method. A validated obstruction may eliminate a particular proof strategy under specified assumptions. A proved negative result can become a durable mathematical contribution in its own right. The value of preserving such distinctions becomes especially apparent in long-running multi-agent investigations, where mathematical context must survive numerous model calls and changes in computational strategy.

From conversational coordination to structured research memory

A conventional multi-agent system often coordinates work through natural-language messages. One agent proposes an approach, another reports a partial result, and a supervising agent integrates the responses. This can be effective for short investigations, but the representation becomes fragile as mathematical work accumulates. An intermediate claim may be summarized without its assumptions. A later agent may retrieve a conclusion without the reasoning supporting it. Several agents may cite one another’s findings until an unsupported statement appears to have been independently confirmed. The problem is not simply that language models have limited context windows. It is that conversational summaries are weak representations of mathematical dependency and evidence.

Recent research-state systems attempt to address this limitation. Danus, introduced in July 2026, organizes multi-agent mathematical reasoning around a shared Fact Graph. A coordinating agent plans and distributes proof-search tasks, worker agents investigate them in parallel, and a stateless verification component examines proposed claims before they enter the shared fact memory. Admitted facts retain their proofs and dependencies, allowing subsequent reasoning to reuse them without reconstructing the complete conversation.²⁹ This is an architectural change from using a transcript as the principal mathematical memory. The persistent objects are mathematical claims and their supporting relationships, rather than only the exchanges through which those claims were generated. However, the meaning of verification must remain explicit. Danus’s verifier-gated admission mechanism should not be interpreted as making all admitted natural-language facts equivalent to kernel-checked formal theorems. Its assurance depends on the configured checking procedure.

Euler, submitted on 14 October 2026, develops the research-state approach further. It introduces a Research Graph representing open obligations, alternative proof routes, evidence, blockers, and failed approaches, alongside a Fact Graph of admitted mathematical results. Its workbench exposes these structures to researchers, who can inspect the history of an investigation and resume agent teams from saved states.³⁰ This design has two important consequences. First, it makes the mathematical state accessible independently of the conversation that produced it. A researcher can identify an unresolved lemma, examine why one route was abandoned, and investigate an alternative without relying exclusively on a generated summary.

Second, it makes the same structured state available to agents for planning and context selection. An agent need not receive every previous message; it can retrieve the relevant claims, dependencies, and earlier failures associated with its current task. Euler also distinguishes evidence types, including heuristic observations, exact finite results, checked counterexamples, model-reviewed proofs, certificate-supported results, and Lean-kernel-checked proofs. The acceptance of an intermediate claim is conditioned on its correspondence to the mathematical obligation and the specified evidence requirements. This is more than a user-interface feature. It is a mechanism for preventing the evidentiary status of a mathematical statement from changing silently as it moves through a multi-agent investigation.

The reported implementation and case studies provide evidence that such a research-state architecture can be constructed and used in mathematical workflows. They do not establish through controlled comparison that it improves the conceptual understanding of participating mathematicians. That distinction is essential for assessing the broader promise of Math 2.0.

Mathematical understanding has several subjects

When asking whether a multi-agent system increases mathematical understanding, it is necessary to identify whose understanding is being evaluated. The system may develop a more effective representation of the mathematical problem. It may preserve the relationships among claims, identify unresolved obligations, or select relevant prior results more reliably. These are observable improvements in computational research capability, even when no human learning occurs. The human–AI collaboration may instead become more capable. Researchers may solve harder problems, identify mistakes faster, or develop more reliable arguments because the system provides useful reasoning and computational assistance. Alternatively, the human mathematician may acquire greater independent mathematical understanding. After interacting with the system, the researcher may be able to reconstruct the essential argument, explain the role of an assumption, or transfer the method to a different problem without consulting the same model. The three outcomes should not be conflated.

A system can substantially improve collaborative performance while reducing the amount of reasoning the human performs independently. That may be acceptable for some research activities, particularly when the objective is to obtain a reliable result. It is a different outcome from increasing the researcher’s conceptual competence. William Thurston’s On Proof and Progress in Mathematics provides an important conceptual foundation for this distinction. Thurston argues that developing and communicating mathematical understanding is a central purpose of mathematical research, and that the accumulation of formally correct theorems does not fully describe mathematical progress.³¹ This perspective does not imply that every mathematician must independently reconstruct every proof. Modern mathematics already depends on specialized expertise, extensive formal developments, and results whose complete details exceed what any one individual can retain.

It does imply that the ability to generate correct mathematical statements should not be treated as a sufficient measure of a research community’s understanding. An AI system may make an argument accessible by constructing an explanation, but whether that explanation produces understanding remains an empirical and mathematical question.

How to test understanding rather than fluency

An evaluation should therefore examine more than the immediate quality of agent-generated explanations. A researcher could study an AI-assisted proof and later be asked to reconstruct its essential argument without access to the original assistant. Another task might change one of the theorem’s hypotheses and ask the researcher to determine whether the result still holds. A third task might require identifying the point at which a proposed generalization fails. A fourth could ask for an alternative proof using a mathematical method not employed in the original investigation. Such tasks can provide evidence about the ability to manipulate and transfer mathematical ideas rather than merely recognize their presentation. The distinction can be illustrated by the divisibility example developed later in this article. A researcher who has seen a proof that 6 divides n^3-n for every integer may remember the final result without understanding the role of consecutive integers.

A stronger indication of understanding would be the ability to explain why the factorization into three consecutive integers matters, why the proposed divisibility by 12 fails, and how related arguments might apply—or fail to apply—to other polynomial expressions. A transfer task involving n^5-n would require the researcher to adapt or replace parts of the original argument. Correctly identifying those changes would provide stronger evidence of conceptual competence than reproducing the original proof verbatim. The assessment should also distinguish immediate performance from retained understanding. A researcher may successfully complete a transfer task while the AI assistant remains available but fail when the same kind of reasoning must be performed independently.

Both results are informative. The first concerns the capability of the human–AI system. The second concerns the researcher’s independent learning. A controlled study should compare these outcomes against appropriate baselines, accounting for prior mathematical expertise, task difficulty, time spent studying the arguments, and the quality of non-AI assistance. It should also recognize that conceptual understanding may emerge through extended reflection. A single test immediately after an AI-assisted investigation cannot fully establish whether the researcher has developed a durable mathematical insight.

The problem of explanations that conceal dependence

Parallel agents may produce particularly persuasive explanations because several reasoning processes appear to support the same conclusion. The apparent independence can nevertheless be misleading. Suppose one agent proposes a lemma, a second uses it to construct a proof, and a third summarizes the completed argument. The final presentation may look like a sequence of independently developed mathematical findings, even though all three depend on one unsupported assumption. A conversational record may not make that dependence clear, especially if the original statement has been paraphrased or its hypotheses altered. A structured research-state system can expose the dependency: the final argument depends on the intermediate lemma, whose evidence has not yet satisfied the required checking procedure. This improves the inspectability of the reasoning process. It does not automatically improve the human researcher’s understanding, but it creates better conditions for critical examination.

The same applies to explanations of failed proof routes. A graph identifying exactly which obligation remained unresolved may help a mathematician understand why an attempted strategy did not succeed. Yet the graph itself does not establish that no alternative argument could resolve the obligation. Understanding depends partly on the ability to recognize the limits of what has been established. The strongest mathematical research systems should therefore preserve uncertainty as precisely as they preserve accepted results. An unresolved dependency should remain unresolved until supported by appropriate evidence, regardless of how many agents repeat the associated claim.

Could parallel agents improve understanding without increasing proof output?

The possibility is important because it suggests a research objective different from maximizing theorem-production rates. Imagine two AI-assisted environments. The first produces ten valid proofs of a difficult theorem but presents them as independent documents. The second produces only three, but explicitly identifies their essential constructions, compares their assumptions, and shows how each approach relates to established mathematical techniques. The first environment has higher proof throughput. The second may offer a better basis for conceptual synthesis, but that judgment cannot be established by counting its explanations or graph edges. An evaluation would need to determine whether researchers using the second environment can identify reusable methods, formulate useful generalizations, or apply the ideas to unfamiliar problems more effectively.

Conversely, a system that produces extensive explanatory material could burden researchers with additional reading while providing little new insight. More visible reasoning is not necessarily better reasoning. The value of exposing agent research state is therefore conditional on its mathematical structure and its usefulness to the people examining it. This is where Danus and Euler provide useful architectural hypotheses. Their persistent claim structures could allow researchers to navigate the essential dependencies of a result rather than read every agent message. Their representations could also help agents avoid repeating unproductive routes and prevent unsupported intermediate claims from being treated as accepted premises. But these are mechanisms through which understanding might improve, not measurements establishing that it has improved.

A rigorous evaluation must preserve that distinction between plausible causation and demonstrated effect.

Implications for Open Math OS

The central contribution of Ultramath is the opportunity to explore several mathematical strategies concurrently within an integrated computational environment. Its shared workspace and persistent project files make that exploration easier to organize and continue. The next architectural question is whether the resulting investigation is represented in a way that preserves its mathematical structure. Does the system distinguish accepted lemmas from provisional assertions? Can researchers identify which conclusions depend on a particular assumption? Are failed proof strategies and counterexamples recoverable without reconstructing entire conversations? Can a team revisit an earlier research state and determine why a line of inquiry was abandoned? Can mathematical results be independently checked and reused outside the original project?

The public Open Math OS documentation does not establish complete answers to these questions. Danus and Euler demonstrate that structured mathematical research-state mechanisms are technically feasible, although their specific implementations and assurance properties must be assessed independently. They suggest one direction in which an integrated environment such as Open Math OS could evolve. A more ambitious system would combine parallel exploration with evidence-aware mathematical memory, independent verification, and interfaces that allow researchers to interrogate the dependencies and conceptual structure of an investigation. Even then, the presence of those mechanisms would not establish that the system increases mathematical understanding.

The decisive question is whether researchers become more capable of reconstructing, criticizing, and extending mathematical arguments—not merely whether agents can generate and store more of them.

That question cannot be resolved through an architecture diagram or a collection of successful demonstrations. It requires controlled evaluation of mathematical correctness, strategy diversity, computational cost, knowledge reuse, human understanding, and conceptual transfer. The following section therefore turns from the mechanisms that might support Math 2.0 to the experimental methods needed to determine whether those mechanisms actually improve mathematical research.

Testing Math 2.0 with falsifiable research evaluations

The preceding analysis identifies several ways in which Open Math OS could improve mathematical research. Its integrated environment may reduce the operational cost of using AI models and scientific software. Parallel agents may explore more approaches than a sequential assistant. Persistent mathematical artifacts may enable researchers to recover previous investigations, independently examine their evidence, and reuse their results. The platform’s collaborative design may also support activities that individual mathematical assistants do not address effectively. Although these mechanisms are plausible, their existence does not establish their effectiveness.

The central methodological problem is that different definitions of success favor different architectures. A benchmark measuring the number of problems solved will tend to reward powerful mathematical reasoning and extensive search. A reproducibility test will favor environments that preserve executable artifacts. An evaluation of mathematical understanding may favor systems that support explanation, critical examination, and conceptual transfer. A governance assessment addresses properties that none of these mathematical benchmarks can measure. Consequently, Math 2.0 cannot be evaluated through a single leaderboard without reducing its objectives to whichever capabilities the leaderboard happens to measure. A meaningful research programme must instead separate the effects of model assistance, parallel-agent orchestration, persistent mathematical knowledge, and institutional research practices. It should define testable hypotheses, establish appropriate comparison groups, measure outcomes whose mathematical interpretation is clear, and permit results that contradict the architectural claims being investigated.

The following framework is a proposal for such an evaluation. It does not report an experiment conducted on Open Math OS, and none of its predicted benefits should be read as measured platform performance.

What mathematical benchmarks establish—and what they leave unmeasured

Existing mathematical AI benchmarks provide an indispensable starting point because they offer controlled tasks and, in some cases, objective acceptance criteria. The miniF2F benchmark contains formal mathematical statements drawn from competition and educational mathematics, supporting comparisons of automated theorem proving across formal systems. Its value lies in requiring systems to produce proofs of specified propositions rather than merely plausible natural-language answers.³²

PutnamBench extends formal evaluation to undergraduate competition mathematics. Its authors constructed 1,692 formalizations of 640 Putnam Competition theorems, with representations in Lean 4 and Isabelle and a substantial subset also formalized in Coq. This makes it possible to compare proof-generation systems against precisely specified mathematical obligations while exposing difficulties associated with different formal environments.³³

FrontierMath targets much harder mathematical reasoning. Its problems were designed by expert mathematicians and include original tasks drawn from advanced mathematical domains. By using newly constructed problems with relatively well-defined verification criteria, the benchmark addresses some limitations of widely circulated competition datasets, including the risk that models have encountered closely related solutions during training.³⁴ A complementary approach appears in MathArena, which evaluates models on newly released mathematical competitions and includes expert assessment of proof-writing tasks. Its methodology highlights an important distinction between producing a correct final answer and constructing a complete mathematical argument. It also provides evidence of contamination risks in evaluations based on historically available problems.³⁵ These benchmarks measure real capabilities. A model that cannot generate valid proofs or solve sufficiently demanding mathematical problems is unlikely to become a reliable research assistant merely by acquiring a sophisticated user interface.

Nevertheless, none of these benchmarks, by itself, evaluates the complete process through which mathematical research becomes cumulative knowledge. A benchmark normally supplies a problem whose mathematical objective is already defined. Research may instead require discovering that the initial objective is poorly formulated, that a conjecture is false, or that an unexpected connection makes a different question more interesting. Benchmarks also tend to terminate when a result is accepted. They usually do not examine whether another researcher can reconstruct the investigation, identify the essential idea, modify the assumptions, or build on its intermediate findings. This limitation is particularly important for Open Math OS, whose proposed value is not restricted to the mathematical capability of the underlying models. It includes the possibility that a persistent, integrated research environment creates benefits that are absent from an isolated proof-generation benchmark.

The evaluation must therefore retain established mathematical benchmarks while introducing tasks that test reproducibility, conceptual understanding, independent reuse, and control over the research process.

Four experimental conditions

A useful design would compare four research environments representing progressively different forms of assistance. The first condition, H, consists of human mathematicians using conventional research tools without generative AI assistance for the assigned investigation. The participants retain access to the mathematical literature, proof assistants, symbolic computation, and ordinary collaboration tools according to the experimental protocol. The second condition, S, adds a single AI model with a specified set of mathematical tools. It represents a conventional AI-assisted research workflow in which a human researcher interacts sequentially with one model. The third condition, A, introduces parallel-agent orchestration while preserving, as far as practicable, the underlying model, tool availability, and aggregate computational budget of condition S. It isolates the additional contribution of coordinated multi-agent investigation.

The fourth condition, K, combines the same agentic capabilities with a structured mathematical knowledge layer. This layer would preserve mathematical claims, assumptions, evidence, dependencies, failed approaches, and versioned research artifacts in a form usable by agents and human researchers. The comparison is described in Table 4.

Condition	Research environment	Principal variable introduced	Relevant comparison
H — Conventional research	Human researchers using established mathematical and collaboration tools	Baseline without generative AI	Reference for the effect of AI-assisted research
S — Single-model assistance	Human researchers using one AI assistant and specified mathematical tools	Generative mathematical assistance	S versus H: effect of the defined AI workflow
A — Parallel-agent assistance	The same underlying model and tools, with coordinated parallel agents	Agent orchestration and concurrent exploration	A versus S: incremental orchestration effect
K — Knowledge-aware agents	Parallel agents with versioned mathematical claims, evidence, dependencies, and research-state records	Structured mathematical knowledge infrastructure	K versus A: incremental effect of durable epistemic state

Table 4: Proposed research conditions for isolating the effects of AI assistance, agent orchestration, and structured mathematical knowledge. Condition K is an experimental architecture, not a claim that Open Math OS already implements every required mechanism.

The distinctions are causally important. The S–H contrast estimates the effect of the specified AI-assisted workflow relative to conventional research practice. It does not isolate model capability from every difference in interaction, training, or research behavior, because those differences are partly constitutive of the workflow being evaluated. The A–S contrast examines whether parallel agents provide benefits beyond a single assistant operating with comparable resources. If the multi-agent condition receives substantially more inference compute, superior performance cannot be attributed exclusively to orchestration. The K–A contrast is the most relevant to the article’s architectural thesis. Both environments employ comparable agents and scientific tools, but K additionally preserves mathematical research state through explicit objects and relationships.

If K performs better on independent reconstruction and reuse while the other conditions remain comparable, the result would support the proposition that structured knowledge infrastructure adds value beyond computational search. The four conditions should not be treated as a technological progression in which each must outperform its predecessor. A multi-agent system may introduce coordination overhead. A knowledge layer may impose maintenance costs that are unjustified for short tasks. Conventional research may outperform AI-assisted environments in domains where current models offer little reliable expertise. These outcomes would be scientifically informative.

The design also requires a clarification concerning Open Math OS itself. Because the public platform documentation does not establish the complete knowledge-layer mechanisms specified for K, that condition might have to be implemented as a separate prototype or integration. The experiment would then evaluate the proposed infrastructure architecture, rather than make a direct claim about existing Open Math OS functionality.

Separate the model effect from the infrastructure effect

One of the strongest potential confounders is variation in the underlying language model. Suppose a system using structured mathematical memory outperforms a conventional assistant, but also uses a more capable model checkpoint. The result would not identify whether the improvement came from the knowledge infrastructure, the model, or their interaction. The main comparison should therefore hold model versions constant wherever feasible. The study should identify the model checkpoint, inference parameters, available context, tool permissions, and relevant retrieval resources. If the agents operate through a hosted service that does not expose these properties, the resulting limitations must be disclosed.

Model improvements should be evaluated in a separate dimension. For example, the experiment could repeat selected conditions using different model families or checkpoints. This would reveal whether structured mathematical knowledge produces similar benefits across different reasoning capabilities or whether its advantages depend on a particular model. A factorial extension would be especially informative where resources permit. Investigators could vary agent orchestration and structured knowledge independently while holding the model constant. This would help distinguish the isolated effect of each mechanism from the additional benefit or cost of combining them. Such a design would also allow the possibility that persistent mathematical knowledge is useful even without parallel agents. A single model with structured memory might outperform a larger team of agents relying on unstructured conversations. That result would challenge the assumption that greater agentic complexity is the natural route toward better mathematical research infrastructure.

The evaluation tasks must represent mathematical research, not only problem solving

A research-oriented evaluation requires a task corpus with substantially greater diversity than a conventional theorem-proving benchmark. Competition problems remain useful because their correctness conditions are relatively clear and their difficulty can be estimated. However, their relevance to sustained mathematical research is limited. The problem is already formulated, its importance is determined externally, and successful completion ordinarily does not require maintaining a research programme over an extended period. The corpus should therefore include several kinds of mathematical activity.

Proof construction tasks would require the establishment of a specified theorem, possibly through a formal proof assistant. They evaluate deductive correctness, proof-search effectiveness, and computational cost.

Conjecture revision tasks would begin with a false or incomplete proposition. Participants would need to discover counterexamples, identify the assumptions responsible for failure, and formulate a valid replacement. These tasks evaluate whether the research system preserves the distinction between solving the original question and changing the question.

Research continuation tasks would provide partially completed investigations containing auxiliary lemmas, calculations, failed attempts, and unresolved obligations. Participants would be asked to continue the work without access to its original authors.

Formalization and maintenance tasks would require participants to translate an informal result into a formal system, verify the correspondence, and modify or extend the resulting development without introducing unnecessary dependencies or unmaintainable proof structures.

Open-ended mathematical investigations would address questions whose complete resolution is not necessarily known in advance. Such tasks would assess validated partial progress, useful counterexamples, well-founded conjectures, and independently judged mathematical contributions. The distinction between closed and open problems must remain explicit. For a benchmark theorem with a known formal target, correctness may be evaluated mechanically. For a research-grade open question, significance and novelty cannot be inferred from a predetermined answer key. The latter tasks therefore require independent expert evaluation and a documented process for identifying related literature. Their results may remain provisional even after a computational investigation appears successful. The evaluation should also avoid treating task novelty as a guarantee against training contamination. A problem constructed recently may be mathematically equivalent to familiar material or closely related to examples present in the model’s training data.

Controlled task generation, withheld research materials, independently developed variants, and explicit contamination analysis can reduce this risk. None eliminates it completely.

Correctness is necessary, but mathematical fidelity is a separate requirement

Mathematical correctness must remain a primary outcome. Where a complete formalization exists, the evaluation should independently execute the relevant checker under a pinned environment, inspect the accepted statement, and verify its permitted logical assumptions. However, a kernel-checked proof of a proposition does not establish that the proposition is the one the researcher intended to prove. For example, a model may introduce an additional hypothesis that makes the theorem easier, restrict a universally quantified variable to a narrower domain, or alter a definition during formalization. The resulting proof may be valid while failing to answer the original research question. This requires separate assessments of formal validity and semantic fidelity.

Formal validity concerns whether the encoded proof is accepted under the declared logical environment. Semantic fidelity concerns whether the encoded theorem corresponds to the intended informal mathematical claim. For informal proofs, qualified independent reviewers should evaluate logical completeness, the adequacy of assumptions, and the justification of critical intermediate steps. Reviewers should not be asked to infer correctness from the fluency of the final exposition or from a model’s self-assessment. The evaluation must also distinguish the verification of a mathematical conclusion from the verification of the process used to obtain it. An agent might discover a valid theorem through an irreproducible heuristic search. The mathematical result can still be independently checked and accepted, even if the original search cannot be reconstructed exactly.

Conversely, a perfectly reproducible computational procedure may produce an invalid mathematical inference. Reproducibility is evidence about the execution of the process; it is not automatically evidence that every conclusion drawn from that process is justified. The study should preserve both forms of evidence rather than using reproducibility as a substitute for mathematical correctness.

Understanding must be evaluated through conceptual transfer

The most demanding aspect of the evaluation concerns mathematical understanding. A model can generate an explanation that a researcher finds persuasive without establishing that the researcher has acquired a transferable mathematical method. Satisfaction ratings, perceived clarity, and the ability to repeat the explanation immediately after reading it are insufficient measures of deeper understanding. A stronger evaluation would examine what the researcher can do after receiving the assistance. One test would ask the participant to reconstruct the essential steps of a proof without consulting the AI system. Another would modify a theorem’s assumptions and require the participant to determine whether the result remains valid. A third would present a related problem whose solution requires adapting the original method rather than repeating its exact derivation. A fourth might ask the researcher to identify an error introduced into a plausible mathematical argument.

These tests assess different aspects of understanding: retention, recognition of essential hypotheses, critical evaluation, and conceptual transfer. They should not necessarily be combined into a single comprehension score because each addresses a distinct capability. The timing of the assessment also matters. Immediate reconstruction may reflect short-term recall. Delayed testing provides stronger evidence of retained competence, although performance will also depend on how much related mathematical work the participant has completed in the intervening period. The study should therefore distinguish assisted research performance from independent mathematical competence. A researcher may become much more productive while using an AI system without becoming more capable of solving similar problems unaided. That may represent genuine value for some professional research workflows, but it is not the same claim as an improvement in human mathematical understanding.

The distinction is central to the Math 2.0 thesis. An infrastructure that increases the number of completed proofs while leaving conceptual transfer unchanged would support a narrower productivity claim than one that demonstrably improves the ability of mathematicians to reconstruct and extend mathematical ideas.

Independent reuse is the critical test of the knowledge layer

The K–A comparison becomes most informative when evaluated through a controlled research-continuation experiment. In the first phase, a research team investigates a mathematical problem using its assigned environment. The team produces an assortment of theorems, conjectures, computations, intermediate results, failed approaches, and explanations. In the second phase, an independent team receives the preserved research materials but cannot consult the original participants. It must reconstruct the relevant claims, establish which results are accepted, identify the applicable assumptions, reproduce selected computations or formal checks, and extend one component of the research. The control condition receives conventional exported files and conversations. The knowledge-aware condition receives the corresponding artifacts together with stable claim identities, explicit evidence records, typed dependencies, and structured research-state information. The comparison should preserve the substantive mathematical content available to the receiving teams. Otherwise, a better result for K might simply reflect access to more information rather than the value of its organization.

The principal outcome would be whether independent researchers can reconstruct and continue the investigation correctly and efficiently. Failures should be classified by cause. A team might be unable to locate the correct theorem version, reconstruct a missing computational dependency, understand the role of a definition, or determine why an earlier conjecture was abandoned. These failures have different architectural implications. A missing software dependency suggests a reproducibility problem. An ambiguous theorem statement suggests inadequate semantic preservation. An inaccessible counterexample suggests a deficiency in research-state representation. A misunderstood proof strategy may instead reveal a problem of mathematical exposition.

The experiment should therefore record not only whether the continuation succeeds, but also which information was required and where reconstruction failed. This is the clearest test of the hypothesis that mathematical knowledge infrastructure creates value beyond persistent conversations and project files. If the structured knowledge condition does not materially improve independent continuation, its additional complexity may not be justified for the tested class of research activities.

Measure cost, including the cost of verification

The resource comparison must extend beyond model inference. Parallel agents may complete a task more quickly in elapsed time while consuming substantially more compute. A structured knowledge layer may reduce future reconstruction effort while imposing substantial costs during artifact creation. Human verification is another important resource. A system that generates many candidate mathematical claims may shift effort from proof discovery to reviewing, correcting, and rejecting unsupported results. An evaluation limited to agent execution time would conceal that transfer of work. The study should therefore account for model inference, scientific tool execution, human interaction, verification, correction, maintenance, and the cost of preparing reusable artifacts. These costs should not be collapsed into an arbitrary universal currency when their scientific implications differ.

Wall-clock time measures elapsed completion. Compute expenditure measures computational resources. Human review time measures demands placed on mathematical expertise. The time required to reproduce a result measures a different aspect of its downstream usability. An integrated system may improve one dimension while worsening another. Such trade-offs should be reported explicitly. Resource matching is particularly difficult for parallel agents. Equal token counts do not guarantee equal accelerator usage, and equal elapsed time does not guarantee equal expenditure. Where exact normalization is impossible, researchers should report several resource measures and compare outcomes across predefined budget levels. A system that produces more correct theorems only by consuming disproportionately greater resources may still be useful, but its value must be evaluated under an explicit economic and scientific objective.

Outcomes, statistical design, and falsification

The study should use a multidimensional outcome framework, summarized in Table 5.

Outcome	Proposed measurement	Interpretation limit
Mathematical correctness	Independently accepted proofs, valid counterexamples, semantically faithful formalizations	A formally correct result may encode the wrong intended claim
Research efficiency	Validated outputs, elapsed time, compute cost, human review and correction effort	Faster completion does not imply lower resource consumption
Reproducibility	Independent reconstruction of computations and proof environments	Stochastic discovery processes may not be exactly repeatable
Conceptual understanding	Reconstruction, critique of assumptions, delayed unassisted transfer	Persuasive explanation does not establish retained competence
Knowledge reuse	Independent team successfully verifies and extends prior work	Depends on task selection, researcher expertise, and available background knowledge
Research fertility	Validated generalizations, new counterexamples, useful successor questions	Long-term significance may become apparent only much later
Research authority	Permission enforcement, project portability, documented governance and allocation decisions	Published institutional commitments are not evidence of technical enforcement

Table 5: Prospective outcome measures for evaluating Math 2.0 research environments. The dimensions should be analyzed separately rather than combined into a universal productivity score.

A confirmatory experiment should preregister its principal hypotheses, inclusion criteria, task-selection procedures, resource constraints, statistical analyses, and practical thresholds for meaningful effects. Researchers or research teams should be randomly assigned to the experimental conditions, with assignment stratified where appropriate by mathematical expertise, prior use of proof assistants, familiarity with AI, and task difficulty. For longer collaborative investigations, randomization should ordinarily occur at the team level. Assigning members of the same collaborating team to different conditions risks contamination because mathematical strategies and AI-generated results can be communicated across treatment boundaries. A crossover design can improve efficiency for short tasks, but it is less suitable for evaluating retained mathematical understanding. A researcher cannot necessarily forget a technique learned while using one environment before beginning a supposedly independent task in another condition.

The statistical analysis must respect the experimental unit and the possibility that multiple tasks undertaken by the same participant or team produce correlated outcomes. Effect estimates should be accompanied by uncertainty intervals and sensitivity analyses, with sample sizes justified through the primary outcome and a prospective power or precision calculation. The most important falsification conditions should also be specified before the experiment. If A produces no meaningful benefit over S after accounting for additional computational resources, the claim that parallel orchestration improves research efficiency would be weakened for the tested setting. If K does not improve independent reconstruction or reuse relative to A, the claim that its structured knowledge layer provides additional epistemic value would be weakened.

If AI-assisted environments increase immediate proof completion but reduce researchers’ performance on delayed unassisted transfer tasks, the evaluation would identify a tension between collaborative productivity and independent mathematical competence. If a platform cannot export sufficient evidence to reconstruct its accepted results, a claim of full scientific portability would fail the relevant operational test. Statistical non-significance alone does not establish the absence of a benefit. Claims of practical equivalence or inferiority require appropriately designed comparisons and predefined margins. Similarly, positive findings on a narrow task corpus should not be generalized automatically to mathematical research as a whole. The objective is not to prove that one architecture is universally superior. It is to identify which mechanisms improve which mathematical activities, under which conditions, and at what cost. Such a research programme would move the evaluation of Math 2.0 beyond demonstrations of mathematical AI capability toward evidence about the organization of mathematical discovery itself.

Competing architectures for mathematical AI

Open Math OS is part of a rapidly developing mathematical AI ecosystem whose constituent projects do not all pursue the same objective. Some prioritize the mathematical capability of increasingly powerful models. Others construct reliable formal proof systems and reusable theorem libraries. Agentic research frameworks attempt to coordinate extended investigations, while semantic knowledge systems seek to preserve relationships among mathematical objects. At the institutional level, mathematicians and research foundations are beginning to organize procedures for reviewing, understanding, and assimilating AI-generated results. These approaches are related but should not be evaluated as interchangeable products. The central architectural difference concerns where mathematical knowledge resides, what establishes the validity of its claims, and who has authority to accept and maintain them.

In a model-centered system, substantial computational capability resides in the model and its inference environment. In a formal library, the durable mathematical object is a declaration accompanied by a derivation checked under a specified logical system. In a research-state architecture, the evolving investigation becomes an explicit computational object. In a mathematical commons, accepted contributions must remain usable independently of the particular model or institution through which they originated. The distinctions determine what survives when the original computational process ends.

Frontier-model research: the model as the principal producer

The most visible development in mathematical AI has been the increasing ability of frontier language models to solve difficult mathematical problems. Google DeepMind’s work illustrates this trajectory. Its AlphaProof and AlphaGeometry systems used specialized mathematical representations and reasoning mechanisms, while subsequent versions of Gemini Deep Think demonstrated strong performance on competition-level problems using natural-language mathematical reasoning. By February 2026, DeepMind had described Aletheia, a mathematical research agent based on Gemini Deep Think that integrates problem-solving, natural-language verification, revision, and literature retrieval.³⁶ The system uses a generator–verifier–reviser loop. A model produces a candidate solution, a natural-language verifier examines it, and the result may be accepted, revised, or rejected in favor of a new attempt. This arrangement is important because it incorporates criticism into the computational research process rather than relying on the first generated argument.

DeepMind also reports work on research-level mathematical questions, including applications to arithmetic geometry, combinatorics, and problems related to Erdős conjectures. The company distinguishes different degrees of AI autonomy and proposes classifications of the scientific significance of reported contributions. These classifications reflect an important limitation of benchmark-based evaluation. A mathematical result can be difficult for an AI system to obtain without constituting a major advance for the mathematical community. The architecture nevertheless remains primarily oriented around frontier reasoning capability. Its most significant component is the model, together with the inference-time procedures that generate, criticize, and revise mathematical arguments. The resulting research contribution may subsequently require independent formal checking, human review, publication, or conceptual interpretation.

Aletheia’s verifier should not be confused with a formal proof kernel. A language-model critic can identify mathematical mistakes and improve the reliability of generated arguments, but its acceptance of a proof is not equivalent to independently checking an encoded derivation against the rules of a specified formal system. This distinction is not a criticism of the usefulness of natural-language verification. It identifies the scope of its assurance. A model-based verifier can be effective at detecting flawed arguments, proposing corrections, and selecting promising lines of inquiry. A trusted formal checker addresses a narrower but stronger question: whether a particular formal derivation is valid under its declared logical assumptions.

A future research environment may therefore need both forms of verification.

OpenAI’s October 2026 release: mathematical production and the limits of assimilation

OpenAI’s announcement of 6 October 2026 provides another example of a model-centered mathematical research programme, with unusually direct implications for the mathematical community. The company published a broad collection of mathematical results generated by an internal frontier model, accompanied by manuscripts and selected research artifacts in a public repository. The release includes Lean formalizations for some results, information about computational expenditure, selected summaries of the model’s reasoning, and procedures for revisions and citations.³⁷ Rather than merely reporting performance on predefined tasks, as conventional benchmarks do, the release introduces a collection of mathematical arguments that researchers must examine as potential contributions to the literature. That changes the relevant scientific problem. Producing a candidate result is only one stage in determining whether it is mathematically correct, novel, significant, and useful for further inquiry.

The accompanying formalizations provide an important form of evidence where they are complete and independently checkable. However, the presence of some formalized proofs does not establish the correctness of every manuscript in the collection. Nor does a public repository make the complete generative process independently reproducible. The internal model responsible for producing the results was not released for independent execution at the time of the announcement. OpenAI stated that it was working toward a responsible release of the model, while sharing selected information about the process used to obtain the results. This yields a useful distinction among three forms of reproducibility.

A researcher may be able to verify the result by checking an associated formal proof. The researcher may be able to reconstruct part of the research process from disclosed prompts, summaries, and artifacts. Yet neither capability necessarily allows the researcher to reproduce the original generation process using the same model and computational environment. These are distinct scientific properties. For a valid mathematical theorem, independent proof checking can be sufficient to establish deductive correctness even when the original discovery procedure is unavailable. But understanding why the theorem matters, whether its methods are novel, and how it relates to the literature requires additional investigation.

OpenAI’s release therefore illustrates a central concern of Math 2.0: mathematical AI may increase the rate at which potentially important results appear without increasing the community’s capacity to interpret and assimilate them at the same rate. The bottleneck shifts from producing candidate proofs toward independently determining what mathematical knowledge has actually been created.

Formal proof libraries: mathematics independent of the producer

A different architectural philosophy is represented by Lean and Mathlib. In this approach, the fundamental persistent object is not a model-generated answer or an agent conversation. Rather, it is a formal mathematical declaration whose proof can be checked under specified rules and assumptions. The system that proposes the proof need not be trusted in the same way as the checker. A human mathematician, a specialized automated theorem prover, or a language model may construct a candidate derivation. Its validity is determined by the formal checking process rather than the reputation or reasoning narrative of its producer. This separation is especially powerful in an AI-assisted research environment because models can generate many candidate proofs, some of which are incorrect. A formal checker can reject invalid derivations without requiring the model to recognize every one of its mistakes.

The assurance remains limited to the encoded proposition and its declared logical environment. A correctly checked theorem may still differ from the intended informal statement, while the novelty and conceptual importance of the result require other forms of assessment. Mathlib extends formal verification into an organized and maintained mathematical library. Its contribution procedures, repository history, dependency structures, and review practices allow mathematical objects to be reused and extended across projects and contributors. The central challenge is therefore not only generating proofs that pass the checker, but organizing formal mathematics so that it remains understandable and maintainable.

A large library can accumulate numerous technically valid declarations while becoming difficult to navigate or extend. Definitions may be unnecessarily specialized, similar results may be duplicated, and automatically generated proofs may rely on unwieldy collections of intermediate lemmas. The relevance of these concerns was reinforced on 16 October 2026 by Jeremy Avigad, Kevin Buzzard, Johan Commelin, Rémy Degenne, Kim Morrison, Oliver Nash, and Adam Topaz in How to Formalize All of Mathematics. Their argument distinguishes the volume of formalized mathematical statements from the construction of libraries that can support subsequent mathematical work.³⁸ This provides a useful counterpoint to model-centered mathematical AI.

A frontier model may produce an impressive result whose verification and interpretation remain to be completed. A formal library may preserve comparatively modest results in a form that thousands of later developments can reuse. Neither contribution can be evaluated adequately through the number of new theorems generated in a short period. The architectural complementarity is substantial. Open Math OS can use Lean and Mathlib as tools for formal verification, while a verified mathematical contribution can remain available through independently maintained formal infrastructure after the original Open Math OS project has ended. That independence is one of the strongest foundations for a future mathematical commons.

Research-state systems: preserving the investigation, not only its conclusion

Another architectural approach treats the evolving mathematical investigation as an object that can be represented, queried, and continued. Danus, introduced in July 2026, organizes coordinated mathematical agents around a shared Fact Graph. A central agent plans investigations, worker agents pursue proof tasks, and proposed intermediate facts pass through a verification component before entering the shared memory. The graph preserves claims together with supporting arguments and dependencies.³⁹ This helps address a problem that becomes significant during long mathematical investigations: intermediate findings may be lost or distorted as agents generate new conversations and earlier reasoning moves outside the available context.

Instead of relying entirely on conversational summaries, a fact graph makes accepted intermediate claims independently retrievable. Euler, submitted on 14 October 2026, develops the approach further. It uses a structured research representation containing open obligations, alternative strategies, failed approaches, mathematical dependencies, verification evidence, and preserved states from which researchers can resume an investigation.⁴⁰ The distinction between Danus and Euler is instructive. Danus emphasizes the organization of admitted intermediate mathematical facts for long-horizon agent reasoning. Euler additionally emphasizes the structure of unfinished mathematical work and provides a researcher-facing workbench for inspecting the investigation and revisiting earlier approaches.

Both architectures address a problem that is only partly solved by conventional project persistence. Whereas a saved conversation records what agents said, a structured research-state representation can also record which mathematical claims were proposed, what evidence supports them, which obligations remain open, and why an attempted strategy was abandoned. This is especially relevant when different agents share partial results. Without explicit evidentiary distinctions, an unsupported claim can propagate through several reasoning steps and acquire the appearance of an established premise. A research-state graph can make the chain of dependence visible and require appropriate checking before a claim is reused. These systems do not eliminate the mathematical limitations of model-based verification. The assurance associated with an admitted fact depends on its checking mechanism, which may differ from the guarantee supplied by an independent proof assistant. Nor do their published case studies establish that researchers using them develop deeper conceptual understanding.

They nevertheless show that the research process itself can be represented more precisely than through a collection of chat transcripts. This suggests a natural complement to Open Math OS. The integrated workspace provides models, tools, persistent computation, and collaboration. A structured research-state layer could preserve the mathematical relationships connecting the activities performed within that workspace. Whether the combined architecture improves research efficiency and understanding remains a question for the experimental evaluation developed in the preceding section.

Mathematical knowledge infrastructure: beyond the research session

A research-state system and a mathematical knowledge infrastructure solve related but distinct problems. The former organizes an ongoing investigation, whereas the latter preserves contributions so that researchers outside the original project can discover, verify, and reuse them. Mathlib provides an established example of durable formal knowledge within a particular proof-assistant ecosystem. MMT investigates modular representations that can support interoperability across mathematical foundations. TheoremGraph and related research explore large-scale mathematical dependency and retrieval structures. These systems differ in their representations and assurance models, but they share an objective that extends beyond remembering an agent’s previous activity.

A durable mathematical contribution should retain its identity, statement, assumptions, evidence, and relationships after the original computational process has ended. This requirement becomes particularly important as model-generated mathematics increases in volume. Without stable artifact identities and typed relationships, independent researchers may face an expanding collection of files, manuscripts, and explanations whose mathematical status is difficult to determine. Semantic retrieval can help locate potentially relevant material, but it cannot establish deductive implication merely by identifying textual or embedding similarity. Formal proof checking can validate particular derivations, but it does not automatically organize the conceptual relationships among different results. The relevant architecture should therefore support several forms of evidence simultaneously while preventing weaker forms of evidence from being presented as stronger ones.

A mathematical knowledge graph could connect formal dependencies, reviewed semantic correspondences, counterexamples, generalizations, and historical contributions. Its effectiveness would depend on preserving the different evidentiary status of those relationships. Such a system need not be operated by the same organization that hosts the models producing the research. Indeed, independent maintenance and interoperability may be important requirements if the objective is to prevent mathematical knowledge from becoming dependent on one provider’s computational infrastructure.

Institutional assimilation: mathematics still requires a community

The preceding architectures address the technical production, checking, organization, and preservation of mathematical material. They do not fully address the work through which mathematical results become part of a discipline’s shared understanding. On 29 September 2026, the independent Advisory Group on Mathematics and Artificial Intelligence published recommendations concerning the responsible release of AI-generated mathematical results. The group distinguished work that a responsible human mathematician already understands from results whose arguments have not yet been adequately assimilated by the people involved in their production.⁴¹ For the latter category, its recommendations emphasize better mathematical exposition, attribution, independent repositories, disclosure of relevant computational information, formalization where feasible, and support for subsequent human understanding.

The group also argues that the development of such understanding should remain directed by the mathematical community rather than by the laboratories that generated the results. This is an important institutional separation. A laboratory may possess the technical capability to produce many mathematical arguments. It does not follow that the laboratory should control the standards by which those arguments are evaluated, determine their scholarly significance, or direct the research programmes needed to interpret them. The mathematical community has existing institutions for these purposes: journals, scholarly repositories, research groups, workshops, conferences, libraries, and educational programmes. These institutions may need additional resources and new practices to accommodate AI-generated mathematics, but they are not rendered obsolete by the computational systems that produce it.

The institutional distinction became especially concrete on 15 October 2026, when the Simons Foundation announced a partnership with Anthropic and OpenAI involving $15 million in combined funding and resources to help mathematicians evaluate AI-assisted results, learn and use new tools, organize collaborative activities, and develop shared practices.⁴² The Simons Foundation stated that it would manage and award the funding, including through an open call for proposals. Anthropic and OpenAI would also provide models and computing resources to supported researchers. OpenAI separately identified its $5 million contribution to the initiative in an update to its 6 October mathematics announcement. That contribution is part of the overall partnership, not an additional amount to be added to the announced $15 million.

The institutional structure is significant because it separates the organizations supplying AI resources from the foundation responsible for administering the research support. That arrangement does not automatically guarantee independence. Its effectiveness depends on grant conditions, selection procedures, governance, and the research activities actually supported. As of 16 October 2026, the initiative had been announced but its scientific outcomes could not yet be assessed. Nevertheless, it addresses a scarcity that improvements in inference capability cannot automatically eliminate: the time and expertise required to understand, criticize, communicate, and extend mathematical results. This represents a different approach to Math 2.0 from building a comprehensive mathematical research workspace.

It seeks to strengthen the institutions through which mathematical understanding is produced and maintained, rather than integrate every activity into one technical platform.

Open Math OS occupies a distinctive position

Against this landscape, Open Math OS occupies an interesting intermediate position. Its current technical design resembles an integrated mathematical research workbench: users have access to AI models, parallel agents, scientific computing tools, persistent files, and collaborative projects. Its institutional ambition extends beyond that workbench. SAIR proposes open mathematical models, community participation in development, research-data control, and donated computing resources intended to reduce dependence on commercial providers. The two propositions should be assessed separately. The workbench can be evaluated through usability, mathematical task performance, resource efficiency, reproducibility, and the quality of collaborative workflows. The institutional programme requires evidence concerning licenses, independent deployability, data-use permissions, resource allocation, researcher control, and governance procedures.

Neither proposition establishes that Open Math OS already provides the durable mathematical knowledge layer described earlier. The comparative landscape makes clear that such a layer can be developed through interoperability rather than exclusive vertical integration. An Open Math OS project could export formal developments to maintained proof libraries, exchange versioned research artifacts with independent repositories, and rely on scholarly institutions for publication and interpretation. This would preserve the platform’s operational advantages without requiring SAIR to become the sole authority over the mathematical record created using its tools. The resulting division of responsibilities is summarized in Table 6.

Architectural model	Representative examples	Primary object or activity	Principal assurance or authority	Main limitation relative to Math 2.0
Frontier-model mathematical research	Gemini Deep Think, Aletheia, OpenAI mathematical research models	Candidate proofs, conjectures, research arguments	Model-assisted criticism, external review, formal checking where available	Mathematical production does not establish durable understanding or independent reproduction of discovery
Formal proof infrastructure	Lean, Mathlib	Formal statements, checked proofs, maintained declarations	Trusted checking mechanisms and formal-library review	Deductive validity does not establish conceptual significance or cover every stage of exploration
Agentic research-state systems	Danus, Euler	Intermediate facts, obligations, failed approaches, research dependencies	Evidence-gated research-state management	Structured investigation does not automatically demonstrate increased human understanding
Mathematical knowledge infrastructure	MMT, TheoremGraph, formal dependency services	Versioned statements, formal–informal links, mathematical relationships	Evidence-qualified dependencies and maintained representations	Semantic relationships and cross-system interoperability remain difficult
Integrated mathematical workspace	Open Math OS	Shared research projects, computation, agents, files, collaboration	Researcher review, available mathematical tools, platform policies	Persistence and integration do not automatically establish independent verification or epistemic portability
Institutional assimilation	AGMAI recommendations, Simons Foundation initiative	Scholarly review, interpretation, education, community coordination	Independent mathematical judgment and institutional governance	Institutional activity does not replace computational tools or formal assurance

Table 6: Comparison of the principal architectural approaches to mathematical AI as of 16 October 2026. The systems address different responsibilities and cannot be ranked meaningfully through a single problem-solving benchmark.

The central trust boundaries

The comparison identifies several distinct forms of trust. A model’s apparent ability to reason mathematically is not the same as independent assurance that a particular proof is correct. A proof assistant’s acceptance of a derivation is not the same as evidence that the theorem represents the intended informal claim. A structured research history is not the same as a durable mathematical knowledge base. A public repository is not necessarily a community-governed institution, and a free hosted service is not necessarily independently reproducible. These distinctions matter because mathematical AI systems increasingly combine capabilities that are technically compatible but epistemically different.

An agent may generate a conjecture, run numerical experiments, search the literature, produce a natural-language proof, and construct a formal derivation within one workflow. A unified interface is convenient, but it can make the evidentiary differences between those operations less visible unless the system represents them explicitly. An architecture suitable for cumulative mathematical research should preserve those differences. In particular, the system producing a mathematical claim should not be the sole authority determining whether the claim is valid or scientifically significant. Verification records should identify the mechanisms on which they depend. Scholarly publication should preserve independent review and attribution. Mathematical artifacts should remain usable when the model or provider that generated them is no longer available. This is the main architectural lesson of the comparison.

The strongest future environment may combine frontier mathematical reasoning, formal checking, structured research memory, semantic knowledge management, and independent institutions. But their integration should not erase their distinct responsibilities.

Integration without monopoly

Open Math OS’s advantage lies in reducing fragmentation. A mathematician benefits from an environment in which model-assisted reasoning, scientific computation, formalization, and collaboration do not require constant manual transfer of files and context. There is a genuine engineering value in this integration. However, the same benefits need not require all mathematical knowledge to be stored and governed by one platform. An integrated research workspace can invoke a formal proof checker maintained by an independent community. It can register mathematical artifacts in a portable repository. It can retrieve semantic relationships from external knowledge services and submit results to scholarly institutions with their own review procedures. The resulting architecture would be more heterogeneous than a single vertically integrated system, but its components could provide distinct assurances and remain replaceable as their technologies evolve.

This arrangement also creates costs. Independent services require interoperable formats, stable identifiers, compatible access policies, and procedures for resolving inconsistent metadata or competing mathematical interpretations. Federation does not eliminate technical or institutional governance. It changes where those responsibilities reside. The relevant objective is not maximal decentralization for its own sake. It is preserving mathematical correctness, interpretability, and research autonomy without creating unnecessary dependence on a particular model, interface, or organization. The developments of October 2026 suggest that the capabilities required for such an ecosystem are emerging through several distinct programmes rather than one unified project.

Open Math OS contributes an integrated operational environment. Frontier laboratories contribute increasingly capable mathematical reasoning systems. Formal proof communities supply trusted checking and maintained mathematical libraries. Research-state systems investigate the representation of extended reasoning and failed approaches. Independent scholarly initiatives begin addressing the human and institutional costs of assimilating machine-generated mathematics. Their combination could be substantially more important than any one component considered separately. The architectural challenge is to make that combination reliable. The next section therefore develops a reference architecture for mathematical research infrastructure in which production, verification, mathematical knowledge preservation, and scholarly authority remain explicit and interoperable responsibilities. Such an architecture would allow systems like Open Math OS to contribute to a mathematical commons without requiring them to become the exclusive custodians of the mathematics they help produce.

Toward a mathematical research infrastructure

The comparison of existing mathematical AI architectures reveals a recurring asymmetry. Systems are becoming increasingly capable of generating mathematical material, but the mechanisms through which that material becomes reliable, interpretable, and reusable remain distributed across separate tools and institutions. A frontier model may produce a proof candidate; a formal proof assistant may verify a particular derivation; a scientific computing environment may generate supporting evidence; and a mathematician may establish the relationship between those results and the broader literature. Yet the connections among these activities are often preserved only through documents, software repositories, and conversational histories.

Open Math OS addresses part of this fragmentation by bringing models, agents, computation, and collaboration into a persistent workspace. The proposed next step is more demanding: an infrastructure in which the mathematical contributions produced through those activities retain their identity, evidence, meaning, and dependencies independently of the environment that generated them. This is not a proposal to replace mathematical papers, formal libraries, or existing scholarly institutions with one universal platform. Nor is it an architecture attributed to the current implementation of Open Math OS. It is a reference model intended to identify the responsibilities a future Math 2.0 infrastructure would have to support, the interfaces connecting them, and the boundaries that should remain independently verifiable.

The central design principle is to make the mathematical contribution, rather than the model conversation or computational session, the durable object around which the infrastructure is organized.

Separate mathematical production, assurance, and authority

The proposed architecture begins by distinguishing three responsibilities that are frequently combined within an AI-assisted workflow. Production consists of the activities through which mathematical material is generated. Researchers formulate questions, agents propose approaches, symbolic systems explore examples, programs test conjectures, and proof assistants help construct formal derivations. These activities can involve uncertain, provisional, or incorrect statements because their purpose includes exploration.

Assurance concerns the evidence supporting a particular mathematical claim. A formal checker can establish that a proof term is valid under a specified logical environment. An independent computation can confirm that a numerical experiment produces an expected result under reproducible conditions. A mathematical reviewer can assess whether a formal theorem faithfully represents an intended informal proposition.

Authority determines who may initiate research, authorize access to unpublished material, allocate resources, accept results into a shared library, publish contributions, or issue corrections. Authority is institutional and procedural; it does not follow automatically from a model’s mathematical capabilities. These responsibilities must remain distinguishable even when the same software interface exposes all three. Suppose an agent produces a Lean proof and reports success. That report is an output of mathematical production, not an independently established verification record. The assurance layer must identify the exact theorem, reconstruct the relevant environment, and perform the required checking procedure.

Even if the derivation is accepted, the result should not automatically become a published mathematical contribution. The correspondence between the formal statement and the intended theorem, its originality, and its scientific relevance remain separate questions. The distinction prevents several forms of circular assurance. An agent should not establish the correctness of its own proof merely by declaring that the proof is correct. A model-generated explanation should not certify the interpretation of the theorem simply because it is persuasive. And a system capable of publishing a result should not be presumed authorized to disclose unpublished research.

The aim is not to exclude AI from verification or mathematical judgment. AI systems can assist with both. The requirement is that their outputs carry evidence appropriate to their actual checking procedures and that consequential decisions remain attributable to the parties authorized to make them.

The proposed reference architecture

The architecture can be decomposed into six cooperating technical and institutional functions. The research authority function identifies the research objective, responsible researchers, available resources, data permissions, and operations delegated to agents. Its controls should distinguish, for example, permission to read an unpublished manuscript from permission to publish it or use it for model training. The agent orchestration function organizes investigations. It selects tasks, coordinates models, retrieves mathematical context, records proposed approaches, and preserves unresolved obligations. Its principal working representation is a research-state graph rather than solely an accumulating conversation. The scientific execution function provides controlled environments for formal proof development, symbolic computation, numerical experiments, and other mathematical tools. It records the inputs, execution configuration, and outputs needed for appropriate reconstruction.

The assurance function examines claims using identified verification mechanisms. Formal derivations, computational findings, semantic correspondences, and scholarly interpretations require different evidence. The assurance layer must preserve those distinctions. The mathematical knowledge function registers durable contributions with stable identities, exact revisions, supporting evidence, dependencies, corrections, and links to alternative interpretations. Its knowledge graph connects mathematical objects rather than merely indexing project files. Finally, the scholarly function concerns attribution, independent review, dissemination, maintenance, correction, and eventual assimilation into mathematical research. Its operators and decision-making procedures need not belong to the provider hosting the original computational investigation. The relationships are represented in Figure 2.

%%{init: {"theme":"neo","look":"handDrawn","layout":"elk"}}%%
flowchart TB
    R[Researcher or research team]
    P[Permissions and data policy]

    subgraph RESEARCH["Research and computational production"]
        A(Agent planning and orchestration)
        T[Scientific mathematical tools]
        S[(Research-state graph)]
        C[(Candidate contributions)]
    end

    subgraph ASSURANCE["Independent assurance boundary"]
        V(Formal checking)
        M(Semantic and mathematical review)
        E[(Typed evidence records)]
        G{Status-specific release criteria met?}
    end

    subgraph KNOWLEDGE["Durable mathematical knowledge"]
        K[(Versioned artifact registry)]
        L[(Mathematical knowledge graph)]
    end

    subgraph SCHOLARLY["Independent scholarly authority"]
        I[Scholarly reviewers]
        U[(Published scholarly record)]
    end

    R -->|authorizes objectives| A
    P -.->|constrains operations| A
    P -.->|constrains access| K
    A -->|invokes| T
    A -->|records investigations| S
    S -->|supplies research context| A
    T -->|produces outputs| C
    S -->|selects durable findings| C
    C -->|submits formal artifacts| V
    C -->|submits claims and interpretations| M
    V -->|records checking evidence| E
    M -->|records assessment| E
    E -->|supplies qualification evidence| G
    G -->|criteria satisfied| K
    G -->|revision required| A
    K -->|indexes typed relationships| L
    K -->|submits contribution| I
    I -->|accepts for publication| U
    L -->|supplies reusable results| A

Figure 2: Proposed Math 2.0 research infrastructure. Computational production, independent assurance, durable mathematical knowledge, and scholarly acceptance remain separate responsibilities, while validated results and unresolved obligations can inform subsequent investigations.

The diagram represents a logical architecture, not a verified Open Math OS deployment topology. It does not prescribe specific databases, orchestration frameworks, cloud providers, container runtimes, or proof assistants. Its boundaries have stronger meaning than the boxes themselves. In particular, an agent execution should not replace the verification evidence issued by an independent checker, nor should subsequent edits silently modify a validated theorem. A semantic similarity suggested by a model must not become an established deductive dependency, just as a contribution must not become public automatically because it passed a technical check. The architecture also distinguishes registration from publication. A researcher may preserve a conjecture as a durable object without claiming to have proved it. A valid counterexample can be registered as evidence refuting a conjecture. A formally checked theorem may be preserved in a private research repository before being submitted for scholarly review.

The release criteria must therefore depend on the artifact’s declared status. There should be no universal gate requiring every preserved mathematical idea to be formally proved.

The mathematical artifact as a durable unit of knowledge

The reference architecture requires an explicit contract for the mathematical objects exchanged between its components. A minimally useful mathematical artifact must identify the contribution and its exact revision, together with the statement, relevant mathematical context, evidence, dependencies, provenance, and lifecycle information. These properties have different roles. A contribution identifier enables references to a developing mathematical result across successive revisions, whereas a revision identifier fixes an exact statement and its associated evidence; a content digest, by contrast, identifies a particular serialized object and detects changes to its bytes. The distinctions matter because a content digest is not the mathematical identity of a theorem.

Two proof files can have different hashes while establishing the same proposition. Conversely, superficially similar theorem names can refer to statements with different hypotheses, definitions, or type parameters. Determining whether two mathematical claims are equivalent may itself require a proof. A useful artifact contract should therefore preserve exact formal representations without assuming that syntactic identity, logical equivalence, and conceptual identity are interchangeable. The following simplified structure illustrates the proposed data model. It is a conceptual contract, not an Open Math OS API.

contribution:
  id: "urn:math-example:contribution:cubic-divisibility"
  revision: "rev-2"
  status: "proved"

statement:
  informal: "Six divides n cubed minus n for every integer n"
  formal_representation:
    system: "Lean 4"
    declaration: "CubicDivisibility.divisible_by_six"
    source_artifact: "proof-source-rev-2"

evidence:
  - id: "check-001"
    type: "formal_kernel_check"
    checked_statement: "CubicDivisibility.divisible_by_six"
    environment_manifest: "lean-environment-001"
    axiom_report: "axioms-001"
    result: "accepted"

dependencies:
  - target: "urn:math-example:contribution:consecutive-integers"
    relation: "uses_mathematical_method"
    evidence: "review-002"

provenance:
  investigation: "research-session-001"
  responsible_research_team: "team-001"
  source_revision: "proof-source-rev-2"

release:
  visibility: "project"
  mathematical_status: "formally_checked"
  scholarly_status: "not_peer_reviewed"

The example deliberately separates mathematical status from scholarly status. A kernel-checked derivation may remain unpublished, while a manuscript can be published without every theorem being machine-checked. The states describe different dimensions rather than mutually exclusive positions on one scale. A production contract would need further precision. It would specify identifier syntax, schema versions, permitted evidence types, reference integrity, signature validation where relevant, authorization rules, and the treatment of corrections and withdrawals. The environment manifest must be concrete enough for independent reconstruction. For Lean, this may include the selected toolchain, package configuration, resolved Mathlib revisions, imported modules, and the checker used to examine the proof.

The Lean build system Lake records resolved dependency revisions in lake-manifest.json, providing an existing mechanism that can support reproducibility of formal developments.⁴³ The artifact contract should refer to such established mechanisms rather than invent an entirely new build system for mathematical proofs.

Evidence must be typed rather than reduced to one confidence score

A research infrastructure will receive evidence from several sources, each supporting a different kind of claim. A numerical search may establish that a conjecture holds for every integer in a finite interval. A symbolic algebra system may derive an identity. A Lean checker may accept a formal derivation. An expert mathematician may review the correspondence between that derivation and an informal statement. These findings cannot be represented adequately through one undifferentiated verified flag. A formally checked theorem has a strong guarantee concerning derivability under its encoded assumptions. The guarantee does not establish whether the theorem is novel or significant. An independent computational reproduction establishes that a stated calculation can be reconstructed under specified conditions; it does not convert a finite experiment into a proof of an infinite universal claim. Likewise, a semantic review may provide good evidence that a formalization captures an intended theorem without supplying the mechanical certainty of a proof checker.

An artifact could therefore possess several evidence records with different scopes.

Evidence type	What it can support	What it does not establish
Formal proof checking	Validity of an exact formal derivation under identified assumptions	That the encoded proposition is the intended theorem, or that it is novel
Computational reproduction	Reproduction of a specified mathematical computation	Universal validity beyond the computation’s scope
Counterexample validation	Falsity of a particular universal statement	Truth of every proposed replacement statement
Semantic correspondence review	Reviewed relationship between formal and informal mathematical representations	Deductive correctness independently of the supporting proof
Scholarly review	Assessment of correctness, exposition, originality, or significance under stated criteria	Mechanical verification of every proposition
Provenance attestation	Evidence connecting artifacts, operations, and responsible actors	Mathematical truth, ownership, or scholarly priority by itself

Table 7: Proposed assurance distinctions for mathematical artifacts. Verification mechanisms support different claims and should not be collapsed into one universal confidence score.

This representation also enables evidence-sensitive retrieval. A researcher looking for formally checked theorems should be able to exclude provisional model judgments. An agent investigating a conjecture may legitimately retrieve computational hints, but it should know that those hints are not established premises. A scholarly reviewer may need the informal explanation and historical context in addition to the formal proof. The infrastructure becomes more reliable when users can select the evidence standard appropriate to their task.

Provenance and reproducibility are related but distinct

Provenance concerns how a mathematical artifact came to exist: which inputs were used, which activities transformed them, which agents participated, and what outputs were generated. The W3C PROV family provides an existing general model for representing entities, activities, agents, and their derivation relationships.⁴⁴ It can support interoperable records of mathematical investigations without requiring every system to share the same internal execution architecture. For example, a proof candidate can be represented as an entity generated by a model execution. The execution is an activity associated with a specified model configuration and research task. A subsequent formal check produces an evidence record associated with the exact proof artifact and checking environment. The resulting provenance graph can help an independent reviewer reconstruct the sequence of operations. However, provenance is not proof of correctness. A perfectly documented execution may have used an invalid mathematical assumption, while a valid theorem may have been discovered through an irreproducible heuristic search.

Nor does provenance establish ownership or priority merely by recording a timestamp. Attribution disputes and research rights depend on additional evidence and institutional procedures. The proposed infrastructure should therefore use provenance to support reproducibility and accountability while preserving the distinction between what occurred, what was mathematically established, and what was institutionally authorized.

Two complementary forms of mathematical memory

The reference architecture distinguishes a research-state graph from a durable mathematical knowledge graph. The research-state graph represents work in progress. It contains open conjectures, candidate lemmas, unresolved obligations, failed strategies, computational experiments, and alternative approaches. It helps researchers and agents continue a particular investigation. The mathematical knowledge graph represents contributions selected for durable reuse. Its nodes identify mathematical objects and their versions; its edges represent typed relationships such as formal dependency, implication under specified assumptions, generalization, formalization, or refutation. These graphs serve different purposes. The first should tolerate uncertainty and exploratory material. The second should preserve sufficiently explicit claims and evidence to support independent interpretation.

A finding need not be proved to enter the durable registry. An open conjecture, a valid counterexample, or a reviewed negative result can constitute useful mathematical knowledge. But its status must be preserved accurately. The architecture should also support corrections without destroying history. If a previously accepted proof is discovered to rely on an inappropriate assumption, the affected artifact can acquire a new status and version-specific correction record. The dependency graph can then identify other results requiring reassessment. Those results are not automatically false merely because a dependency has changed. They may have alternative proofs or may remain valid under revised assumptions. The graph identifies the need for review; it does not replace mathematical reasoning about the consequences.

An incremental implementation strategy

The complete architecture need not be built before any of its benefits can be realized. A practical implementation could begin by extending an existing Open Math OS-like project environment with reproducibility manifests. Each substantial computational result would retain the relevant source files, inputs, dependency versions, and execution metadata. The next step would introduce versioned proof-evidence records associated with exact mathematical declarations. Formal checking could be performed through independently executable proof-assistant tooling, without requiring the model that generated the proof to participate in its acceptance. A small artifact registry could then assign stable identifiers to selected results and preserve their revisions. Initially, it might support only a limited vocabulary of mathematical relationships: formal dependency, refutation, version supersession, and reviewed correspondence between informal and formal statements.

Only after these mechanisms were demonstrated on real collaborative research projects would it be necessary to invest in more ambitious semantic inference, cross-foundation interoperability, or large-scale mathematical knowledge graphs. This order avoids attempting to solve the hardest semantic problem first. It establishes identifiable mathematical claims and reliable evidence before introducing inferred relationships among them. The resulting system could be deployed as an extension to Open Math OS, as an independent service, or as part of a federated mathematical knowledge ecosystem. The implementation choice is secondary to the assurance properties: researchers must be able to inspect and reuse the resulting mathematical artifacts without relying on the authority of the system that initially generated them. The proposed architecture thus identifies a transition from operational persistence, where a system retains research sessions and files, to epistemic persistence, where the mathematical meaning and evidence of contributions survive beyond the sessions in which they originated.

The distinction becomes clearer when followed through a specific mathematical investigation.

An end-to-end mathematical research workflow

The reference architecture can be examined through a mathematical investigation whose complete reasoning is accessible without relying on a frontier model. A simple example is appropriate because the objective is not to demonstrate extraordinary AI problem-solving capability. It is to identify what a mathematical research infrastructure must preserve as an investigation moves from conjecture to counterexample, corrected theorem, formal verification, conceptual generalization, and independent reuse. The example also makes the distinction between a successful mathematical argument and a successful mathematical research workflow concrete. The final theorem is only one output. The original conjecture, the counterexample that refutes it, the assumptions used in the corrected argument, and the mathematical structure explaining the result may all become useful to subsequent researchers.

The workflow is illustrative. It has not been executed in Open Math OS, and its proposed artifact records and verification procedures should not be interpreted as existing platform features.

Begin with a research objective, not merely a proof request

Suppose a mathematician wishes to characterize the positive integers that divide

f(n)=n^3-n

for every integer n. The researcher initially proposes the conjecture that 12 divides the polynomial for all integer inputs. There are two distinct mathematical objects here. The research objective is to determine the universal divisibility properties of the polynomial. The initial conjecture is a particular proposed answer to that objective. A system that treats the conjecture as the entire task may fail to preserve the broader research problem when the conjecture is refuted. A system that retains both objects can continue the investigation toward a corrected result. The researcher might authorize several investigative activities. An agent could search for counterexamples. Another could factor the polynomial symbolically. A third might investigate number-theoretic properties of the resulting expression.

The agents need not possess identical responsibilities. The counterexample search is concerned with refuting a proposed universal statement; the symbolic computation examines algebraic structure; and the number-theoretic investigation attempts to establish general divisibility properties. These activities can be coordinated through a common research-state representation while remaining separate sources of evidence. The initial artifact record should identify the research objective, the conjecture, the intended domain \mathbb Z, and the authorization under which the investigation is conducted.

A counterexample changes the status of the conjecture

The original conjecture fails for n=2, because

f(2)=2^3-2=6,

and 12 does not divide 6. This observation conclusively refutes the stated universal claim. It is not merely a failed attempt to construct a proof. The distinction is essential to a mathematical research-state system. A proof search can terminate unsuccessfully because an agent has exhausted its budget, selected an ineffective strategy, or failed to identify a relevant lemma. Such failure does not establish the falsity of the original theorem. A valid counterexample has a different logical status. It identifies an object satisfying the theorem’s quantified domain while violating its asserted property. The infrastructure should therefore retain the original conjecture as a refuted mathematical object linked to the exact counterexample.

The research objective remains active. In fact, the counterexample gives useful information about the strongest possible replacement theorem. Any positive integer dividing f(n) for every integer n must divide f(2)=6. Therefore, the greatest universal positive divisor cannot exceed 6. The counterexample has already contributed to the eventual maximality proof, even though it refuted the initial conjecture. A system that simply removes failed approaches and retains successful theorems would lose this relationship.

Symbolic computation exposes the mathematical mechanism

The next stage is to examine the polynomial’s structure. A symbolic algebra system can establish the factorization

n^3-n=(n-1)n(n+1). \tag{3}

The right-hand side is a product of three consecutive integers. Among any three consecutive integers, at least one is divisible by 3, and at least one is even. Consequently, the product is divisible by both 2 and 3, and therefore by 6. This establishes

\forall n\in\mathbb Z,\qquad 6\mid(n^3-n).

The argument applies to negative integers and zero as well as positive integers, since the divisibility properties of consecutive integers do not depend on the sign of the starting value. The result can now be combined with the earlier counterexample. Because 6 divides every value of the polynomial, it is a common divisor. Because f(2)=6, every positive common divisor must divide 6. Thus

\gcd\{n^3-n:n\in\mathbb Z\}=6. \tag{4}

Here the gcd of the set denotes its greatest nonnegative common divisor. The inclusion of the nonzero value f(2)=6 ensures that the gcd is well defined and positive. This resolves the research objective. Notice, however, that the resolution involves several mathematical relationships. The factorization supplies an algebraic identity; the consecutive-integer argument establishes universal divisibility; and the counterexample both refutes the proposed divisor 12 and, together with the corrected theorem, establishes maximality. The final conclusion depends on different pieces of evidence for its existence and optimality. These distinctions are mathematically meaningful and should remain available to researchers examining the result later.

Formal verification must address the exact proposition

A research team may now decide to formalize the corrected theorem in Lean. The intended statement can be represented by the following proposition:

∀ n : ℤ, (6 : ℤ) ∣ n ^ 3 - n

This is a formal proposition, not a complete Lean theorem declaration or an executed proof. A valid formalization workflow would require a proof term or tactic-generated derivation accepted under an explicitly identified Lean environment. The resulting assurance should be attached to the exact proposition checked, not merely to a manuscript or conversational statement claiming that the theorem was proved. The environment should also identify the relevant Lean toolchain and dependencies. For Mathlib-based work, the project configuration and resolved dependency manifest provide an established basis for reconstructing the required library versions. An independent checker should inspect the theorem’s axiom dependencies and identify any unsupported assumptions or incomplete placeholders.

Lean’s official validation guidance explains that proofs using sorry can elaborate through the sorryAx axiom and that #print axioms can expose dependencies on such axioms. It also describes additional checking procedures for compiled proof objects.⁴⁵ However, successful formal checking still does not establish that the encoded proposition is the intended mathematical statement. An agent might prove divisibility by 6 only for positive integers, or introduce an additional hypothesis that makes the formal statement weaker than the intended theorem. The resulting derivation could be valid within its own environment while failing to establish the original claim over all integers. This creates two assurance requirements.

The first requirement, deductive validity, concerns whether the formal proof establishes the encoded proposition under its declared assumptions; the second, semantic fidelity, concerns whether that proposition corresponds to the theorem the researcher intended to establish. The first can be addressed through formal checking. The second requires examination of the relationship between the mathematical representations, potentially assisted by automated tools but not established merely through their syntactic similarity. The illustrative workflow has established the theorem through ordinary mathematical reasoning. It has not produced or executed a Lean proof, so no kernel-checking result is claimed.

Preserve the research history as connected mathematical objects

Once the corrected theorem is established, the knowledge system should preserve more than its final statement. The original conjecture was false, but its counterexample contributed to the optimality argument. The factorization revealed the structural mechanism behind the corrected theorem. The resulting proof can be interpreted and extended independently of the particular computational session in which these observations occurred. A proposed registry could represent the investigation through related artifacts.

Artifact	Mathematical content	Evidentiary status	Relationship to the investigation
Original conjecture	12\mid n^3-n for all integers n	Refuted	Initial proposed answer
Counterexample	n=2, giving f(2)=6	Mathematically validated	Refutes the original conjecture and bounds possible common divisors
Algebraic identity	n^3-n=(n-1)n(n+1)	Established algebraic identity	Exposes the consecutive-integer structure
Corrected theorem	6\mid n^3-n for all integers n	Established by the informal proof presented here	Supplies the universal divisibility result
Maximality result	Greatest universal positive divisor equals 6	Established by combining divisibility and the value at n=2	Resolves the original objective
Formal proof artifact	Lean derivation of the corrected theorem	Not produced or checked in this example	Would provide additional independently checkable evidence

Table 8: Mathematical artifacts and evidence in the illustrative divisibility investigation. The final theorem does not replace the refuted conjecture or the evidence supporting its correction.

The table distinguishes the mathematical truth of a statement from the existence of a particular machine-generated verification record. It would be incorrect to mark the corrected theorem as Lean-verified merely because its mathematical proof is elementary or because Lean is available in the research environment. The registry should also maintain separate identities for the claims and their representations. A natural-language proof, an executable SymPy calculation, and a future Lean declaration may all relate to the same mathematical result without being interchangeable artifacts. This distinction allows the knowledge system to acquire stronger evidence over time without rewriting its history.

Understanding emerges through generalization

The corrected theorem is useful, but its mathematical value becomes clearer when the researcher asks why the number 6 appears. The proof relies on the fact that the polynomial factors into three consecutive integers. This suggests a more general result concerning products of consecutive positive integers. For positive integers m and k,

\prod_{j=0}^{k-1}(m+j) = k!\binom{m+k-1}{k}. \tag{5}

The identity follows from the factorial representation of the binomial coefficient. Since the binomial coefficient is an integer, every product of k consecutive positive integers is divisible by k!. This theorem provides a conceptual explanation of the earlier argument. The appearance of 6=3! is not an accidental numerical property of the cubic polynomial; it follows from a more general relationship between consecutive products and factorial divisibility. For n\geq2, selecting m=n-1 and k=3 recovers the factorization-based divisibility theorem. The remaining integer cases are handled directly or through the same consecutive-integer reasoning. This generalization connects the original result to combinatorics and to the algebraic structure of integer-valued polynomial expressions.

The knowledge graph should preserve the relationship as a mathematical generalization supported by a specific argument, not merely as a textual similarity between two formulas. There is also an important distinction between a formal dependency and a conceptual connection. The original divisibility theorem can be proved directly without invoking binomial coefficients. The more general identity provides another perspective on why it is true, but it is not necessarily a dependency of the original proof. A mathematical knowledge infrastructure should permit both relationships without confusing them.

Reuse requires more than retrieving the answer

Suppose a second research team later encounters the corrected theorem and wishes to investigate similar properties of higher-degree polynomials. One candidate is

\forall n\in\mathbb Z,\qquad 30\mid(n^5-n).

This statement is true, but the proof does not follow simply by repeating the earlier three-consecutive-integers argument. One approach uses modular arithmetic. For each prime p in \{2,3,5\}, the integer p-1 divides 4. Fermat’s little theorem gives n^{p-1}\equiv1\pmod p when p does not divide n, and hence n^5\equiv n\pmod p. When p divides n, the same congruence holds trivially. Thus n^5-n is divisible by 2, 3, and 5, so it is divisible by their product 30. Since 2^5-2=30, no greater positive integer can divide n^5-n for every integer n. Consequently,

\gcd\{n^5-n:n\in\mathbb Z\}=30. \tag{6}

This is another elementary, known result, not a novel discovery attributed to an AI system. Its relevance is the transfer of mathematical understanding. A researcher must recognize the general objective, determine which ideas from the cubic case remain applicable, and identify where a different mathematical mechanism is required. A conventional search system might retrieve the original theorem or a similar formula. A richer mathematical knowledge system could additionally expose the assumptions, proof method, maximality argument, related modular arithmetic results, and the status of candidate generalizations. The additional information would be useful only if it helped the researcher reason correctly. Generating numerous links between polynomial identities would not, by itself, establish successful conceptual transfer. This is precisely the distinction between retrieving mathematical content and enabling its effective reuse.

What the workflow implies for Open Math OS

The example clarifies both the immediate relevance of Open Math OS and the additional functionality proposed in this article. Open Math OS documents an integrated environment containing mathematical models, parallel agents, symbolic computing tools, Lean, Mathlib, persistent project files, and collaborative research facilities. These capabilities can support the principal computational activities illustrated here: searching for counterexamples, experimenting with symbolic representations, constructing proof candidates, discussing mathematical explanations, and preparing formalizations. The public materials do not establish that the system automatically creates stable mathematical contribution identifiers, preserves typed refutation relationships, enforces independently reproducible verification, or maintains a global semantic knowledge graph. Those are proposed extensions.

The workflow also indicates why a mathematical knowledge layer should not simply preserve every agent message indefinitely. The durable contributions are the meaningful mathematical objects and their evidence, not the full volume of computational activity. For the present example, preserving the complete execution history of every exploratory agent would be excessive. Preserving the false conjecture, its valid counterexample, the corrected theorem, the proof evidence, and the generalization may be sufficient for the intended educational and research use. For a larger collaborative project, more detailed execution manifests and provenance records could become necessary because reconstructing the work would otherwise be expensive or impossible.

The required level of assurance should therefore depend on the contribution’s status, significance, intended use, and downstream dependencies. The result is a more demanding concept of research success than completion of a single proof. A successful workflow should allow another researcher to determine what was established, how it was established, which assumptions were essential, which alternatives were explored, and what can legitimately be constructed from the result. That is the practical objective of the proposed mathematical commons. It is also the point at which the architectural proposal encounters its strongest objections.

Why architecture alone cannot guarantee mathematical progress

The proposed infrastructure addresses several identifiable weaknesses of contemporary AI-assisted mathematical research. It can preserve assumptions and proof evidence, make computational experiments more reproducible, expose dependencies among mathematical claims, and reduce the risk that intermediate results disappear within conversational histories. Although valuable, these properties are not sufficient conditions for mathematical progress. A technically reliable infrastructure could preserve thousands of valid but uninteresting theorems. It could make every calculation reproducible while providing little insight into the mathematical structures being investigated. It could formalize statements efficiently while discouraging exploration of concepts that are not yet sufficiently precise to encode. The distinction is fundamental because mathematical discovery is not only a process of generating and validating propositions. It also involves deciding which concepts are productive, which questions deserve attention, and which explanations reveal connections that change how a field is understood.

Those activities may increasingly benefit from AI assistance, but their scientific value cannot be inferred solely from the architecture of the assisting system.

Premature formalization can narrow the space of discovery

Formalization requires explicit definitions, assumptions, and logical relationships. These constraints are valuable when mathematical claims need to be checked or maintained. During early exploration, however, the relevant concepts may themselves be uncertain. Researchers frequently begin with informal intuitions, incomplete arguments, analogies, and examples that suggest a mathematical structure before they know how to define it precisely. Finding an appropriate definition may itself be a substantial part of the discovery. Imre Lakatos’s Proofs and Refutations provides a classical account of this process. Through the development of results concerning polyhedra, Lakatos shows how conjectures, attempted proofs, counterexamples, and criticism can lead mathematicians to revise the concepts used in their arguments.⁴⁶

A counterexample may therefore do more than refute a fixed proposition. It may expose the inadequacy of a definition or reveal an assumption that had previously remained implicit. This creates a tension with infrastructure organized around stable mathematical objects and formal dependencies. A system that demands exact formal statements at the beginning of every investigation may favor problems already expressible within familiar libraries and established conceptual frameworks. More exploratory research may appear less productive simply because its mathematical objects have not yet stabilized. The appropriate response is not to reject formalization. It is to distinguish the requirements of exploratory research from those of durable publication.

An AI-assisted workspace should tolerate provisional mathematical concepts and competing interpretations. A formal library can apply stronger acceptance criteria once a result is sufficiently developed for independent checking and reuse. The architecture should preserve the transition between these states without requiring every early-stage idea to satisfy the standards of a completed theorem.

Correctness does not determine mathematical significance

Formal checking answers a precise question: whether a specified derivation establishes a proposition under its declared assumptions. It does not establish whether the proposition is important, whether its proof is illuminating, or whether the result contributes new mathematical understanding. A theorem may be deductively valid but already known. An agent may produce numerous correct special cases of a more general result without identifying the general structure. A formally verified proof may be difficult to maintain because its generated definitions or intermediate lemmas are unnecessarily complicated. Such limitations are not failures of formal proof checking, which was never intended to decide mathematical significance. The problem arises when the existence of a formal certificate is treated as a complete assessment of scientific value.

The distinction is especially consequential in systems capable of generating mathematical material at scale. If proving a lemma becomes inexpensive, the production of additional checked declarations may cease to be a useful proxy for the creation of important mathematical knowledge. The same limitation applies to semantic knowledge graphs. A theorem that appears central in a dependency network may be a widely used low-level declaration rather than a conceptually important result. A semantic similarity measure may identify a plausible connection between two papers without establishing that the connection is mathematically useful. These representations can inform scholarly judgment. They cannot replace it.

Infrastructure creates an economic burden

The proposed mathematical knowledge layer also introduces costs. Proof artifacts must be recorded and maintained. Computational environments must be documented. Semantic relationships require validation. Mathematical identities and revisions must remain consistent. Corrections may trigger reviews of downstream dependencies. Access controls, data-use permissions, and governance procedures require operational administration. For a large collaborative formalization programme, these costs may be justified by the difficulty of reconstructing work and maintaining results across many contributors. For a small exploratory calculation, they may be disproportionate. The divisibility example illustrates the distinction. Establishing the maximal universal divisor of n^3-n requires elementary reasoning. A complete formal registry, extensive provenance capture, independent reviewers, and elaborate governance procedures would impose unnecessary costs if the example were simply a private exercise. The same result might legitimately require stronger documentation if it were incorporated into a shared formal library or used as a dependency in a larger mathematical development. The relevant principle is proportional assurance: stronger requirements are warranted when artifacts are intended for durable or consequential reliance.

The evidence and governance required for an artifact should reflect its declared status and intended reliance, not an assumption that all mathematical activity must satisfy the same maximum standard. Exploratory calculations can remain lightweight. Reusable internal results may require versioned files and documented assumptions. Publicly accepted formal theorems should retain independently checkable evidence. Contributions used in consequential external applications may require additional validation of their domain assumptions. Such differentiation avoids turning mathematical exploration into an administrative workflow while preserving stronger guarantees where they become necessary.

Quantitative evaluation can distort mathematical priorities

The same problem arises when mathematical research is evaluated through numerical indicators. A platform can measure solved problems, checked declarations, generated conjectures, proof-search duration, graph relationships, model tokens, and computing expenditure. These quantities are useful for understanding particular aspects of system behavior. They become dangerous when institutions begin treating them as complete measures of mathematical progress. Donald Campbell’s analysis of quantitative indicators describes how measurement systems can become distorted when their outputs influence consequential institutional decisions.⁴⁷ The mechanism is directly relevant to AI-assisted mathematics. A system rewarded for generating formally checked theorems might produce large numbers of trivial consequences. A knowledge graph evaluated by its number of relationships may accumulate weak semantic associations. An agent rewarded for producing novel conjectures may generate statements that are syntactically different from existing results but conceptually redundant.

In each case, the system may optimize the measurement while contributing little to the underlying scientific objective. A more sophisticated metric does not automatically eliminate the problem. Scientific significance, conceptual novelty, and mathematical understanding are difficult to reduce to stable numerical functions. The evaluation framework developed earlier therefore separates correctness, efficiency, reproducibility, understanding, reuse, and autonomy rather than collapsing them into one score. Even that framework requires continuing scrutiny. Once benchmark tasks are repeatedly used to guide model development, improvements may reflect adaptation to the evaluation procedure rather than a corresponding improvement in mathematical research capability.

Independent tasks, controlled comparisons, transparent limitations, and expert judgment remain necessary. The purpose of evaluation should be to identify the conditions under which particular research mechanisms are useful, not to construct a permanent numerical ranking of mathematical intelligence or scientific value.

Knowledge graphs cannot eliminate conceptual disagreement

The proposed semantic layer creates another difficulty: mathematical concepts do not always admit one canonical interpretation. Different researchers may understand the same theorem through algebraic, geometric, combinatorial, or computational perspectives. These interpretations can be mutually compatible without being identical. A semantic graph that forces every result into one authoritative classification risks losing precisely the alternative viewpoints through which mathematical understanding develops. Even claims of equivalence require care. Two mathematical statements may be equivalent under one set of assumptions but not another. Their equivalence may depend on a choice of foundations or on translations between different formal systems. Similarly, two proofs can establish the same proposition while contributing different mathematical ideas.

A durable knowledge infrastructure should therefore distinguish exact formal identities from broader semantic interpretations. It should permit alternative attributed explanations and represent uncertain connections as hypotheses rather than established relationships. The objective is to make conceptual disagreement visible and productive, not eliminate it through automated standardization. This also limits the use of language models for semantic graph construction. A model can propose useful relationships, but the graph must retain the evidentiary status of those proposals. A machine-generated assertion of equivalence should not become a mathematical fact merely because it is stored in a structured database.

Scientific sovereignty can create new centers of authority

A mathematical commons also faces an institutional paradox. Paradoxically, an infrastructure designed to reduce dependence on proprietary AI providers may itself become a central authority over mathematical knowledge. A widely used artifact registry can influence which results are visible. A semantic ontology can privilege particular mathematical interpretations. A governance committee controlling scarce computing resources can influence which research directions receive support. These powers may be exercised responsibly, but their existence should not be concealed by the language of openness or community ownership. A nonprofit institution is not automatically governed by its users. A public repository is not necessarily institutionally independent. An advisory committee does not necessarily possess binding authority. The relevant safeguards include portability, transparent allocation rules, independent verification, accountable decision-making, and procedures for contesting disputed judgments.

A mathematical knowledge system should also permit legitimate alternatives. Independent repositories may preserve the same result under different scholarly arrangements. Researchers may maintain competing semantic interpretations. A formal theorem should remain verifiable even when its original hosting platform is no longer available. Federation creates its own difficulties, including inconsistent identifiers, differing policies, and incompatible representations. The answer is not maximal decentralization without shared standards. It is to make the necessary shared technical interfaces explicit while preserving independent authority over scientific judgments that need not belong to one operator. A mathematical commons is therefore better understood as an interoperable institutional ecosystem than as a single universally trusted database.

Greater automation does not guarantee greater human understanding

There is a final, more fundamental limitation. Even if every mathematical result were correctly verified, efficiently indexed, and perfectly preserved, mathematicians would not necessarily understand more mathematics. A researcher may become substantially more productive through an AI system while performing less independent reasoning. An agent may produce excellent explanations that the reader cannot reconstruct later. A large collection of related proofs may remain conceptually opaque despite being fully formalized. These outcomes do not make AI assistance worthless. Collaborative mathematical capability is a legitimate objective, even when not every participant independently masters every component of the resulting work. However, that objective must be distinguished from increasing human mathematical understanding.

An infrastructure can expose the dependencies of a proof, offer alternative explanations, and make its assumptions easier to examine. These mechanisms create opportunities for understanding; they do not ensure that understanding occurs. The same limitation applies to future AI systems themselves. A model might discover mathematical structures that are difficult for humans to interpret while nevertheless producing correct and valuable results. Requiring immediate human comprehension as a condition for every mathematical contribution could unnecessarily restrict research. The appropriate response is to preserve the distinction between established mathematical validity and unresolved interpretation. A formally verified result can remain valid even when its conceptual significance is not yet understood. The infrastructure should preserve that result and support later investigations into its meaning, rather than assign it an unjustified significance ranking or discard it for lack of an accessible explanation.

This reinforces the importance of the scholarly community. Mathematical understanding develops through criticism, comparison, exposition, teaching, and the discovery of connections that may emerge long after a theorem has been proved. No artifact schema or governance structure can guarantee those developments.

The limit of an operating-system approach

The objections do not invalidate the proposed Math 2.0 architecture. They establish the boundaries within which its value must be assessed. Formal proof checking is indispensable when deductive assurance is required, but it does not determine mathematical significance. Structured provenance improves reconstructability, but recording research activity can impose disproportionate costs. Semantic knowledge graphs support navigation and reuse, but they cannot eliminate ambiguity or conceptual disagreement. Community governance can protect scientific independence, but it can also introduce new forms of concentration and institutional authority. A successful infrastructure must therefore remain modular, proportionate, contestable, and open to evidence that some of its mechanisms provide insufficient value for particular research activities.

The decisive question is not whether every mathematical investigation can be represented within a comprehensive computational system. It is whether mathematical researchers can use increasingly powerful AI capabilities without losing the ability to inspect, criticize, understand, and independently extend the resulting mathematics. Open Math OS provides a plausible operational foundation for that ambition by integrating models, scientific tools, persistent computation, and collaborative research. The broader mathematical commons proposed in this article would add durable mathematical artifacts, explicit assurance, semantic relationships, independent repositories, and accountable scholarly governance. Neither architecture guarantees mathematical progress. Their contribution must be established through the mathematical activities they enable and the independent research they make possible. That is the appropriate standard for assessing whether Math 2.0 moves beyond the production of increasingly large numbers of correct proofs toward the construction of more durable and meaningful mathematical knowledge.

Conclusion: from an operating system to a mathematical commons

Open Math OS represents a meaningful development in the emerging relationship between artificial intelligence and mathematical research. Its importance lies less in the capabilities of any individual model than in the attempt to organize AI-assisted mathematics around persistent research projects, scientific computing, formal verification tools, parallel agents, and human collaboration. Rather than treating mathematics as a sequence of isolated problems submitted to a chatbot, the platform proposes an environment in which people and computational systems can participate in sustained investigations.

The initiative is also institutionally distinctive. SAIR’s founders recognize that the future of mathematical AI will be shaped not only by model performance, but also by access to computing resources, rights over unpublished research, the openness of scientific tools, and the authority to determine how those tools are developed and used. Its stated commitments to open-weight models, researcher consent, attribution, and community governance respond to concerns that mathematical discovery could become increasingly dependent on infrastructure controlled by a small number of commercial AI laboratories.⁴⁸

These objectives make Open Math OS worth examining as a serious experiment in mathematical research infrastructure rather than dismissing it as another AI assistant. At the same time, its current maturity must be assessed accurately. In announcing the soft launch on 16 October 2026, Terence Tao explicitly described the hosted models as existing third-party open-weight systems whose mathematical capabilities remain behind those of leading proprietary frontier models. The development of a more specialized SAIR mathematical model, along with further improvements to the platform, remains part of the initiative’s future programme.⁴⁹ The immediate contribution is therefore the integration of existing capabilities into an accessible collaborative environment. The more ambitious proposition—that such an environment can support mathematical understanding, durable knowledge, and effective scientific independence—remains to be demonstrated.

Three different meanings of mathematical infrastructure

The analysis developed in this article suggests distinguishing three overlapping but conceptually different systems. A mathematical AI workbench enables researchers to perform mathematical activities more effectively. It provides access to language models, computational tools, proof assistants, shared files, and persistent research environments. Its contribution can be assessed through the quality of its assistance, the reliability of its computational workflows, and the resources required to complete mathematical tasks. Open Math OS already presents a recognizable implementation of this model, although some of its operational properties remain unverified through independent testing.

Mathematical research infrastructure adds the mechanisms through which research results retain their mathematical meaning and evidentiary status beyond the original investigation. Its central objects are identifiable contributions: conjectures, theorems, counterexamples, constructions, formal proofs, computational experiments, and explanatory relationships. Such an infrastructure must preserve exact statements, assumptions, version histories, supporting evidence, and appropriately qualified dependencies. A proof generated by an agent should remain independently checkable. A corrected theorem should not silently replace the proposition originally investigated. A failed conjecture and its counterexample should remain recoverable where they provide useful mathematical information. A mathematical commons extends these technical guarantees into an interoperable and institutionally accountable ecosystem. Mathematical contributions can be examined and reused across research platforms; independent institutions can maintain repositories and verification services; researchers retain effective authority over their unpublished work; and decisions concerning access, attribution, publication, and shared resources remain contestable.

These are not three mandatory stages of one product roadmap. A research workbench can use independent mathematical repositories from the outset. A commons can emerge through cooperation among existing formal libraries, research platforms, universities, foundations, and scholarly institutions rather than through one comprehensive operating system. The distinction matters because technical integration and institutional centralization are different objectives. The benefits of using mathematical models, scientific computing, and formal verification within one interface do not require the same organization to control every accepted theorem, research artifact, and scholarly decision. Indeed, the scientific value of a mathematical commons may depend on ensuring that no individual provider becomes indispensable to the continued validity, accessibility, or interpretation of the mathematical record.

The real bottleneck is not always proof production

The developments of 2026 make this distinction increasingly consequential. Frontier AI laboratories are demonstrating greater mathematical reasoning capabilities, and OpenAI’s October release of AI-generated mathematical results illustrates the growing scale at which computational systems can produce candidate contributions to the literature.⁵⁰ Yet mathematical validity is not equivalent to mathematical significance. An independently checked proof may establish a correct theorem without revealing why it matters, which methods are reusable, or how the result connects to existing research. As the cost of generating candidate mathematical arguments falls, the cost of examining, interpreting, and assimilating them becomes comparatively more visible. The problem is not necessarily an absolute shortage of proofs. It is the potential divergence between the rate at which mathematical material can be generated and the capacity of researchers to convert that material into reliable and meaningful knowledge. This helps explain why the institutional response matters as much as the technical one.

The Simons Foundation’s 15 October 2026 initiative, supported through $15 million in combined funding and resources from the foundation, Anthropic, and OpenAI, explicitly addresses the work needed to evaluate AI-assisted mathematical results, develop mathematical understanding, and support community-directed engagement with new tools.⁵¹ Such efforts do not replace more capable mathematical models. They address activities that improvements in model inference do not automatically eliminate: independent verification, conceptual explanation, scholarly review, education, and the formation of productive research communities. The same observation qualifies the ambitions of Open Math OS.

A persistent workspace can make mathematical investigations easier to continue. Parallel agents can increase the number of approaches explored. Formal proof assistants can provide strong deductive assurance for appropriately encoded propositions. But none of these capabilities, individually or in combination, guarantees that researchers will identify more fruitful concepts, acquire deeper understanding, or produce results that subsequent mathematicians can use. The relevant objective is therefore not to maximize mathematical output as an end in itself, but to improve the conditions under which computational discoveries can become part of cumulative mathematical research.

What would constitute convincing evidence?

The transition from an AI workbench to mathematical research infrastructure should be evaluated through observable properties rather than architectural promises. Independent reconstruction is the first requirement. Researchers should be able to export an investigation, recover its relevant computational dependencies, reproduce appropriate experiments, and establish the status of its mathematical claims outside the original hosting environment.

Independent mathematical assurance is the second. A result presented as formally verified should identify the exact proposition, logical assumptions, proof artifact, and checking environment. Where the result exists only as an informal proof, computational observation, or model-reviewed argument, its evidence should be described accordingly.

Durable mathematical knowledge is the third. A mathematical contribution should remain identifiable across revisions, with relationships that distinguish formal dependency from conceptual similarity, established implication from speculative association, and valid counterexample from inconclusive search.

Demonstrated understanding and reuse is the fourth. A research team should be able to reconstruct and extend previous work using its preserved mathematical artifacts. Controlled evaluations should establish whether structured knowledge and agent coordination improve conceptual transfer, independent continuation, or research efficiency relative to simpler workflows.

Effective scientific sovereignty is the fifth. Researchers should be able to enforce appropriate data-use restrictions, inspect relevant decisions, transfer their work between providers, and participate meaningfully in the governance of shared infrastructure. Public commitments to openness and community participation are important, but they are not substitutes for independently demonstrable controls. These requirements also provide falsification criteria. If a knowledge-aware environment does not improve independent reuse, its additional complexity may be unjustified for the activities tested. If parallel agents consume more resources without producing additional valid or useful findings, their orchestration advantage remains unestablished. If a purportedly open research platform cannot support meaningful portability or enforce the stated rights over research materials, its contribution to scientific sovereignty is correspondingly limited. Such outcomes would not invalidate the broader Math 2.0 programme. They would identify which mechanisms require revision, which benefits are context-dependent, and which objectives cannot be achieved merely through further technical integration.

Beyond the operating-system metaphor

The operating-system metaphor is useful because it emphasizes shared services. Just as conventional computing environments abstract away many details of hardware and software execution, an integrated mathematical workspace can reduce the operational burden of combining language models, symbolic computation, proof assistants, and persistent research files. The metaphor nevertheless has limits. A conventional operating system primarily coordinates computational resources and processes. Mathematical research also requires interpretation, criticism, evolving concepts, and institutional judgments concerning the significance of results. These cannot be reduced to the correct execution of software operations. The proposed mathematical artifact layer addresses part of the gap by preserving claims together with their evidence and relationships. It would allow a result generated through one computational environment to remain independently inspectable and reusable in another. Yet even this infrastructure cannot determine which mathematical questions deserve investigation or guarantee that a verified theorem contributes to understanding. Formal correctness, mathematical significance, and scientific value remain distinct.

This is why a mathematical commons must be understood as both a technical and an institutional construction. It needs reliable computational interfaces and durable knowledge representations, but also scholarly practices capable of accommodating uncertainty, disagreement, correction, and conceptual discovery. It should permit different mathematical interpretations to coexist, different institutions to maintain compatible resources, and different models to contribute to research without making any one of them the final authority over its conclusions. The purpose is not to place every mathematical activity inside one system. It is to ensure that the products of those activities retain their meaning and usefulness as they move among systems, researchers, and institutions.

What remains after the computation?

The central argument of this article can now be stated more precisely. Open Math OS is an operationally significant step toward Math 2.0 because it treats mathematical AI as part of a sustained, collaborative research environment rather than only as a machine for answering mathematical questions. Its integration of models, agents, scientific tools, and persistent projects addresses practical obstacles to the wider adoption of AI in mathematical research. SAIR’s institutional programme adds an important ambition: mathematical researchers should have meaningful influence over the models, resources, data policies, and infrastructure through which that research increasingly occurs.

Neither achievement, on the public evidence available through 16 October 2026, establishes the existence of a complete mathematical knowledge commons. The stronger claim requires durable mathematical artifacts, independent assurance, interoperable representations, effective governance, and empirical evidence that the resulting systems improve the ability of researchers to reconstruct, understand, criticize, and extend mathematical work. Those requirements should not be viewed as additional product features to be accumulated indiscriminately. They define responsibilities that may be fulfilled by different systems and institutions, with different forms of evidence and authority. The future of mathematical AI may therefore depend less on the emergence of one comprehensive mathematical operating system than on the development of an ecosystem in which increasingly capable computational agents can contribute to a mathematical record that remains independently verifiable, intellectually meaningful, and institutionally accountable.

The decisive question concerns what survives when the computation ends. Can another mathematician check the theorem without trusting the model that produced it? Can a failed investigation be reconstructed without reading thousands of conversational messages? Can an alternative proof reveal a reusable mathematical idea? Can a research team extend an earlier result without depending on the original platform? And can mathematicians retain the authority to determine which questions are worth pursuing next? A theorem factory produces mathematical outputs. A mathematical commons makes those outputs—and the ideas, evidence, and investigations surrounding them—durable inputs to further mathematical progress.

See also machine learning longforms

What Kind of Thing Is an Alien Mind?

Reading Jakub Pachocki on intelligence, agency, alignment, opacity, and recursive self-improvement

AI Adoption, Productivity, and the Missing Middle

A review of Banca d'Italia QEF 1009 on Italy's AI adoption, firm productivity, and policy architecture

Harnessing Focus: Merging AI and Market Dynamics

The attention paradigm: bridging natural language processing and economic theory

See also mathematics longforms

Homomorphic Encryption for Developers

From algebraic foundations and textbook RSA to practical BFV and dependable private computation

The Mathematics Behind a Racing Shell

Why rowing-boat simulation is a difficult multiphysics engineering problem

Sudoku and Satisfiability Modulo Theories

You can solve it the standard way or... with Python and math

See also posts

Math 2.0: Beyond the Theorem Factory

Terence Tao on proof abundance, mathematical understanding, and the redesign of research

The Infinite SaaS Factory

Satya Nadella's vision and the computational conditions for software on demand

When Mathematical Discovery Became a Production System

OpenAI’s 372 result families and the epistemology of proof abundance

How Sovereign Is Kolibri?

Aleph Alpha's German foundation model is strongly sovereign in production and deployment, but not across the full technological stack

From 67 Submissions to 19,525: The Research Explosion

ICLR submissions have grown nearly 300-fold since 2013 and 68% in a single conference cycle

AI Agents Are Solving Open Problems and Changing What Mathematics Is For

Navier–Stokes, machine-scale mathematical search, and the changing meaning of mathematical progress

Footnotes

1. Montano, A. (2026). Math 2.0: Beyond the Theorem Factory. Earlier article.

2. Tao, T. (2026). Math 2.0. Lecture slides.

3. SAIR Foundation. (2026). Open Math OS: Infrastructure for Math 2.0. Official launch announcement.

4. Lean Project. Validating a Lean Proof. Official documentation.

5. Tao, T. (2026). SAIR Open Math OS released. What’s new, 16 October 2026. Tao describes the soft launch, hosted third-party models, their current capability limitations, team-based interaction, donated compute, and plans for mathematics-specific post-training. Primary announcement.

6. Tao, T. (2026). SAIR’s Open Math Model initiative. What’s new, 18 September 2026. Tao explains the foundation’s origins, nonprofit purpose, and initial research activities. Founder’s account. See also SAIR Foundation (2025), Welcome to the SAIR Blog, for its institutional description. Institutional background. SAIR’s October 2026 UCLA event programme also identifies Chuck Ng as a co-founder. Official event programme.

7. Tao, T. (2026). SAIR’s Open Math Model initiative. What’s new, 18 September 2026. The original announcement distinguishes the objective of creating open scientific models and tooling from the wider foundation’s existing events and competitions. Primary announcement.

8. SAIR Foundation. (2026). An Open Commitment to Mathematics and Science. Published 21 September 2026. Identifies XTX Markets and Susquehanna International Group as supporters of the open research programme and specifies the competitions they are supporting. Official announcement.

9. SAIR Foundation. (2026). Open Math OS: Infrastructure for Math 2.0. Official launch announcement.

10. Tao, T., et al. (2026). A Severe Misalignment of AI in Mathematics. Declaration initially signed by twenty-five Fields Medalists, published 11 September 2026. The statement criticizes the use of mathematical problem solving primarily as an AI performance benchmark and emphasizes the broader purpose of mathematical research. Primary declaration and initial signatories.

11. Tao, T. (2026). SAIR Open Math OS released. What’s new, 16 October 2026. Tao describes the soft launch, hosted third-party models, their current capability limitations, team-based interaction, donated compute, and plans for mathematics-specific post-training. Primary announcement.

12. SAIR Foundation. (2026). Open Math OS: Infrastructure for Math 2.0. Official launch announcement.

13. Open Math Model. (2026). Open Math OS. Platform overview.

14. SAIR Foundation. (2026). Open Math OS: Infrastructure for Math 2.0. Official launch announcement.

15. Open Math Model. (2026). Open Math OS. Platform overview.

16. Bolan, M., Breitner, J., Brox, J., et al. (2025). The Equational Theories Project: Advancing Collaborative Mathematical Research at Scale. arXiv, arXiv:2512.07087. The project investigated 22,028,942 implication relationships among 4,694 magma identities through collaborative human and computational reasoning, with formal validation in Lean. Preprint.

17. Lean Project. Validating a Lean Proof. Official Lean documentation covering proof checking, axiom inspection, incomplete proofs, and rechecking stored declarations. Official documentation.

18. Tao, T. (2026). SAIR Open Math OS released. What’s new, 16 October 2026. Tao describes the soft launch, hosted third-party models, their current capability limitations, team-based interaction, donated compute, and plans for mathematics-specific post-training. Primary announcement.

19. Avigad, J., Buzzard, K., Commelin, J., Degenne, R., Morrison, K., Nash, O., & Topaz, A. (2026). How to Formalize All of Mathematics. Guest article published on the Xena Project blog, 16 October 2026. The authors examine the distinction between high-volume AI-generated formalization and mathematical libraries that are structured, maintainable, and useful for further research. Primary article.

20. SAIR Foundation. (2026). Open Math OS: Infrastructure for Math 2.0. Official launch announcement.

21. W3C. (2013). PROV-Overview. W3C specification.

22. Lean Prover Community. Mathlib4. Repository.

23. Rabe, F., & Kohlhase, M. (2013). A scalable module system. DOI.

24. Li, X., et al. (2026). The Network Structure of Mathlib. arXiv, arXiv:2604.24797. Study of formal-library dependency structure and the distinction between software and mathematical centrality. Preprint.

25. Kurgan, S., et al. (2026). TheoremGraph: Bridging Formal and Informal Mathematics. arXiv, arXiv:2606.25363. Research on formal and informal mathematical dependency extraction, semantic matching, and retrieval. Preprint.

26. Liu, J., et al. (2026). Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory. Preprint.

27. Chen, Q., et al. (2026). Euler: Towards Human-Centered Multi-Agent Mathematical Discovery. Preprint.

28. SAIR Foundation. (2026). Open Math Model initiative. Institutional statement.

29. Liu, J., et al. (2026). Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory. Preprint.

30. Chen, Q., et al. (2026). Euler: Towards Human-Centered Multi-Agent Mathematical Discovery. Preprint.

31. Thurston, W. P. (1994). On proof and progress in mathematics. Preprint.

32. Zheng, K., Han, J. M., & Polu, S. (2021). MiniF2F. Preprint.

33. Tsoukalas, G., et al. (2024). PutnamBench. Preprint.

34. Glazer, E., et al. (2024). FrontierMath. Preprint.

35. Balunović, M., Dekoninck, J., Petrov, I., Jovanović, N., & Vechev, M. (2025). MathArena: Evaluating LLMs on Uncontaminated Math Competitions. arXiv, arXiv:2505.23281. The work introduces evaluation on newly released competitions and includes proof-writing assessment, while documenting concerns about contamination in established mathematical benchmarks. Preprint.

36. Google DeepMind. (2026). Accelerating mathematical and scientific discovery with Gemini Deep Think. Official research announcement.

37. OpenAI. (2026). Sharing AI progress in mathematics. Published 6 October; updated 15 October. Official announcement.

38. Avigad, J., Buzzard, K., Commelin, J., Degenne, R., Morrison, K., Nash, O., & Topaz, A. (2026). How to Formalize All of Mathematics. Guest article published on the Xena Project blog, 16 October 2026. The authors examine the distinction between high-volume AI-generated formalization and mathematical libraries that are structured, maintainable, and useful for further research. Primary article.

39. Liu, J., et al. (2026). Danus: Orchestrating Mathematical Reasoning Agents with Fact-Graph Memory. Preprint.

40. Chen, Q., et al. (2026). Euler: Towards Human-Centered Multi-Agent Mathematical Discovery. Preprint.

41. Advisory Group on Mathematics and Artificial Intelligence. (2026). Responsible Release of AI-Generated Mathematics. Published 29 September 2026. The recommendations distinguish mathematics already understood by responsible researchers from AI-generated results requiring additional scholarly assimilation; they address independent repositories, formalization, attribution, disclosure of computational information, community-directed understanding, and access to advanced models. Official recommendations.

42. Simons Foundation. (2026). Simons Foundation launches $15M effort to help mathematicians navigate AI era. Published 15 October. Official announcement.

43. Lean Project. Lake: Build Tools and Distribution. Official Lean documentation describing project configuration, package dependencies, and reproducible builds. Lake’s dependency resolution uses lake-manifest.json to retain the resolved dependency revisions, including Mathlib where it is imported as a package. Official documentation. See also the Lean repository’s Lake documentation.

44. W3C. (2013). PROV-Overview. W3C specification.

45. Lean Project. Validating a Lean Proof. Official Lean documentation covering proof checking, axiom inspection, incomplete proofs, and rechecking stored declarations. Official documentation.

46. Lakatos, I. (1976). Proofs and Refutations. Cambridge University Press. Publisher page.

47. Campbell, D. T. (1979). Assessing the impact of planned social change. DOI.

48. SAIR Foundation. (2026). Open Math Model initiative. Institutional statement.

49. Tao, T. (2026). SAIR Open Math OS released. What’s new, 16 October 2026. Tao describes the soft launch, hosted third-party models, their current capability limitations, team-based interaction, donated compute, and plans for mathematics-specific post-training. Primary announcement.

50. OpenAI. (2026). Sharing AI progress in mathematics. Published 6 October; updated 15 October. Official announcement.

51. Simons Foundation. (2026). Simons Foundation launches $15M effort to help mathematicians navigate AI era. Published 15 October. Official announcement.