Towards a Semantic Language of Mathematics

The current state of the field — research perspective as of 23 October 2026

The central question is no longer simply whether mathematics can be represented in a form computers understand. We already have proof assistants, formal libraries, computer algebra systems, mathematical knowledge bases, semantic document formats, and AI systems that can translate some informal mathematical statements into formal definitions and proofs.

The deeper question is whether these separate achievements can become a coherent, interoperable, searchable, machine-checkable mathematical knowledge system—one in which mathematical meaning survives translation between authors, notation systems, foundations, proof assistants, and applications.

Your 2016 starting point is particularly valuable because it gives us a historical baseline. We should assess progress against the original vision, not just list new software. For each of your 46 topics, the investigation should distinguish:

• What exists: software, formal libraries, standards, datasets, protocols, and research systems that have actually been built.
• What works: capabilities demonstrated in practice, with evidence and limitations.
• What remains fragmented: problems that are solved within one ecosystem but not across mathematics as a whole.
• What remains open: the research and engineering required for a global semantic mathematics library.

One important distinction will guide the entire review: a proof assistant’s ability to check a theorem is not the same as a universal language for mathematical knowledge. Lean, Coq/Rocq, Isabelle, HOL Light, Mizar, computer algebra systems, and mathematical publishing formats each solve different parts of the problem. The current challenge is how to connect their achievements without losing meaning or compromising correctness.

1. Executive assessment: how far have we come since 2016?

The strongest conclusion from the evidence is that the field has made major progress in machine-checkable formal mathematics, AI-assisted formalization, and mathematical markup, but has not yet produced a universal semantic language or a unified global mathematical library.

The distinction matters because several advances can look like the original vision while solving only one part of it.

The state of the field in October 2026

Established and usable

Proof assistants, large reusable formal libraries, machine-checked proofs, mathematical markup, computer algebra, public repositories, and collaborative formalization workflows.

Advancing rapidly

LLM-assisted theorem proving, translation from natural language to formal statements, formalization of textbooks and research papers, and automated proof search.

Partially solved, but fragmented

Semantic representation, cross-system interoperability, theorem search, notation disambiguation, links between informal papers and formal proofs, and semantic preservation across translations.

Still open at global scale

A shared, foundation-independent representation of mathematical meaning; broad coverage of research mathematics; reliable preservation of meaning through automatic translation; and sustainable community-wide maintenance.

This assessment is supported by several developments that are especially important to your original vision:

• The Mathlib library for Lean 4 has become a major shared infrastructure for formalized mathematics, with collaborative development, documented conventions, generated documentation, and reusable results.

  image

  GitHub

• The W3C’s MathML 4 Working Draft dated 22 October 2026 addresses mathematical notation, content markup, and accessibility. However, it remains a Working Draft, not a finalized universal semantic language for mathematical reasoning.

  image

  W3C

  +1

• AI systems have begun formalizing substantial bodies of mathematics. In April 2026, researchers reported an Isabelle/HOL formalization of 806 results across all 39 sections of Munkres’ Topology, with over 85,000 lines of generated formal code and zero remaining sorry placeholders.

  image

  arXiv

• In September 2026, Anthropic reported an end-to-end Lean formalization of Fermat’s Last Theorem, produced largely autonomously in 11 days. The published project contains roughly 13 million lines of Lean code and 29,500 intermediate theorems. Its significance is substantial, but it does not by itself solve semantic interoperability or establish that all mathematics can be automated.

  image

  Anthropic

  +1

The next question is what these achievements mean for each of your 46 topics.

2. Research scope and an important methodological rule

The cutoff for this review is 23 October 2026. I distinguish three different types of evidence:

• Implemented capability: a released tool, standard, library, or inspectable formal artifact.
• Published research result: a reported experiment or theorem formalization, whose precise claims depend on the authors’ methods and verification.
• Long-term vision: a proposed capability that has not yet been established at the required scale.

This distinction is particularly important for AI. A system can report a high success rate at generating formal statements, another high success rate at proving supplied statements, and a much lower success rate when required to read an original mathematical problem, interpret it correctly, formalize it, and prove the corresponding claim.

A 2025 NeurIPS study of miniF2F demonstrated exactly this issue. Its authors found that the best complete pipeline achieved about 36% on the original evaluation setup; after correcting discrepancies between informal and formal problem statements, the revised miniF2F-v2 benchmark produced a best reported end-to-end accuracy of 70%. These are results for that particular benchmark and experimental setting—not estimates of AI’s ability to formalize arbitrary research mathematics.

image

NeurIPS Proceedings

That finding connects directly to your central concern: the meaning of a theorem must survive the entire pipeline, not merely the final proof checker.

Part I — The original vision and its technical foundations

1. The vision for a library

The original idea was to move beyond a library that merely stores mathematical documents toward one that stores mathematics in a form computers can interpret and use.

A conventional digital library might index a paper by its title, author, abstract, keywords, and publication date. A semantic mathematical library would additionally identify:

• The definitions introduced in the paper.
• The hypotheses of each theorem.
• The mathematical objects to which the theorem applies.
• The theorem’s conclusion and proof dependencies.
• Equivalent formulations and related results.
• The formal proof, if available.
• The notation used by the author and the intended meaning of that notation.

Consider a theorem stating that every continuous function on a compact topological space is bounded. A document-search system can find the sentence. A semantic library should also be able to recognize the relevant concepts—continuity, compactness, topological spaces, and boundedness—and locate compatible results in other documents or formal libraries.

This vision is being realized in pieces through formal libraries, structured mathematical documents, theorem search, and AI-assisted formalization. But there is still no single system that captures all published mathematics in this integrated form.

Current assessment: Strong progress in reusable formal knowledge; no universal mathematical library yet.

2. Challenges in standardization

The difficulty is that mathematics has several different kinds of standards, each serving a different purpose.

OpenMath was designed to represent mathematical objects and their semantics for communication between software systems. MathML addresses mathematical notation and content for web use. They are valuable components, but neither is a replacement for the full logic, type system, libraries, and proof-checking environment of a theorem prover.

image

OpenMath

+1

The current MathML 4 work is particularly relevant because it continues to develop a structured representation of mathematical notation and content, including accessibility annotations. Its status on 23 October 2026 is still a Working Draft.

image

W3C

The unresolved standardization question is therefore not simply, “Which syntax should everyone use?” It is:

Which information must every representation preserve, and which differences between mathematical foundations are acceptable?

3. Bridging mathematical communities

Different communities optimize for different goals.

Press photos

Working mathematicians

Value conceptual clarity, concise proofs, familiar notation, and freedom to choose definitions and methods.

Lean: How AI and Proof Automation Are Changing Mathematics

Formal-methods researchers

Need explicit types, precise definitions, proof terms, reproducibility, and machine-checkable correctness.

Computer algebra and scientific computing

Focus on symbolic manipulation, computation, numerical methods, and effective algorithms.

Revolução no laboratório de matemática: é o software, agora, que avalia os teoremas. - JupiterHomes

AI and machine-learning researchers

Need training data, formal benchmarks, executable feedback, scalable search, and measurable success criteria.

The major development since 2016 is that these groups have more opportunities to collaborate around shared artifacts: open formal libraries, public repositories, benchmarks, and AI-assisted workflows.

The remaining gap is institutional and technical. A theorem proved in one system may depend on a particular foundation, library hierarchy, or notation convention. Translating it into another system can require more than translating syntax.

Research on interoperability between Rocq and Isabelle, for example, investigates translation through the Dedukti proof framework. This is an active route toward sharing formal libraries, not evidence that all proof assistants are already interoperable.

image

blanqui.gitlabpages.inria.fr

4. Designing interaction between humans and computers

Formalization has historically demanded that mathematicians learn the syntax and proof engineering conventions of a particular system.

Modern tools are moving toward workflows in which a mathematician can write a paper, specify a theorem, produce a formal blueprint, ask an AI assistant to generate code, and have a proof assistant check the result.

The EPFL AI for Math project develops document-level autoformalization tools, including LeanFlow. Its focus is not merely completing an isolated proof hole: it is building formal projects from mathematical documents through a structured workflow.

image

aiformath.epfl.ch

+1

A useful interaction model is:

1. The human states the mathematical problem in ordinary language or conventional notation.
2. The system identifies the intended definitions, assumptions, domains, and conclusion.
3. The user reviews the proposed formal statement.
4. An agent constructs a proof and consults existing library results.
5. The kernel checks the proof.
6. The system preserves the correspondence between the original statement and the formal theorem.

Step 3 is essential. A perfectly checked proof of the wrong formal statement does not establish the intended mathematical result.

Current assessment: AI-assisted interaction is real and improving, but semantic review and traceability remain necessary.

5. Formalization of theorems

Formalization means expressing mathematical definitions, statements, and proofs in a formal system so that a machine can verify them according to that system’s rules.

For example, the familiar theorem

\[ a+b=b+a \]

is not yet a fully specified formal statement. We must know what \(a\) and \(b\) are, which operation \(+\) denotes, and what properties the operation satisfies.

A formal version could quantify over elements of a commutative additive structure:

\[ \forall a,b,\quad a+b=b+a. \]

A theorem prover then checks the precise formal statement and its proof. This eliminates certain classes of ambiguity and proof error, provided the formalization faithfully represents the intended claim and the trusted checking system behaves correctly.

The current state is much stronger than in 2016. Formalization now includes large libraries of abstract algebra, analysis, topology, number theory, and other areas. The Lean community’s library, Mathlib, is a shared, maintained infrastructure rather than merely a collection of isolated demonstrations.

image

GitHub

+1

However, formalization still has different levels of difficulty:

• Formalizing an elementary theorem using existing library definitions.
• Formalizing a research theorem whose supporting concepts already exist.
• Developing missing mathematical infrastructure.
• Translating an entire paper, textbook, or proof network.
• Formalizing a new mathematical discovery while preserving the author’s intended meaning.

These should not be treated as equivalent tasks.

6. Digital mathematics

Digital mathematics now includes at least four distinct layers:

1. Digital documents: PDFs, scanned books, LaTeX manuscripts, HTML papers.
2. Structured notation: mathematical expressions represented as parseable trees or markup.
3. Formal mathematics: definitions and proofs encoded in proof-assistant languages.
4. Computational mathematics: executable algorithms, symbolic computation, numerical experiments, and scientific models.

The important insight is that a document can be digitally accessible without being semantically understood by a computer.

A scanned page may contain a correct proof, but OCR alone does not reveal its logical dependencies. LaTeX can preserve the author’s notation while leaving many semantic choices implicit. A formal proof can be machine-checkable while being difficult for a human to read.

The current MathML 4 specification explicitly distinguishes mathematical notation from mathematical content, and describes applications such as automatic reasoning, mathematical search, industrial and scientific applications, and interactive textbooks.

image

W3C

The broader opportunity is to connect these layers rather than force every author to begin by writing fully formal proof code.

7. Semantic preservation

Semantic preservation is one of the most important unsolved aspects of the project.

Suppose a paper states:

Every continuous real-valued function on a compact space is bounded.

A formalization must settle questions that the informal sentence leaves implicit:

• Is the space compact in the topological sense?
• Is the function defined on the whole space?
• Is its codomain \(\mathbb R\), or is it a subspace of \(\mathbb R\)?
• Is continuity defined relative to the intended topologies?
• Does the result require compactness, or a stronger condition?
• Is the conclusion boundedness of the image, or the existence of a finite bound?

The formal theorem may be correct, but the translation can still be wrong if the assumptions have been altered or omitted.

This is not a hypothetical problem. The miniF2F-v2 study found discrepancies between informal and formal statements in more than half of the original benchmark problems it examined. Correcting those discrepancies substantially changed the measured performance of the end-to-end pipeline.

image

NeurIPS Proceedings

A future semantic mathematics system should therefore preserve more than a proof term. It should maintain a traceable chain:

\[ \text{Original statement} \longrightarrow \text{Interpretation} \longrightarrow \text{Formal statement} \longrightarrow \text{Proof}. \]

Each arrow needs its own evidence, tests, or review process.

8. Global library structure

A global library should not be imagined as one enormous file or a single centralized proof assistant.

A more realistic architecture would have several interconnected layers.

Human-facing sources

Papers · Books · Notes · Diagrams · Research datasets

Semantic extraction and alignment

Definitions · Symbols · Assumptions · Theorem statements · Provenance

Mathematical knowledge graph

Concept relationships · Dependencies · Equivalent results · Citations

Formal systems

Lean · Rocq · Isabelle · HOL Light

Computational systems

CAS · Numerical tools · Scientific software

Applications

Search · Proof verification · Education · Research · Engineering · AI agents

This is a proposed architectural synthesis, not a claim that a single implementation currently provides all these layers.

Its key principle is that each mathematical object should have a stable identity, provenance, and explicit relationships to the representations used by different tools. The architecture should allow a user to find a theorem even when the theorem is stored in another proof assistant or originally published in a PDF.

9. Library use cases

A semantic library becomes valuable when it can perform work that ordinary document search cannot.

Many individual use cases are already served by specialized systems. The missing piece is a coherent way to connect them.

For example, a theorem prover may verify a lemma, but a separate discovery interface is needed to locate it. A mathematical search engine may locate a paper, but it may not know whether the theorem has been formally verified. A computer algebra system may simplify an expression, but its result is not automatically a proof in an arbitrary formal foundation.

10. Scaling the project

There are two different scaling problems.

Scaling formalization: Can we formalize more mathematics, faster, with fewer expert hours?

Scaling semantic infrastructure: Can we make all those formalizations discoverable, maintainable, interoperable, and meaningful across systems?

AI has made significant progress on the first problem. The 2026 formalization of Munkres’ Topology and the reported Lean formalization of Fermat’s Last Theorem illustrate how large projects can be decomposed into many smaller tasks, assisted by AI agents, and checked by proof infrastructure.

image

arXiv

+1

But volume alone does not solve the second problem. A library containing millions of lines of formal code could still be difficult to search, maintain, explain, or translate. A small, carefully designed semantic vocabulary may be more useful for some applications than a vast collection of unconnected proof artifacts.

Scaling therefore requires at least five complementary improvements:

• Reusable and well-maintained foundational libraries.
• Better theorem search and dependency analysis.
• Automated formalization with reliable semantic checks.
• Modular project design and versioning.
• Sustainable incentives for mathematicians and software contributors.

11. Foundation selection

A formal foundation specifies the rules and objects through which mathematical statements and proofs are represented.

Different proof assistants make different choices. For example:

• Lean uses dependent type theory and supports a broad ecosystem for formal mathematics.
• Rocq (formerly widely known as Coq) also uses dependent type theory, with its own foundational choices and ecosystem.
• Isabelle/HOL is based on higher-order logic.
• HOL Light uses a higher-order logic foundation.
• Mizar formalizes mathematics using a set-theoretic approach.

The practical question is not merely which foundation is philosophically best. It is which foundation supports the mathematics, proof engineering, automation, community, and interoperability requirements of a project.

For a universal semantic library, it is unlikely that one formal foundation will immediately replace all the others. A more realistic goal is to preserve a common semantic description where possible, while explicitly recording the foundational commitments that cannot be ignored.

A theorem may translate directly between two systems, require a proof transformation, or fail to translate without extra assumptions. A robust system should record which case applies rather than treating every translation as automatically valid.

12. Homotopy type theory

Homotopy type theory (HoTT) connects type theory with ideas from homotopy theory. In univalent foundations, equivalence between mathematical structures plays a central role in how objects are understood.

Its importance to semantic mathematics is conceptual as well as technical. It encourages us to ask whether mathematical structures should be identified by their internal representation or by the equivalences that preserve their essential properties.

For example, two representations of a structure may differ internally while being mathematically equivalent. A semantic library should ideally be able to express that relationship without incorrectly treating every difference in representation as a difference in mathematical content.

However, HoTT is not a universal interchange format for all mathematical software. Adopting it would not automatically translate existing Lean, Rocq, Isabelle, or computer algebra libraries into one another.

Its current role is better understood as one important foundational and conceptual approach among several, particularly relevant to the semantics of structures and equivalences.

13. Dependent type theory

Dependent type theory permits types to depend on values. This makes it possible to express rich mathematical statements directly in a formal language.

For instance, a vector type can encode its length:

\[ \operatorname{Vector}(A,n), \]

meaning a vector of elements of type \(A\) whose length is \(n\).

A function consuming such a vector can specify its expected length in its type. The type system can then rule out certain invalid operations before they occur.

For theorem proving, dependent types allow propositions and their proofs to be represented within the same formal framework. Under the Curry–Howard correspondence, propositions correspond to types and proofs correspond to terms inhabiting those types.

This expressiveness is one reason dependent type theory supports both programming and mathematical formalization. Lean’s official documentation explicitly presents dependent type theory and interactive theorem proving as core subjects.

image

Lean Lang

Its trade-off is complexity. A rich formal language can express more mathematics, but it can also make elaboration, proof search, notation, and translation more demanding.

The semantic-language project must therefore decide not only what can be represented, but also what humans and automated systems can work with efficiently.

14. Formalizing notation

Notation is not merely decoration. It often carries implicit conventions, contextual assumptions, and information about mathematical structure.

Consider the symbol \(+\). It might denote:

• Addition on natural numbers.
• Addition on real numbers.
• Vector addition.
• Addition in an abstract group.
• Addition of matrices.
• A formally defined operation on another structure.

A notation parser can recognize the symbol. A semantic system must determine which operation is intended.

The same problem occurs with \(f^{-1}\), which may refer to an inverse function, an inverse image, or a multiplicative inverse depending on context.

The current mathematical markup ecosystem provides structured notation and content representations, but it does not eliminate the need for context, declarations, and domain-specific semantics. MathML 4 explicitly acknowledges that mathematical notation can be ambiguous and context-dependent.

image

W3C

A practical solution is to represent a symbol together with its declaration, type, scope, and relevant assumptions. The rendered notation can then be changed without changing the underlying mathematical object.

15. Semantic challenges

The main semantic challenges are deeper than parsing symbols.

A semantic system must account for:

1. Context: Which definitions and assumptions are in scope?
2. Types and domains: What kinds of objects can a symbol denote?
3. Partiality: Is an expression always defined?
4. Overloading: Can one symbol denote different operations?
5. Equivalence: When are two representations mathematically interchangeable?
6. Foundations: What logical principles does the theorem rely on?
7. Provenance: Where did a definition or theorem come from?
8. Translation: Does a transformed statement mean the same thing?
9. Human intent: What did the original author mean, beyond the literal notation?

The last point is especially difficult. Human mathematical writing is often intentionally economical. An expert reader supplies conventions and background knowledge that a machine must either recover or ask the author to make explicit.

A future semantic language should not pretend that all mathematical meaning can be inferred from surface syntax alone.

16. Theorem structure

A theorem is more than a sentence followed by a proof.

Its structure typically includes:

• A name and stable identifier.
• A proposition or statement.
• Explicit assumptions.
• Definitions and notation.
• Dependencies on earlier results.
• A proof or a reference to a proof.
• Its foundational assumptions.
• A human-readable explanation.
• Provenance, authorship, version, and publication context.

For a theorem about continuous functions on compact spaces, the system should identify the definitions of compactness and continuity used in that theorem and the precise relationship between its assumptions and conclusion.

The theorem should also be connected to related statements: stronger versions, special cases, equivalent formulations, and applications.

Formal libraries already capture much of this structure internally. The unresolved task is making it available through a common semantic and discovery layer across libraries, documents, and tools.

17. Importance of semantics

Semantics determines what a mathematical expression means, not just how it looks.

This distinction becomes essential when a system is asked to do more than display mathematics. A theorem-search engine must distinguish related but non-equivalent results. A proof assistant must know exactly which proposition is being proved. An AI system must not silently change a hypothesis while rewriting a statement.

A semantic representation can also enable multiple visualizations of the same underlying expression: conventional notation, spoken mathematical language, a structured tree, or a formal statement.

But semantics must be precise enough for the intended task. A representation designed for accessible speech may be sufficient for a screen reader but insufficient to certify a proof. A formal proof term may be sufficient for a kernel but insufficient to explain the theorem to a student.

The lesson is that mathematical semantics needs multiple layers of fidelity, with explicit guarantees for each.

18. Algebraic structures

Algebra provides an especially clear demonstration of why semantic reuse matters.

A group, ring, field, module, or vector space is not merely a collection of elements. It consists of a carrier together with operations and axioms.

For example, a group is a set-like type \(G\), a multiplication operation, an identity element, inverses, and laws governing those operations.

Once a theorem is proved at the appropriate level of abstraction, it can be reused for many concrete groups. A result about arbitrary groups should not have to be reproved separately for every group of matrices, permutations, or symmetries.

Formal libraries make this kind of reuse possible by organizing results around abstract structures and their relationships.

The semantic challenge is to preserve those abstraction relationships when moving between systems. If two libraries encode groups using different type classes, coercions, or conventions, a translation must preserve the structure and theorem dependencies—not just rename the symbols.

19. Concrete incompleteness

The word incompleteness has several meanings in this field, and they should not be confused.

• Gödel incompleteness: Certain sufficiently expressive, consistent formal systems cannot prove every true statement expressible in their language.
• Library incompleteness: A formal library does not yet contain a desired theorem or definition.
• Formalization incompleteness: A paper has been partially formalized, with gaps remaining.
• Proof incompleteness in a workflow: An AI agent has generated a statement or proof sketch, but the result has not been fully checked.

The latter three are engineering problems, not direct consequences of Gödel’s theorems.

A semantic library can become much more complete in coverage without eliminating the theoretical limits of formal systems. Conversely, the existence of undecidable propositions does not make a large, useful formal library impossible.

The practical objective is to make the coverage and gaps explicit: which results are formalized, which are only described informally, which depend on additional axioms, and which are still conjectural.

20. Decidability problems

A problem is decidable when an algorithm can determine the correct answer for every valid input and terminate.

Some mathematical tasks are decidable within restricted theories. Others are undecidable in general. General theorem proving in expressive logics cannot be reduced to a universally terminating algorithm that decides every theorem.

This matters for the semantic-language vision because a common representation should not promise that every mathematical question can be answered automatically.

A system can still provide useful services:

• Decide particular classes of formulas.
• Normalize or simplify supported expressions.
• Search for a proof.
• Find counterexamples in bounded domains.
• Verify a supplied proof.
• Report that a task remains unresolved.

The distinction between not proved, disproved, not yet found, and undecidable in the chosen setting is essential.

For example, failure to find a proof using a tactic does not establish that the theorem is false. A semantic library should preserve this distinction in its results and interfaces.

21. Diagrammatic reasoning

Diagrams are central to many areas of mathematics, including geometry, topology, category theory, algebraic topology, and mathematical physics.

Yet a diagram can play several different roles:

• Illustration of an idea.
• Visual shorthand for a formal construction.
• Representation of relationships between objects.
• Part of a proof whose correctness depends on structural properties.
• An informal sketch whose details must be supplied in a rigorous argument.

A semantic system needs to distinguish these roles. Merely storing an image of a commutative diagram does not make the diagram machine-checkable.

In category theory, for example, a diagram can be represented as a collection of objects and morphisms, together with equations expressing commutativity. The semantic representation contains more than the arrows drawn on the page.

For geometric diagrams, the intended assumptions may include incidence, orientation, metric relations, or a particular construction. Recovering those assumptions from a picture alone is often ambiguous.

Current formal systems can represent and verify many diagrammatic arguments when the underlying objects and relations are formalized. A universal solution for automatically interpreting arbitrary mathematical diagrams remains a separate research challenge.

Part II — Community, infrastructure, and adoption

22. Notational issues

Notation remains one of the largest barriers between ordinary mathematical writing and a reusable semantic representation.

Consider:

\[ \int_a^b f(x)\,dx. \]

Its meaning depends on more than the symbols. Is \(f\) continuous, measurable, or integrable in some specified sense? Is the integral Riemann, Lebesgue, or another kind of integral? What are the domain and codomain of \(f\)? Which measure or integration convention is intended?

An expert reader may recover the intended interpretation from surrounding text. A formal system needs enough explicit information to elaborate the expression unambiguously.

The emerging solution is to separate three layers:

1. Notation: what the author writes.
2. Interpretation: what the expression denotes in context.
3. Formal meaning: the object or proposition that a formal system represents.

MathML and OpenMath contribute to the first two layers. Proof assistants provide precise formal meanings within their respective foundations. A universal semantic language would need reliable mappings between these layers.

23. History of formalization

The field did not begin in 2016. Its history includes mathematical logic, automated deduction, computer algebra, interactive theorem proving, and digital libraries.

Some important milestones provide context:

• 1930s: Formal logic and foundational investigations established much of the theoretical background.
• 1950s–1970s: Early computer-based theorem proving and symbolic computation began to turn mathematical reasoning into executable procedures.
• 1970s–1990s: Interactive proof assistants and formal proof languages developed into more capable systems.
• 1990s–2010s: Major formal verification projects demonstrated that substantial mathematical results could be checked by computers.
• 2016: The Fields Institute workshop on semantic representation of mathematical knowledge brought together researchers to discuss a shared semantic language and global digital mathematics library.
• 2020s: Large collaborative mathematical libraries, LLM-assisted theorem proving, and document-level autoformalization substantially expanded the practical scale of formalization.
• 2025–2026: Research projects reported automated formalization of substantial textbooks and major classical theorems.

The historical lesson is that the current progress builds on decades of work in formal logic, libraries, and proof engineering. AI has accelerated parts of the workflow, but it did not create the foundational infrastructure on which the new systems depend.

For the 2016 workshop, the critical primary source remains the workshop white paper. It reported that the meeting did not achieve consensus on a concrete semantic language. The present-day progress should be evaluated against that original gap, not just against the number of new theorem-proving tools.

24. Community engagement

Mathematical formalization depends on communities that create definitions, maintain libraries, review contributions, and teach newcomers how to contribute.

Mathlib is a particularly important example. It is a user-maintained Lean library with documented conventions, contribution guidance, generated documentation, and a public discussion community.

image

GitHub

Community participation has become more important as libraries grow. A contribution can affect many downstream theorems, so library maintainers must balance mathematical generality, naming, dependency structure, performance, and long-term maintainability.

For a global semantic mathematics project, community engagement should extend beyond formal proof developers to:

• Research mathematicians.
• Mathematical publishers and librarians.
• Computer algebra developers.
• Proof-assistant communities.
• AI researchers.
• Educators and accessibility specialists.
• Scientific and engineering organizations.

The objective should not be to persuade every mathematician to use one proof assistant. It should be to make participation useful even for people who work primarily with conventional papers and notation.

25. Modularization

A global mathematics project must be modular or it will become difficult to maintain.

Useful units of organization include:

• Mathematical concepts and definitions.
• Theorems and proofs.
• Subject-specific libraries.
• Formal foundations.
• Document-level formalization projects.
• Translation interfaces.
• Search and visualization services.
• Provenance and version information.

Modules should have explicit dependencies. If a definition changes, the system should be able to identify which results may need to be rebuilt or rechecked.

AI formalization projects also benefit from modularization. The 2026 LeanFlow research studies structured workflows for translating papers into Lean projects, while the Fermat’s Last Theorem formalization used a dependency graph and intermediate theorem tasks to coordinate a large proof effort.

image

arXiv

+1

However, dividing a project into modules is not enough. Modules must have stable interfaces and compatible semantics. Otherwise, modularization merely produces many smaller, disconnected libraries.

26. Mathematics education

Formalization can improve mathematics education in several ways.

A student could explore a theorem, inspect its assumptions, test examples, view a dependency graph, and compare an informal proof with a formal one. An interactive textbook could connect a definition to the theorems that depend on it.

Lean already has a growing educational ecosystem, including the Natural Number Game, Mathematics in Lean, and introductory resources listed by the official Lean website.

image

Lean Lang

The major opportunity is to make the transition from ordinary mathematical thinking to formal reasoning gradual.

A student should be able to begin with familiar notation and receive help understanding why a particular formal statement requires an explicit domain or assumption. The system should teach mathematical meaning rather than merely report syntax errors.

There are also limitations. Formalization introduces its own concepts, notation, and debugging work. A student can spend substantial time satisfying a proof assistant’s requirements without necessarily understanding the underlying mathematics more deeply.

The educational challenge is therefore to design activities in which formal checking supports conceptual understanding rather than becoming an end in itself.

27. Barriers to adoption

Several barriers remain even with improved AI assistance.

AI can reduce some costs, but it cannot remove the need to decide what should be formalized, maintain the resulting code, and verify that the formal artifact captures the intended mathematical claim.

A particularly important adoption principle is to allow partial participation. A researcher might contribute a formal definition, a verified theorem, a document annotation, a translation rule, or a useful test case without formalizing an entire paper.

28. Industrial applications

Semantic mathematics is not restricted to pure mathematics.

In engineering and industry, formal mathematical specifications can help describe and verify properties of algorithms, numerical methods, control systems, and software.

Potential applications include:

• Verifying algebraic transformations in symbolic computation.
• Checking mathematical assumptions in scientific software.
• Validating algorithms used in safety-critical systems.
• Connecting mathematical models to executable implementations.
• Reusing formally verified results in engineering workflows.

Formal verification is already an established field, but its application to a specific industrial system depends on the system’s model, the properties being verified, and the relationship between the model and the actual implementation.

A semantic mathematical library could reduce duplicated work by making verified mathematical results easier to discover and reuse. However, a theorem proved about an abstract model does not automatically establish that a physical system behaves correctly. The implementation and its connection to the model must also be verified.

29. Need for verification

The need for verification becomes more urgent as AI generates more mathematical statements and proofs.

A language model can produce a convincing-looking proof that contains a subtle logical error. It can also formalize a different theorem from the one a mathematician intended. These are distinct failure modes.

Formal proof checking addresses the first problem by verifying that a proof term follows the formal system’s rules. The second requires validating the formal statement against the original mathematical claim.

The Lean kernel is central to this model. The Lean 4 repository’s kernel implementation contains the type-checking core that checks formal declarations. The number of source lines in that directory is not, by itself, a complete measure of the trusted computing base: runtime and supporting components also matter.

The 2026 Fermat’s Last Theorem project illustrates a more extensive verification strategy. Its published repository describes a clean Lean build, an audit of axioms, a comparison with Mathlib’s statement, and acceptance by an independent Lean kernel implementation written in Rust, nanoda, after project-specific patches. These are meaningful checks, though the scope of the assurance depends on the artifact and verification process.

image

anthropics/fermats-last-theorem · GitHub

For a semantic library, verification should cover at least three distinct questions:

1. Proof correctness: Does the formal proof check?
2. Statement fidelity: Does the formal theorem express the intended mathematical claim?
3. Artifact integrity: Can the proof, dependencies, and relevant source artifacts be inspected and reproduced?

No single check substitutes for all three.

30. Economics and incentives

Formal mathematics requires investment in definitions, proofs, library infrastructure, maintenance, and education.

The economic question is not simply whether AI can generate code more cheaply. It is whether the resulting mathematical knowledge can be reused enough to justify the cost of producing and maintaining it.

A formalized theorem can benefit many later projects if its definitions are general, its proof is maintainable, and its dependencies are stable. A narrowly formalized result with extensive duplicated infrastructure may have much lower reuse value.

A sustainable ecosystem needs incentives for:

• Mathematicians who contribute formalizations.
• Developers who maintain proof infrastructure.
• Reviewers who validate statements and proofs.
• Publishers who preserve machine-readable artifacts.
• Organizations that fund open mathematical resources.
• Educators who create accessible learning materials.

Academic credit, funding, open licenses, persistent identifiers, citation mechanisms, and reproducible artifacts can all contribute.

A key unresolved problem is how to reward work whose benefits are distributed across a large network of later results. The global-library vision depends on treating reusable mathematical infrastructure as valuable scholarly output, not merely as supporting code.

Part III — Translation, AI, and major achievements

31. Translation techniques

Translation is the bridge between different mathematical representations.

There are several distinct translation tasks:

• LaTeX to structured mathematical markup.
• Scanned pages to recognized mathematical notation.
• Natural-language statements to formal propositions.
• Informal proofs to formal proofs.
• One proof-assistant language to another.
• One mathematical foundation to another.
• Formal mathematics to human-readable explanations.

These translations have different requirements.

A LaTeX-to-MathML conversion may preserve the visible expression while leaving some meaning ambiguous. An informal-to-Lean conversion must identify the intended definitions and assumptions. A Lean-to-Isabelle translation may need to reconstruct a proof in a different logic or library environment.

The 2024–2026 Rocq–Isabelle interoperability project is an example of research aimed at translating libraries through Dedukti and related formal systems. Its existence demonstrates that cross-system translation is an active research direction, not that arbitrary libraries can already be exchanged transparently.

image

blanqui.gitlabpages.inria.fr

A robust translation system should report the strength of its guarantee. For example:

• Syntactic conversion: the output is valid syntax.
• Structural conversion: the expression tree or declaration structure is preserved.
• Semantic correspondence: the source and target objects have a defined relationship.
• Proof-preserving translation: the target theorem is justified under stated conditions.
• Verified equivalence: a formal argument establishes the relevant equivalence or preservation property.

This hierarchy would prevent a successful file conversion from being mistaken for a mathematically correct translation.

32. Current achievements

Several achievements show how far the field has progressed.

ReasLab IDE

Reusable formal libraries

Mathlib provides a shared foundation for large amounts of formalized mathematics, with conventions and community processes for extending it.

image

GitHub

Topology - Munkres J.R. - 2000

Large-scale textbook formalization

The 2026 Munkres topology project reported 806 fully proved results across 39 sections, with over 85,000 lines of Isabelle/HOL code and zero sorry placeholders.

image

arXiv

Fermat’s Last Theorem – Trinity College Library, Cambridge

Formalization of major classical mathematics

In September 2026, Anthropic announced an end-to-end Lean formalization of Fermat’s Last Theorem. The released artifact and verification reports make this a particularly significant milestone for AI-assisted formal mathematics.

image

Anthropic

+1

PPT - Scientific Markup Languages Birds of a Feather Brief Overview of MathML PowerPoint Presentation - ID:4374530

Mathematical markup and accessibility

MathML continues to develop structured representations for mathematical notation and content, with applications in accessibility, publishing, and computational processing. MathML 4 remained a Working Draft at the October 2026 cutoff.

image

W3C

These achievements represent real progress, but they measure different things. A formal library measures accumulated reusable mathematics. A textbook formalization measures the feasibility of converting a substantial body of content. A theorem-proving benchmark measures performance on a particular task distribution. A markup standard supports structured representation and interchange.

None of these alone establishes that a universal semantic language has been completed.

33. Future costs

Even if AI makes theorem formalization dramatically cheaper, the total cost of a semantic mathematical library will remain broader than the cost of generating proof code.

The long-term cost categories include:

• Formalization: converting mathematical content into precise definitions and proofs.
• Semantic validation: checking that the formalization matches the original intent.
• Infrastructure: maintaining libraries, search systems, storage, and build pipelines.
• Interoperability: creating and maintaining translation interfaces.
• Quality assurance: auditing assumptions, dependencies, and generated artifacts.
• Curation: organizing concepts, names, versions, and provenance.
• Education: teaching researchers and students to use the system.
• Governance: deciding how standards and shared resources evolve.

AI may reduce the human effort needed for some of these tasks, but it can also increase the volume of material that needs review and maintenance.

A rational economic strategy is therefore not to formalize everything indiscriminately. It is to prioritize high-value mathematics: foundational definitions, widely reused theorems, safety-critical results, important research proofs, and areas where formalization enables substantial new capabilities.

34. Future of proof assistants

Proof assistants are likely to become more integrated into mathematical research workflows.

Instead of treating the prover as a specialized editor used only by formal-methods experts, researchers may increasingly use it through document editors, AI agents, notebook environments, and collaborative mathematical workspaces.

Useful future capabilities include:

• Better support for informal-to-formal workflows.
• More effective theorem search.
• Improved proof reconstruction and minimization.
• Richer explanations of proof failures.
• Easier library migration and dependency management.
• More portable proof artifacts.
• Better support for long-running, collaborative formalization projects.

The important design choice is to preserve a small, dependable checking core while allowing more complex and probabilistic components to assist with proof discovery.

AI agents can suggest definitions, lemmas, and proof strategies. The proof assistant should remain responsible for checking the formal result rather than trusting the agent’s confidence.

35. Proof visualization

Formal proof code is machine-checkable, but often difficult for humans to inspect.

A semantic library could offer several synchronized views of a theorem:

• The original informal statement.
• Its formal statement.
• A natural-language explanation.
• A proof outline.
• A dependency graph.
• The underlying formal proof.
• A record of assumptions and axioms.
• A comparison with related formulations.

For example, a proof dependency graph might reveal that a theorem depends on compactness, a particular form of continuity, and a supporting result in topology. A user could inspect each dependency and determine which parts of the argument are new.

The visualization must not hide important logical information. A simplified explanation should be clearly distinguished from the formal proof, and a dependency graph should not imply that a theorem has been proved merely because all its nodes are displayed.

The goal is not to replace formal proof objects with diagrams. It is to make the structure and meaning of verified mathematics easier to explore.

36. AI in theorem proving

AI-assisted theorem proving has become one of the most rapidly advancing parts of the field.

It is useful to distinguish three tasks:

1. Autoformalization: translating informal mathematics into formal definitions or statements.
2. Automated proving: finding a proof of a supplied formal theorem.
3. End-to-end formal mathematics: interpreting an informal problem, formalizing it, constructing a proof, and verifying that the result matches the original claim.

The third task is the most relevant to a semantic language of mathematics because it requires the entire chain of meaning to remain intact.

The 2025 miniF2F-v2 study showed why separate success rates for formalization and theorem proving can be misleading: statement discrepancies materially reduced the end-to-end performance of systems evaluated on the original benchmark.

image

NeurIPS Proceedings

The 2026 Fermat’s Last Theorem project demonstrates the growing scale of AI-assisted formalization. But the achievement should be understood precisely: the system formalized an already established theorem using existing mathematical knowledge, libraries, and prior human work. It was not a new proof of the theorem in the historical sense, nor did it independently invent all the mathematics on which the proof depends.

image

Anthropic

+1

The future research question is how to make these capabilities general, auditable, and useful for mathematical research beyond selected benchmarks and major demonstrations.

37. Formalizing Wolfram-style mathematics

Wolfram Language and Mathematica provide powerful symbolic and computational representations of mathematics. They can manipulate expressions, represent functions, perform symbolic transformations, and support scientific computation.

But a symbolic expression being executable or simplifiable does not automatically mean that it is a formally proved theorem in a proof assistant.

For example, a computer algebra system might simplify an expression under particular assumptions. A formal theorem prover needs a precise statement of those assumptions and a proof that the transformation preserves the expression’s meaning in the relevant domain.

A bridge between computational mathematics and formal proof would ideally preserve:

• The symbolic expression.
• Its domain and assumptions.
• The transformation being applied.
• The mathematical conditions under which the transformation is valid.
• A proof certificate or formal derivation, where available.

The long-term goal should not necessarily be to make one language replace the other. It should be to let symbolic computation, numerical methods, and formal proof cooperate through explicit interfaces and guarantees.

38. Machine learning for formalization

Machine learning can assist at multiple points in a formalization workflow:

• Recognizing mathematical expressions in documents.
• Identifying likely definitions and notation.
• Predicting formal theorem statements.
• Retrieving relevant library results.
• Suggesting intermediate lemmas.
• Generating candidate proof terms.
• Repairing failed proof attempts.
• Explaining formal errors.
• Estimating which tasks are likely to succeed.

The most effective systems increasingly combine language models with external tools and formal feedback.

For example, LeanFlow studies a structured workflow for converting mathematical papers into Lean projects. Its 2026 report evaluates the influence of workflow mechanisms and model choices on project completion, tool calls, and token use.

image

arXiv

This illustrates an important architectural principle: a successful system needs more than a powerful model. It needs retrieval, project structure, proof checking, task management, and a way to recover from failures.

For semantic mathematics, the machine-learning component should propose interpretations and formalizations, while the surrounding system tracks evidence and uncertainty. It should never silently equate plausible language generation with verified mathematical meaning.

39. Case studies

Three case studies illustrate different aspects of the current state.

Case study A — Munkres’ Topology in Isabelle/HOL

Reported completed formalization

Researchers reported more than 85,000 lines of Isabelle/HOL code covering 39 sections and 806 fully proved results, with zero sorry placeholders. The project used AI agents and Isabelle’s proof automation. This demonstrates the feasibility of large-scale textbook formalization, while leaving questions of long-term maintenance, exposition quality, and cross-system interoperability open.

image

arXiv

Case study B — Fermat’s Last Theorem in Lean

Released formal artifact

In September 2026, Anthropic reported an end-to-end Lean formalization produced largely autonomously in 11 days, with 29,500 intermediate theorems and roughly 13 million lines of code. The project includes verification documentation and an independent-kernel check. It demonstrates AI’s ability to coordinate large formalization work, but relies on extensive prior mathematical and library infrastructure.

image

Anthropic

+1

Case study C — MathML 4

Active standards development

MathML 4 continues to develop ways of representing mathematical notation and content for web publishing, accessibility, and software interchange. As of 23 October 2026, it was a W3C Working Draft. It is a useful semantic infrastructure component, but it does not provide a complete formal proof language or a universal library of theorems.

image

W3C

+1

Together, these cases show that the field is advancing on three different fronts: large-scale formal content, automated production of formal proofs, and structured representation of mathematical notation. The next major challenge is to connect them reliably.

Part IV — What mathematics is, and what a universal system should do

40. Formalism as an ideal

Formalism is valuable because it makes assumptions, definitions, and inference rules explicit. A proof assistant can check whether a formal derivation follows the rules of the chosen system.

But formalization is not a neutral conversion from human writing into code. It involves choices about definitions, foundations, notation, and the level of abstraction.

A formal proof can be perfectly valid while the chosen formal statement fails to capture the theorem the author intended. Conversely, an informal proof can be mathematically illuminating even when translating every step into formal code would be expensive.

The ideal should therefore be formal rigor where required, with transparent links to human mathematical understanding.

A universal system should make clear which claims have been formally checked, which are informal explanations, and which rely on interpretation or unverified assumptions.

41. Nature of mathematics

Mathematics is not only a collection of propositions and proofs.

It also includes definitions, examples, conjectures, counterexamples, constructions, algorithms, diagrams, heuristics, explanations, and the process by which mathematicians discover new concepts.

A semantic library that stores only finished theorems would capture an important but incomplete part of mathematical activity.

For example, an open research problem may have several partial results, computational experiments, proposed approaches, and counterexamples to stronger conjectures. A useful system should preserve those relationships without mistakenly classifying a conjecture as a theorem.

It should also support different mathematical viewpoints. Two researchers may use different definitions or foundations to study related structures. The library should be able to describe the relationship between their approaches rather than forcing every concept into one rigid hierarchy.

The long-term objective is not to dictate how mathematics must be done. It is to make mathematical knowledge easier to understand, connect, verify, and reuse.

42. Automated invention

Automated theorem proving and mathematical discovery are related, but they are not the same task.

A system can prove a supplied theorem without discovering the theorem. It can also find a proof of a conjecture that a human has formulated, without having invented the conjecture or identified its significance.

Automated mathematical invention can involve:

1. Generating conjectures from existing structures.
2. Searching for examples and counterexamples.
3. Identifying patterns in mathematical data.
4. Proposing definitions that unify existing results.
5. Discovering useful intermediate lemmas.
6. Proving new statements.
7. Evaluating whether the result is significant and genuinely new.

Formal verification can help establish the correctness of a discovered result. It does not automatically establish novelty, usefulness, or conceptual importance.

A semantic library could support discovery by exposing dependencies, equivalent theorems, known special cases, and gaps in formalized knowledge. This would make it easier for AI systems and human mathematicians to identify meaningful research directions.

43. Accessible organization

A universal mathematical library needs several forms of organization simultaneously.

A textbook organizes knowledge pedagogically. A research paper organizes it around a particular contribution. A formal library organizes it according to dependencies and reusable definitions. A semantic graph organizes it around concepts and relationships.

These organizations are complementary rather than interchangeable.

A useful library should support searches such as:

• Find theorems involving compactness and continuity.
• Find a formal proof of a statement in real analysis.
• Show which definitions a theorem depends on.
• Compare two formulations of a result.
• Find a proof assistant that contains the result.
• Identify a missing lemma needed for a formalization.
• Trace a formal theorem back to its source paper.
• Show which results may be affected by a changed definition.

The key is to combine semantic search with formal structure, provenance, and human-readable explanations.

A single tree of subject classifications will not be enough. Mathematical results often belong to several areas and can be useful in unexpected contexts.

44. Importance of machine learning

Machine learning is important because the amount of mathematical writing that already exists far exceeds what has been fully formalized.

AI can help bridge that gap by reading documents, identifying mathematical structure, suggesting formal statements, retrieving related results, and generating candidate proofs.

However, a machine-learning model does not automatically know whether a formal statement faithfully represents the original author’s intent. Nor does a high benchmark score guarantee reliable performance on unfamiliar mathematical research.

The strongest architecture is therefore a collaboration between probabilistic and deterministic components:

• Probabilistic components propose interpretations, search strategies, lemmas, and proofs.
• Deterministic components parse and type-check formal expressions, execute algorithms, and verify proof artifacts.
• Human reviewers resolve ambiguous intent, assess significance, and validate the relationship between the source and its formalization.

This division of responsibility makes it possible to exploit AI’s flexibility without treating its outputs as inherently trustworthy.

45. Future of mathematics

The most plausible future is not a world in which all mathematics is immediately replaced by formal code. It is a world in which formal verification and semantic infrastructure become increasingly available throughout mathematical work.

Mathematicians may continue writing papers in conventional notation, while tools produce formal statements and proofs alongside them. Research libraries may provide dependency-aware search and verified theorem reuse. AI agents may help extend existing formal libraries, while proof assistants check the results.

For that future to be useful, several requirements must be met:

• Mathematical meaning must survive translation.
• Formal libraries must remain maintainable.
• Proof artifacts must be reproducible and auditable.
• Human explanations must remain connected to machine-checkable statements.
• Different foundations must be represented honestly.
• Contributors must have incentives to maintain shared infrastructure.
• AI-generated content must be evaluated against the intended mathematics.

The ultimate measure of success will not be the size of the generated codebase. It will be whether mathematicians can discover, understand, verify, and reuse knowledge more effectively than they can today.

Part V — The 2016 workshop and the position in 2026

46. What has changed since the 2016 workshop?

The 2016 workshop aimed to develop design principles for a semantic representation of mathematical knowledge. Its white paper recorded substantial discussion, but also a crucial limitation: the participants did not reach consensus on a concrete semantic language or a specific actionable direction.

The present situation is different in an important way. The community now has more mature, reusable infrastructure with which to pursue the vision:

• Large formal libraries maintained collaboratively.
• More capable proof assistants and proof-checking workflows.
• Structured mathematical markup for publishing and accessibility.
• Research on interoperability between formal systems.
• AI-assisted formalization of documents and textbooks.
• Automated proof generation combined with formal checking.
• Large-scale case studies demonstrating that substantial mathematical developments can be formalized.

Yet the original global-language problem remains. These systems still differ in foundations, semantics, representation, intended use, and guarantees. Their successes do not automatically combine into a universal library.

The distinction can be summarized as follows.

The evidence supports a clear conclusion: we have progressed from discussing the feasibility of a semantic mathematical library to building many of its essential components, but we have not yet integrated those components into a universal system.

What should be built next?

If the goal is to move the field toward the original vision, I would prioritize the following research and engineering directions.

1. A semantic interchange layer

Define a minimal common representation for mathematical objects, statements, assumptions, provenance, and relationships to formal proofs. It should complement Lean, Rocq, Isabelle, OpenMath, and MathML rather than attempt to replace them all.

2. A semantic-preservation test suite

Build benchmark cases for ambiguous notation, missing hypotheses, overloaded operators, equivalent definitions, and cross-system translations. Measure whether the intended claim survives each transformation.

3. A provenance-aware mathematical knowledge graph

Connect papers, definitions, theorems, proofs, authors, formal libraries, and versions. Distinguish formal verification from informal mention and conjecture.

4. An end-to-end formalization workflow

Combine document parsing, theorem extraction, statement review, library retrieval, AI-generated proofs, kernel checking, and a report linking each formal result to its original source.

5. A sustainable community and governance model

Establish contribution rules, stable identifiers, versioning, licensing, review practices, and incentives for maintaining shared mathematical resources.

A practical research roadmap

I would not start by attempting to formalize all mathematics or by designing an entirely new proof assistant. A smaller demonstrator would provide better evidence and a more manageable engineering path.

1. Phase 1 — Select a bounded mathematical domain

   Choose a domain with reusable definitions and meaningful theorem dependencies, such as elementary real analysis, abstract algebra, or general topology.

2. Phase 2 — Collect source material and formal artifacts

   Link a small set of papers or textbook sections to the corresponding formal definitions and theorems in an existing library.

3. Phase 3 — Create a semantic record format

   Record the statement, assumptions, symbols, source location, formal-system identifier, proof status, and dependencies.

4. Phase 4 — Build search and translation tools

   Let users search by mathematical meaning, inspect related theorems, and trace results between informal documents and formal libraries.

5. Phase 5 — Evaluate semantic fidelity

   Test whether the system preserves hypotheses and conclusions, distinguishes equivalent from merely similar statements, and reports failures honestly.

6. Phase 6 — Expand to another formal system

   Only after the initial representation works should the project attempt cross-system translation, where differences in foundations and libraries become explicit.

The central evaluation metric should not be the number of generated formal declarations. It should be the proportion of mathematical claims whose intended meaning is preserved, whose formal status is known, and whose proof or source can be inspected.

Final conclusion

The vision discussed in 2016 has not disappeared. It has become more technically feasible because the field now has larger formal libraries, stronger proof assistants, better mathematical markup, and AI systems capable of assisting with substantial formalization projects.

But the hardest problem is still not just generating formal code. It is connecting human mathematical intent, precise semantics, formal statements, proofs, and reusable knowledge in a way that is reliable across tools and communities.

The most promising direction is therefore not a single language that forces every mathematician and proof assistant into the same system. It is an interoperable semantic infrastructure that preserves meaning, records assumptions, links multiple representations, supports verified translation, and lets humans and AI reuse mathematical knowledge without confusing plausible interpretation with proven correctness.

That is the gap between the current state and the original global-library vision—and it is a concrete research problem rather than merely a long-term aspiration.

Primary sources and further reading

1. W3C — Mathematical Markup Language (MathML) Version 4.0, Working Draft of 22 October 2026 — mathematical notation, content markup, and web interoperability.

   image

   W3C

2. Lean community — Mathlib 4 — reusable formal mathematics and community infrastructure.

   image

   GitHub

3. Anthropic — Formalizing Fermat’s Last Theorem, 4 September 2026 — a major recent AI-assisted formalization.

   image

   Anthropic

4. NeurIPS 2025 — miniF2F-Lean Revisited — evidence on statement alignment and end-to-end evaluation.

   image

   NeurIPS Proceedings

5. Bryant et al. — Munkres’ General Topology Autoformalized in Isabelle/HOL, 2026 — a large-scale textbook formalization case study.

   image

   arXiv

6. EPFL AI for Math — document-level autoformalization and related research tools.

   image

   aiformath.epfl.ch

7. OpenMath — Overview — an established approach to representing mathematical objects and their semantics.

   image

   OpenMath

8. Wolfram Foundation — 2016 Semantic Representation of Mathematical Knowledge Workshop White Paper — the historical baseline for evaluating the original vision.

Towards a Semantic Language of Mathematics

Historical research article · 2016 perspective · Based on the supplied workshop transcript

1. Introduction: The vision of a global mathematical library

The central ambition discussed in the 2016 workshop was to transform mathematics into a form that computers could understand, organize, search, verify, and help develop — without losing the meaning of the mathematics that humans had created over centuries.

Mathematics is one of humanity’s largest intellectual achievements. Its knowledge is distributed across research papers, books, lecture notes, computational systems, and the minds of mathematicians. Unlike ordinary information, mathematical knowledge has a particularly long useful life: results published decades or even centuries ago may remain essential to modern research.

The workshop explored a fundamental question:

Can we build a common semantic language through which mathematical knowledge can be represented, connected, communicated, and used by both humans and computers?

This was not simply a proposal to scan mathematical books or place papers online. Digitization makes documents accessible; semantic representation makes their mathematical content interpretable. A global mathematical library would aim to connect definitions, assumptions, theorems, proofs, algorithms, notation, historical sources, and computational tools.

The participants came from several communities, including pure mathematics, symbolic and computer algebra, automated reasoning, and interactive theorem proving. One of the workshop’s most important purposes was to bring these communities together and identify practical steps toward a shared vision.

The account below deliberately preserves the 2016 historical perspective. It distinguishes the workshop’s aspirations and contemporary assessments from any claims about what might be possible today. It follows the supplied transcript rather than projecting later AI developments backward into the discussion.

The historical setting is well established. The workshop took place at the Fields Institute in Toronto on February 3–5, 2016, and was organized with the Wolfram Foundation and the International Mathematical Union’s working group on a Global Digital Mathematics Library, with support from the Alfred P. Sloan Foundation. Its stated goal was to establish design principles for a semantic language applicable to mathematics as a whole.

image

2. The vision: What should a mathematical library become?

The idea of a global mathematical library went beyond creating a searchable archive of mathematical publications. The goal was to build a computationally usable representation of mathematical knowledge.

Consider a research paper containing a definition, a theorem, a proof, and several references. A conventional digital library might store the paper as a PDF and allow keyword searches. A semantic library would aim to identify each mathematical object and the relationships between them.

For example, it could represent:

• A definition of a group.
• A theorem stating that every abelian group is a group.
• The assumptions under which the theorem holds.
• A formal proof establishing the result.
• The original publication and author.
• Related theorems and computational procedures.

The distinction is fundamental. A document archive retrieves the document containing a result. A semantic mathematical library aims to retrieve the result itself, explain its dependencies, and potentially make it available for further computation or proof.

The workshop transcript describes a system in which algorithms and theorems coexist, with definitions, sources, and other mathematical information connected to them. Such a system could support both mathematical exploration and verification.

image

2.1 A library for discovery, not merely storage

Suppose a mathematician proves a theorem $T$ and wants to determine whether an equivalent or sufficiently similar result already exists.

A semantic library should ideally help answer:

1. Has this theorem already been proved?
2. Is there a related theorem under different notation?
3. Which definitions and assumptions are required?
4. Can an existing result be adapted to the new problem?
5. Is there an algorithm that computes a relevant quantity?
6. Can the result be formally verified?

These questions explain why ordinary text search is insufficient. Two papers may express the same mathematical idea using different notation, terminology, or foundational assumptions.

The library would need to recognize mathematical meaning, not merely matching words.

2.2 The broader public benefit

The proposed library was also a way to preserve intellectual heritage and make mathematics accessible to researchers outside the specialty in which a result originated.

A physicist might encounter a problem without knowing whether the appropriate tool belongs to differential geometry, algebra, analysis, or another field. A semantically organized library could reveal connections and help identify relevant mathematical methods.

The potential benefits discussed in the workshop included accelerating research and education, improving collaboration, strengthening mathematical software, and reducing unnecessary duplication of work.

image

3. Why standardization was necessary

A shared library requires a way to exchange mathematical knowledge across different systems. This was one of the central technical challenges of the 2016 workshop.

Mathematicians already use a wide range of notation, terminology, proof styles, and foundational systems. Computer algebra systems have their own internal representations, while theorem provers use formal languages with explicit logical rules.

The workshop’s challenge was therefore not simply to invent a new syntax. It was to find a representation that different communities could use without forcing all of them to abandon their existing methods.

3.1 The tension between one standard and many mathematical traditions

A common representation offers substantial benefits:

• Mathematical objects can be exchanged between software systems.
• Results can be searched across repositories.
• Definitions can be reused rather than repeatedly reconstructed.
• Formal verification can be connected to mathematical publications.
• Computational and logical tools can operate on shared data.

However, a rigid standard could impose an unwanted uniformity on mathematical practice.

One researcher might use set theory, another type theory, and another a category-theoretic perspective. Even when their results can be translated into a common framework, their preferred ways of expressing and developing mathematics may differ.

The workshop therefore emphasized finding a reasonable central standard and a way to manage differences, rather than insisting that every mathematician adopt exactly the same notation or logical foundation.

image

3.2 Standardization as a coordination problem

The problem has both a technical and a social dimension.

Technically, a standard must specify how mathematical objects, statements, assumptions, and relationships are represented. Socially, it must be acceptable to the people who create and use mathematical knowledge.

A theoretically elegant language would not be enough if it proved too difficult to use or could not accommodate important areas of mathematics.

The practical strategy emerging from the workshop was to identify achievable intermediate steps, determine where consensus was possible, and use real mathematical examples to evaluate the proposed language.

4. Bridging mathematical communities

The workshop brought together researchers from communities that had developed related but distinct approaches to computation and mathematical reasoning.

Two particularly important communities were:

• Computer algebra: systems that manipulate mathematical expressions, simplify formulas, calculate symbolic results, and solve classes of mathematical problems.
• Automated and interactive theorem proving: systems that search for proofs or allow a human to construct a proof whose logical correctness can be checked by a computer.

These approaches were complementary, but they had not historically developed as one unified environment.

4.1 Symbolic computation and proof verification

Consider the equation

A computer algebra system can factor the expression:

and calculate the solutions $x=1$ and $x=-1$ over the real numbers.

A theorem prover addresses a different question: under explicitly specified definitions and assumptions, can the assertion be established through valid logical steps?

The first capability emphasizes computation; the second emphasizes proof and logical justification. A complete mathematical environment should allow the two to cooperate.

For example, a symbolic system might propose an identity, while a proof assistant checks that identity under the appropriate assumptions. Conversely, a formally verified theorem might provide a justified fact that a computational system can reuse.

The important goal was not to make the systems identical. It was to connect their capabilities.

4.2 Combining computation, proofs, and readable mathematics

The workshop’s broader vision involved three interacting layers:

1. Human-readable mathematics: papers, definitions, explanations, notation, and mathematical intuition.
2. Computational mathematics: symbolic manipulation, algorithms, and numerical or exact calculations.
3. Formal mathematics: explicit logical statements and machine-checkable proofs.

The ideal system would preserve links among these layers. A statement in a readable mathematical paper would correspond to a structured representation, which in turn could connect to a formal proof or computational implementation.

The 2016 discussions treated this integration as a major opportunity, while recognizing that a fully unified system had not yet been realized.

image

fieldsinstitute.ca

+1

5. Designing the interaction between humans and computers

A mathematical language must be useful to mathematicians, not just convenient for machines.

The transcript describes a longstanding ambition: a person should be able to communicate a mathematical intention to a computer, have the system interpret it precisely, receive proof checking, and obtain assistance with some of the reasoning.

The difficulty is that mathematical practice relies on substantial shared context. Mathematicians routinely omit details they regard as obvious, use notation whose meaning depends on the subject, and move between intuition and formal argument.

A machine, however, cannot safely assume that every omitted condition is harmless.

5.1 From informal intention to formal statement

Suppose a mathematician writes:

Every continuous function on a compact interval attains a maximum.

A human reader may recognize the intended theorem immediately. A formal system needs more precise information:

• What is the domain?
• What is the codomain?
• What definition of continuity is being used?
• Is the interval closed and bounded?
• What does “attains a maximum” mean?
• Which mathematical structures and previously established results are available?

Once these details are represented explicitly, a proof assistant can check whether the conclusion follows from the premises.

The purpose of formalization is not necessarily to force the mathematician to write every detail manually. It is to ensure that the system ultimately has a sufficiently precise interpretation of the intended statement.

5.2 The need for readable formal languages

The transcript highlights a tension between machine precision and human readability. Some formal languages were designed primarily for verification, not for expressing mathematical statements in a style that resembles ordinary mathematical writing.

This distinction matters because a language that is technically expressive but unpleasant to read or write creates a barrier to adoption.

The workshop consequently treated the design of mathematical notation and the design of human-computer interaction as research problems in their own right.

A successful language would need to be both precise enough for computers and natural enough for mathematicians to work with.

6. Choosing a mathematical foundation

One of the deepest issues was deciding what kind of formal system should underlie the representation of mathematics.

A foundation determines the objects a system recognizes, the statements it permits, and the rules by which proofs are established. Choosing a foundation is therefore not merely a software engineering decision.

The workshop discussed several approaches, particularly set theory, type theory, dependent type theory, and homotopy type theory.

6.1 Set theory

In set-theoretic foundations, mathematical objects can be represented using sets and membership relations.

For example, the natural numbers, functions, groups, and topological spaces can all be constructed or encoded within a suitable set-theoretic framework.

The advantage is expressive power and a long history of use in mathematical foundations. The difficulty for a semantic language is that the internal representation may not correspond directly to how mathematicians naturally distinguish different kinds of objects.

A set representing a group and a set representing a topological space may both be sets, but the structures and operations associated with them differ.

6.2 Type theory

Type theory provides a different organizational principle. Rather than treating every object as an undifferentiated set, it distinguishes objects according to their types.

For example, a system can distinguish:

• Natural numbers from real numbers.
• Functions from numbers.
• Groups from their underlying elements.
• Propositions from proofs.

Types also help mathematical systems interpret notation according to context.

The symbol $+$, for example, may represent addition on natural numbers, addition on real numbers, or an operation on an algebraic structure. A typed system can use the types of the operands to help determine which operation is intended.

This makes type theory attractive for representing mathematics in a way that reflects mathematical practice.

6.3 Dependent type theory

Dependent type theory extends the idea of types by allowing types to depend on values.

This permits a single formal language to express objects, propositions, and proofs in a closely integrated way.

The Curry–Howard correspondence illustrates the connection between logic and type theory:

• Propositions correspond to types.
• Proofs correspond to terms inhabiting those types.
• Establishing a proposition amounts to constructing an appropriate proof term.

For example, if $P$ is a proposition, a proof of $P$ can be represented by a term whose type is $P$.

The practical significance is that mathematical statements and their proofs can be represented in one framework, with a type checker helping establish that a proof is well formed.

6.4 Homotopy type theory

Homotopy type theory (HoTT) was another important subject discussed at the workshop.

HoTT connects type theory with ideas from homotopy theory and algebraic topology. In this perspective, types can be interpreted as spaces, elements as points, and identity proofs as path-like structures.

One particularly significant idea is the univalence axiom, associated with Vladimir Voevodsky’s work. Roughly speaking, it connects equivalences between suitable types with equality between those types.

This is relevant to mathematical semantics because mathematicians frequently regard equivalent structures as interchangeable for particular purposes.

However, the foundational implications of this approach, its interpretation, and its suitability for different mathematical tasks were matters requiring careful consideration in 2016.

6.5 Why no single foundation was an easy answer

The problem was not that one foundation was obviously incapable of representing mathematics. The challenge was balancing expressive power, formal verification, computational behavior, readability, and compatibility with existing systems.

The workshop discussions explicitly identified the choice between set theory and type theory as a source of differing opinions. The associated white paper also cautioned against assuming that a new language should be designed before examining existing languages and library architectures.

image

The important lesson is that a global library needs to manage differences between foundations, not merely select a favorite and expect the entire mathematical community to adopt it.

7. Formalizing mathematical notation

Mathematical notation is extraordinarily powerful because it compresses complicated ideas into concise expressions. But this compression also creates ambiguity.

The workshop transcript emphasizes that notation is often unambiguous only within a particular mathematical context.

7.1 One symbol, multiple meanings

Consider the symbol $+$.

Depending on context, it may denote:

• Addition of natural numbers.
• Addition of real numbers.
• Addition in an abelian group.
• Addition of matrices.
• A more general operation defined on an algebraic structure.

Likewise, the expression $(1,2)$ could refer to an ordered pair, an open interval in the real line, or a vector, depending on the setting.

Human readers often infer the intended meaning from surrounding text. A computer must have a way to resolve that meaning explicitly.

7.2 Even the word “equation” can be ambiguous

The transcript highlights a more subtle issue: mathematicians do not always use the same terminology for different kinds of mathematical assertions.

Compare the following:

and

The first is commonly treated as an equation to solve. The second is a universally quantified assertion. The third is a numerical identity or equality without a free variable.

Different mathematical traditions may classify such expressions differently. Even a seemingly elementary term therefore requires a sufficiently precise definition if it is to serve as part of a universal semantic language.

7.3 Partial functions and undefined expressions

Another important issue is that mathematical functions are not always defined for every possible input.

Consider

As a real-valued function, this expression is undefined at $x=0$.

A formal system must determine how such expressions are represented, how undefined values propagate, and how assertions involving them are interpreted.

One possible approach is to require explicit domain conditions. Another is to use a formalism that permits partial functions or represents their definedness separately.

These decisions influence the meaning of mathematical statements and the behavior of symbolic computation.

7.4 The need for semantic preservation

Suppose an informal theorem is translated into a formal language. It is not enough for the resulting expression to look similar to the original.

The translation must preserve the intended mathematical content, including:

• The definitions of its symbols.
• The domain of its variables.
• Its quantifiers and assumptions.
• Its treatment of undefined expressions.
• The intended meaning of equality and other relations.

If these elements change silently, the formal statement may describe a different theorem.

The workshop therefore treated notation, semantics, and formalization as interconnected issues rather than separate problems.

image

8. What does it mean to preserve mathematical semantics?

The term semantics was used in several related senses during the workshop. One important distinction was between capturing the content of a mathematical publication and providing a fully formal interpretation of its statements.

These are different levels of representation.

A library might preserve a theorem exactly as it appeared in a paper, including its assumptions and notation. It might instead extract the definitions and theorem statements while leaving the proofs informal. A stronger representation might encode the statements and proofs in a formal logical system.

Each option serves a different purpose.

8.1 Three levels of mathematical representation

Level 1 — Document preservation

Preserve the original paper, notation, bibliography, and surrounding text. This protects the historical record but does not automatically make the mathematics machine-interpretable.

Level 2 — Semantic annotation

Identify definitions, mathematical expressions, theorem statements, assumptions, authors, dates, and relationships. This supports richer search and organization.

Level 3 — Formal verification

Encode the relevant mathematics in an explicit formal system and provide a proof that a proof checker can verify.

These levels are complementary. A formal proof does not replace the original paper’s historical context or explanatory value, while a scanned document alone cannot provide the guarantees of a machine-checked proof.

8.2 Should a library preserve incorrect results?

The transcript raises a subtle historical question: what if the original paper contains a mistake?

If the goal is to preserve the mathematical literature, the system should not silently replace the author’s statement with a corrected one. The original claim may still be historically important or contain useful ideas.

A careful library could preserve the original statement, record a formal interpretation separately, and annotate discrepancies or corrections.

This approach distinguishes historical fidelity from mathematical verification.

8.3 Why semantics is essential for correctness

A computer can only check a statement relative to the meanings and rules provided to it.

If a system reports that $2+2=5$, the immediate issue is not merely whether the answer is false. One must establish what the symbols denote and which operations and rules the system is using.

A formal semantic framework provides explicit definitions and inference rules, allowing correctness to be assessed meaningfully.

This was one of the transcript’s central arguments: formal verification depends on having a sufficiently precise account of what the mathematical expressions mean.

9. The structure of a theorem in a semantic library

The transcript discusses a proposed structure for representing the premises, conclusion, and metadata of a theorem.

This provides a practical way to connect mathematical meaning with information retrieval.

A theorem record could contain three principal components.

The premises must be ordered or otherwise linked so that dependencies can be resolved. For example, a definition may depend on an object introduced earlier.

The conclusion expresses the mathematical claim, while metadata helps users find, identify, and contextualize the result.

9.1 Example: The contracted Bianchi identity

The supplied transcript uses a theorem about the Einstein tensor as an example of structured mathematical representation.

In differential geometry and general relativity, the contracted Bianchi identity states that the divergence of the Einstein tensor vanishes, under the usual definitions and conventions.

A schematic representation might be:

Theorem record

Premises and declarations

• A smooth manifold $M$ of dimension $n$.
• A metric tensor $g$ and its associated connection.

• Definitions of the curvature tensor and Einstein tensor.

  Conclusion

Metadata

Theorem name, historical attribution, publication references, subject classification, and links to formal or computational representations.

The example demonstrates why a theorem cannot always be represented adequately by storing its final formula alone. The meaning of the formula depends on the objects, definitions, conventions, and assumptions associated with it.

The structured record is also more useful for search. A researcher could locate results involving the Einstein tensor, differential geometry, or a particular mathematical expression without relying solely on keyword matching.

10. Mathematical structures and their relationships

Algebraic structures were another important concern in the workshop.

Groups, rings, fields, vector spaces, and other structures organize mathematics by specifying objects together with operations and laws. They are central to the reuse of mathematical knowledge.

For example:

• Every abelian group is a group.
• The additive structure of a ring forms an abelian group.
• The integers form an ordered ring.
• Automorphisms of a suitable structure form a group under composition.

A semantic library should represent not only these structures individually but also the relationships between them.

10.1 Why structure reuse matters

Suppose a theorem has been proved for every group. If the system knows that a particular object is an abelian group, it should be able to use the general group theorem without requiring a second, independent proof.

This depends on representing the relationship between the two structures and making the theorem’s assumptions explicit.

Similarly, a generic theorem about rings may apply to the integers once the integers have been established as a ring.

Such reuse is fundamental to formalized mathematics because large proofs rely on extensive libraries of definitions and previously established results.

10.2 Mathematics is more than a hierarchy

A simple hierarchy might suggest that mathematical structures fit into a tree: groups contain abelian groups, rings have additive group structure, and so on.

But mathematical relationships are more complicated. A single object can carry multiple structures, and the same structure may be reached through different mathematical constructions.

The resulting knowledge representation is better understood as a graph with dependencies, shared definitions, and cycles of conceptual relationships where appropriate.

The workshop’s discussion therefore warned against treating mathematics as a flat list of definitions or a simple tree of classifications.

11. Concrete incompleteness and undecidability

The workshop also addressed foundational limitations on what formal mathematical systems can decide.

The distinction between proving a theorem and determining whether every statement in a given class can be decided is essential.

Gödel’s incompleteness theorems show that sufficiently expressive, consistent formal systems cannot settle every statement expressible within them, subject to the relevant technical conditions.

Undecidability results provide a related but distinct limitation: there are classes of problems for which no general algorithm can always produce a correct yes-or-no answer.

11.1 Why these limits matter for a mathematical library

A global library could help researchers identify known results, check formal proofs, and apply algorithms to new problems. But it should not be assumed that every mathematical question can be settled automatically.

For some problems, a system may find a proof. For others, it may fail to find one within available resources. In still other cases, a general decision procedure may be mathematically impossible.

A well-designed library must distinguish these situations rather than interpreting failure to prove a claim as evidence that the claim is false.

11.2 Why concrete examples matter

The transcript includes a discussion of the search for natural mathematical statements that are independent of particular axiomatic systems.

The concern was not merely to exhibit abstract statements of independence, but to find examples that mathematicians would recognize as meaningful mathematical problems.

This was presented as a difficult foundational research programme, not as a solved engineering task.

The broader lesson for formalization is that computers can clarify what follows from specified assumptions, but the boundaries of proof and decision must remain part of the mathematical picture.

12. Diagrammatic reasoning and mathematical meaning

Not all mathematical reasoning begins with a sequence of equations or a paragraph of text. Diagrams can carry mathematical content in their own right.

The workshop transcript discusses work in which geometric objects and their relationships are extracted from diagram images. Candidate conjectures can then be generated and checked or proved using automated reasoning techniques.

This suggests a possible pipeline:

1. Identify meaningful objects in a diagram.
2. Recover their geometric or structural relationships.
3. Generate candidate mathematical statements.
4. Check numerical or symbolic consequences.
5. Attempt to prove or disprove the resulting conjectures.

However, a diagram’s visual appearance does not necessarily encode every mathematical condition. A drawing may suggest that two lines are parallel or that three points are collinear without establishing those properties formally.

Consequently, diagrammatic reasoning requires a careful distinction between visual evidence and mathematical assumptions.

Category theory offers another important example: commutative diagrams express relationships among objects and morphisms. Their meaning is not reducible to their appearance on a page.

For a semantic library, diagrams should therefore be represented as mathematical structures whenever possible, rather than merely as images attached to documents.

13. The history of mathematical formalization

The 2016 discussions placed the project within a much longer history of attempts to make mathematical reasoning precise.

The development of rigorous analysis, the formalization of arithmetic, set theory, and the work of Frege, Russell, and Whitehead all contributed to the idea that mathematics could be expressed through explicit formal rules.

Later developments in interactive theorem proving made it possible for computers to check mathematical arguments in increasingly substantial ways.

The transcript also highlights the historical significance of Automath and the development of mathematical vernacular: approaches that explored how mathematical content could be represented more explicitly without requiring mathematicians to abandon their ordinary style of exposition.

This history reveals a recurring tension. Formal precision makes mathematical reasoning easier to inspect mechanically, but a formal language that departs too far from mathematical practice can be difficult for working mathematicians to adopt.

The challenge in 2016 was to benefit from decades of foundational and computational research while creating systems that were usable, extensible, and connected to the existing literature.

14. Digital mathematics and the scale of the problem

The scale of the proposed library was one of the reasons the workshop mattered.

The transcript cited estimates of approximately 100 million pages of mathematical research, accumulated across roughly four million papers and books, with around 100,000 new papers appearing annually. These figures were estimates used in the 2016 discussion, not a verified census of the literature.

The challenge was not simply to store this material. It was to convert a substantial portion of it into a form that could support meaningful mathematical operations.

14.1 Digitization versus mathematical understanding

Digitization involves making mathematical documents available in digital form. Optical character recognition (OCR) attempts to extract their text. Mathematical formula recognition goes further by identifying the structure of expressions.

Semantic processing must then determine what those expressions mean.

For example, recognizing the printed symbols in

does not establish what $f$ is, what its domain is, whether the integral exists, or which integration convention is intended.

Those questions require mathematical context and definitions.

A global library would therefore need several complementary technologies: document digitization, mathematical OCR, formula search, structured representations, formal reasoning, and links to computational systems.

The International Mathematical Union’s 2016 account similarly emphasized machine-processable mathematical knowledge, open representations, and links to existing computational resources.

image

Towards a Global Digital Mathematics Library

15. The global structure of the library

A global mathematical library would need an architecture that allows many contributors and systems to exchange knowledge without depending on a single monolithic repository.

A useful conceptual structure has several connected layers:

Original mathematical literature

Papers, books, lecture notes, historical sources

Semantic representation

Definitions, expressions, theorem statements, assumptions, metadata

Mathematical knowledge graph

Dependencies, equivalent results, structures, citations, provenance

Mathematical services

Search, computation, proof checking, visualization, education

Conceptual architecture synthesized from the workshop’s aims; this was not a finalized architecture agreed upon by the participants.

The original documents preserve the historical record. Semantic representations make mathematical content accessible to software. The knowledge graph connects related concepts, while mathematical services use those connections to answer questions and support research.

A distributed approach would also allow institutions and research communities to contribute material in interoperable formats. The IMU’s 2016 vision explicitly included a public mathematical knowledge commons and an international network of knowledge providers.

image

Towards a Global Digital Mathematics Library

16. Library use cases

The value of a semantic library becomes clearer when considered through practical applications.

16.1 Finding existing theorems

A researcher develops a new result and wants to know whether it has already been established.

Instead of searching only for matching phrases, the library could compare the mathematical content of the proposed theorem with existing results, including those expressed using different notation.

16.2 Finding useful assumptions and lemmas

A mathematician trying to prove a theorem may need an intermediate result but may not know its name or where it appears.

A semantic library could identify relevant lemmas, show their dependencies, and provide links to their original sources and formal proofs.

16.3 Discovering relationships across fields

A physicist might need mathematical tools for a problem without knowing which branch of mathematics is most relevant.

The library could reveal related results in several areas, helping the researcher explore connections that might otherwise remain hidden.

16.4 Supporting mathematical software

A computer algebra system could use structured mathematical definitions and established results to improve its symbolic operations.

A theorem prover could retrieve suitable lemmas from a library and use them in constructing formal proofs.

16.5 Preserving historical mathematics

A result that has become obscure may still contain an important idea. Semantic indexing could make it easier to discover and reuse such results, while retaining the original source and its historical context.

These use cases illustrate that the library was intended to support mathematical work, not merely to catalogue publications.

17. Formalization, education, and accessibility

A particularly important part of the workshop was the possibility of using formal mathematics to make mathematical exploration more accessible.

Traditional mathematical education often presents students with established facts, standard techniques, and exercises whose expected solution methods are already known. But research mathematics is exploratory: mathematicians formulate conjectures, test examples, discover patterns, and revise their understanding.

A well-designed mathematical environment could help expose this exploratory process.

17.1 Mathematics as experimentation

Suppose a student investigates the conjecture

is prime for every nonnegative integer $n$.

A computational environment could let the student evaluate the expression for many values, observe a pattern, and formulate a conjecture.

The next step would be to examine whether the conjecture is true in general. In this example, the expression produces primes for $n=0,\ldots,39$, but at $n=40$,

The conjecture is therefore false.

This example illustrates the distinction between experimental evidence and proof. Computation can expose patterns and counterexamples, while formal reasoning can establish claims under precise assumptions.

A mathematical library that combines computation, definitions, and proofs could support this kind of investigation.

17.2 Lowering barriers to entry

The transcript argues that mathematical reasoning should be made more accessible to people who are not professional mathematicians.

A system that provides definitions, examples, executable operations, and explicit rules could allow learners to explore mathematical ideas before mastering the full formal machinery.

The challenge would be to design interfaces that preserve correctness without overwhelming learners with technical detail.

17.3 Why adoption remained difficult

In the 2016 discussion, two obstacles were particularly prominent:

• Many mathematicians did not see enough immediate benefit in using formal methods for their ordinary work.
• Existing proof assistants demanded considerable effort and attention to detail.

These were not simply technical inconveniences. They affected whether people would participate in the collective effort to formalize mathematical knowledge.

18. Industrial applications and the need for verification

Formal mathematics also has practical value outside pure mathematics.

The transcript discusses work on verifying hardware, software, protocols, and floating-point arithmetic. Such applications depend on mathematical properties that may be difficult to establish reliably through testing alone.

Consider numerical computation. A program might implement an approximation to a mathematical function, but a reliable system may need guarantees about its error bounds, domain of validity, and behavior at exceptional inputs.

Formal methods can help establish such properties under explicit assumptions.

The transcript also points to major formalization efforts, including the Kepler conjecture project known as Flyspeck and substantial theorem libraries built with systems such as HOL Light.

These projects illustrated that computer-assisted verification could handle complex mathematics. They also demonstrated the importance of extensive background libraries: a major theorem depends on many definitions, elementary results, and supporting lemmas.

The industrial lesson was that verification is not an isolated activity. It requires a reusable mathematical foundation and an environment in which the relevant knowledge can be composed reliably.

19. The economics of formalization

One of the strongest arguments in the transcript concerns the incentives required to build a global mathematical library.

Formalizing an existing theorem can require considerable effort, even when its informal proof is already accepted. Yet the work may not produce a new mathematical result, and conventional academic reward systems may not recognize it in the same way as original research.

A mathematician may receive professional recognition for proving a new theorem, while formalizing an established theorem may be treated primarily as a computer science contribution.

This creates a mismatch between the collective benefit of a shared mathematical library and the individual incentives to contribute to it.

19.1 The cost of building a mathematical foundation

The transcript includes a historical estimate that formalizing undergraduate mathematics could require approximately 140 million person-years using the technology and assumptions considered at the time.

That figure was an illustrative estimate from the discussion, not an established measurement or a timeless prediction. It depended on assumptions about the amount of material, the time needed to formalize textbook pages, and the technology then available.

Its purpose was to communicate the scale of the effort required.

19.2 Why reusable libraries matter economically

Formalization becomes more efficient when definitions and theorems can be reused.

If every theorem requires reconstructing its entire mathematical background, the cost of formalization grows rapidly. A well-organized library distributes that cost across many projects.

The same applies to notation, interfaces, and proof automation. Improvements in foundational tools can benefit many later formalizations.

19.3 Possible institutional responses

The workshop’s concerns suggest several ways to support the project:

• Recognize high-quality formalization as a legitimate research contribution.
• Fund the construction and maintenance of shared mathematical libraries.
• Encourage collaboration between mathematicians and computer scientists.
• Support open, reusable mathematical representations.
• Develop tools that reduce the effort required to formalize existing results.

The IMU’s 2016 vision of an open mathematical knowledge commons also emphasized the importance of collective participation and non-proprietary, machine-readable representations.

image

Towards a Global Digital Mathematics Library

20. Translation between informal and formal mathematics

The transcript identifies two related but distinct translation problems.

The first is translating an informal mathematical statement into a formal proposition. The second is translating an intuitive proof into a sequence of formal logical steps.

These tasks should not be confused.

A theorem statement may be formalized correctly even when its proof has not been formalized. Conversely, a proof assistant can verify a formal proof only after the theorem and its surrounding definitions have been expressed in the system’s language.

20.1 Statement translation

The system must identify the mathematical objects, assumptions, quantifiers, and conclusion intended by the original text.

For example, the informal statement “every finite subgroup of the multiplicative group of a field is cyclic” requires a precise specification of the field, the subgroup, and the relevant group operation.

A formal statement must preserve these relationships.

20.2 Proof translation

Once the statement is formalized, the proof must be expressed using valid inference steps and previously established results.

A mathematician might write “without loss of generality” and immediately proceed to the next line. A formal system may need a detailed argument showing why the transformation preserves the generality of the theorem.

The transcript discusses the formalization of such reasoning patterns as an important achievement because they occur frequently in geometry and other branches of mathematics.

20.3 Why the two stages should be separated

A system that can formalize theorem statements is already useful for indexing and searching, even if it cannot automatically produce proofs.

Likewise, a formal specification can be useful in software verification even before a complete formal proof of every property is available.

This separation suggests a practical development strategy: begin by representing mathematical content accurately, then progressively add proof reconstruction, verification, and automation.

21. Existing achievements discussed in 2016

The workshop did not begin from nothing. Several areas of research had already demonstrated important parts of the broader vision.

Formalization of Partial Differential Equations using HOL Theorem Proving - Hardware Verification Group

HOL Light and formal theorem libraries

The transcript describes substantial libraries of formally proved mathematics, including proofs of major theorems and work on the Kepler conjecture. These demonstrated that machine-checked proofs could extend well beyond elementary examples.

Computer algebra

Systems such as Maple and Mathematica demonstrated the practical value of symbolic manipulation, equation solving, and computational mathematics. The challenge was to connect these capabilities more directly to formal reasoning and structured mathematical knowledge.

The Flyspeck project

The formal proof of the Kepler conjecture illustrated how large mathematical arguments could be supported by extensive libraries of machine-checked lemmas and definitions.

Paper page - Semantic Search over 9 Million Mathematical Theorems

Digital mathematical libraries

Existing efforts in mathematical knowledge management, mathematical document collections, and formula retrieval provided foundations for a more integrated library. The 2016 proposal aimed to connect these efforts rather than treat each as an isolated project.

The achievements were significant, but they did not yet amount to a universal semantic representation of mathematics.

22. Machine learning and automated theorem proving

The transcript also considers the role of machine learning in mathematical reasoning.

At the time, automated theorem proving already faced a practical problem: a formal library might contain an enormous number of lemmas, but only a small subset would be relevant to a particular proof.

Selecting useful facts was therefore a significant part of automated reasoning.

22.1 Learning which lemmas to use

Suppose a theorem prover must establish a proposition using a library containing thousands or millions of existing results.

Rather than giving the prover every lemma, a selection system could rank likely useful facts according to the goal, the current proof state, or patterns learned from earlier proofs.

The transcript discusses experiments using machine-learning-based lemma selection, including ranking approaches that improved automated theorem-proving performance in the evaluated settings.

This illustrates an important principle: machine learning can help navigate an existing body of formally represented mathematics even when it does not independently establish the correctness of a proof.

22.2 Discovery and verification are different tasks

A learning system might propose a theorem, suggest a useful lemma, or generate a candidate proof.

These outputs are not automatically mathematically correct.

A proof assistant can provide an independent verification stage, checking whether the proposed proof establishes the specified conclusion under the system’s rules.

The combination of learned search and formal verification was therefore a promising direction in 2016.

22.3 The longer-term ambition

The transcript imagines systems that could contribute to mathematical discovery, rather than merely check results already supplied by humans.

The aspiration was to expand the range of problems that could be explored, reduce the amount of detail that mathematicians needed to manage manually, and enable computers to help develop new mathematics.

But this remained a research ambition, not a claim that general automated mathematical discovery had already been achieved.

23. Formalizing Wolfram-style mathematics

One thread in the 2016 material concerned representing abstract mathematical concepts in a language designed to support computation, particularly work associated with Wolfram Research.

The challenge was to express pure mathematics in a computational environment without restricting the language to problems that could already be reduced to numerical calculation.

Abstract structures, function spaces, topological spaces, and general mathematical theorems require representations that preserve their mathematical meaning.

The December 2016 Wolfram discussion described experimental work on representing abstract concepts and theorems of general topology using the Wolfram Language. This was presented as a glimpse of the broader vision of computationally accessible pure mathematics.

image

The broader design question was whether a computational language could serve not only as a tool for calculations but also as a representation of mathematical objects and their relationships.

This was related to, but not identical with, the goal of formal proof verification. A computational representation may enable operations on an object, while a formal proof requires a logical account of why a proposition follows from its assumptions.

A successful global library would need to connect such approaches without confusing their different guarantees.

24. Proof visualization and the structure of mathematical knowledge

Formal proofs often contain far more explicit detail than their informal counterparts. As a result, a large proof library can be difficult to understand simply by reading its source code.

The transcript discusses visualizing proof dependencies, including a representation of the steps required to establish a basic arithmetic fact.

The point of such a visualization is not to make a proof look impressive. It is to expose the underlying structure:

• Which definitions are required?
• Which intermediate lemmas support the result?
• Which parts of the library are reused?
• How does the proof depend on foundational logical rules?
• Which components account for most of the proof’s complexity?

A large formal proof is therefore not merely a long text. It is a network of dependencies connecting the theorem to the foundational results on which it rests.

24.1 Why this matters for scaling

If a library contains many interdependent proofs, visualizations can help identify reusable components, central lemmas, and opportunities for simplification.

They can also help human contributors understand where their work fits within the larger body of formal mathematics.

In this sense, proof visualization is connected directly to the architecture of the global library.

25. Scaling the project: Modularization and community participation

No single researcher or institution could reasonably be expected to formalize the entire mathematical literature.

The workshop therefore considered the organizational problem of distributing work across many contributors.

A useful analogy is parallel computation. One hundred people cannot work efficiently if ninety-nine must wait for the first person to finish every prerequisite. They need ways to work on separate components, agree on interfaces, and combine their results.

25.1 Modular mathematical libraries

A modular library divides mathematical knowledge into components that can be developed and reused independently, subject to clearly specified dependencies.

For example, a team working on a new theorem in differential geometry should not need to reconstruct all of real analysis, linear algebra, and topology from scratch.

Instead, it should be able to import suitable formalized results and build upon them.

This requires stable interfaces, explicit assumptions, consistent definitions, and mechanisms for managing dependencies.

25.2 Avoiding isolated ecosystems

If different groups develop incompatible libraries without ways to exchange their results, much of the effort is duplicated.

Interoperability is therefore as important as individual formalization achievements.

The 2016 workshop’s discussions of modularity, language design, and library organization were all connected to this broader issue.

25.3 Community engagement

A shared mathematical library would need contributors from different countries, specialties, and institutions.

It would also need ways to recognize contributions, maintain quality, document provenance, and make participation worthwhile.

The International Mathematical Union’s 2016 discussion explicitly called for more international engagement and proposed a mathematical knowledge commons based on open, machine-readable representations.

image

Towards a Global Digital Mathematics Library

26. Future costs and the future of proof assistants

The workshop’s vision depended on improvements in the tools used to formalize mathematics.

The transcript discusses the hope that proof assistants would become sufficiently mature and practical to support a much larger formalization effort. It mentions Lean as a potentially promising system, particularly because of the possibility of bridging different traditions in interactive theorem proving.

This was a historical assessment made in 2016. It should not be confused with a claim that the workshop had already selected a universal proof assistant or established a final technical architecture.

The key requirement was a system that could support a large, reusable mathematical library while remaining sufficiently flexible for different branches of mathematics.

The economics of the project were equally important. The transcript’s estimates suggested that the work would require substantial resources, but the participants also emphasized that better tools and reusable foundations could reduce the cost of future formalization.

The central question was therefore not simply how many pages could be formalized. It was whether the necessary software, mathematical foundations, and community structures could be developed together.

27. The future of mathematics: From verification to invention

The broader vision discussed in 2016 was that computers would increasingly participate in mathematical reasoning.

This did not mean replacing mathematicians with machines. It meant extending what mathematicians could investigate by making more mathematical knowledge available for computation and formal reasoning.

The transcript connects this ambition with two longstanding aspects of mathematical work: discovering new results and determining whether proposed results are correct.

A future mathematical environment would ideally support both.

A researcher might explore examples, formulate a conjecture, search for related theorems, identify useful lemmas, and attempt a proof. A formal system could then verify the proof, while the library records the result and its dependencies for later reuse.

Machine learning could assist with conjecture generation, lemma selection, and proof search. Symbolic computation could simplify expressions or evaluate exact mathematical operations. Formal verification could provide guarantees about the correctness of accepted proofs.

The difficult part would be integrating these capabilities into a coherent environment that preserves mathematical meaning and remains useful to human researchers.

The workshop’s longer-term vision was thus not merely a library of completed knowledge. It was a computational environment for the ongoing development of mathematics.

28. What the 2016 workshop actually achieved

A historical account should distinguish the ambition of the workshop from its documented outcome.

The workshop successfully brought together specialists from different mathematical and computational communities, exposed important disagreements, and created opportunities for collaboration.

However, the subsequent workshop white paper explicitly records that the participants did not reach a consensus on a concrete semantic capture language or a directly actionable, agreed-upon set of design principles. The discussions revealed that even the meaning of semantic capture differed among participants. They also raised the possibility that building a library of mathematical content, together with tools to process it, might be a more productive first step than designing a new language in isolation.

image

This is an important result in its own right.

The workshop clarified the breadth of the problem, identified competing priorities, and made clear that a universal representation could not be designed simply by selecting a syntax or a logical foundation.

Its value lay partly in establishing a common research agenda and exposing the technical and organizational questions that needed to be addressed.

29. Conclusion: Toward a semantic language of mathematics

The 2016 workshop explored a profound possibility: that mathematical knowledge could become a shared computational resource, preserving the heritage of mathematics while making it easier to search, understand, verify, and extend.

Achieving this would require more than digitizing papers or creating a universal notation. It would require representations that preserve mathematical meaning, formal systems that support reliable verification, interfaces that respect the way mathematicians work, and a community willing to build and maintain reusable knowledge.

The major themes of the workshop can be summarized as follows:

• Semantics: mathematical expressions must have explicit, reliable meanings.
• Standardization: different systems need ways to exchange mathematical knowledge.
• Foundations: set theory, type theory, and other approaches present different advantages and trade-offs.
• Formalization: theorem statements and proofs must be translated carefully into machine-checkable forms.
• Computation: symbolic systems and theorem provers should complement one another.
• Organization: mathematical knowledge must be represented as a network of definitions, results, dependencies, and sources.
• Accessibility: the system must be useful to mathematicians, students, scientists, and other users of mathematics.
• Economics: sustained progress requires funding, reusable infrastructure, and incentives for contributors.
• Discovery: the long-term objective is to help computers participate in mathematical exploration, not merely archive completed results.

The central challenge was to make mathematics computationally accessible without losing the richness of mathematical practice.

The most important lesson from the workshop was that the future of digital mathematics depends as much on the organization and meaning of mathematical knowledge as on the power of the computers that process it.

Historical sources and further reading

The following sources document the workshop and its 2016 context.

Machine-Checked Proofs and the Rise of Formal Methods in Mathematics

1. Towards a Semantic Language of Mathematics

Wolfram · Published December 20, 2016

The documentary containing the interviews and discussion represented in the supplied transcript.

Watch the documentary

World Knowledge for Abstract Meaning Representation Parsing - ACL Anthology

2. White Paper of the Semantic Representation of Mathematical Knowledge Workshop

Wolfram Foundation · Workshop held February 3–5, 2016

The most important companion document for understanding the actual outcome, unresolved disagreements, and recommended directions.

Read the white paper

ACO Toronto - Fields Institute for Research in Mathematical Science (University of Toronto)

3. Semantic Representation of Mathematical Knowledge Workshop

Fields Institute · February 3–5, 2016

The official event page, with the schedule, speakers, and workshop context.

View the workshop page

4. Towards a Global Digital Mathematics Library

International Mathematical Union · May 2016

Explains the broader vision of open, machine-processable mathematical knowledge and the international infrastructure needed to support it.

Read the IMU account

The documentary is the primary source for the spoken viewpoints; the white paper is essential for distinguishing those viewpoints from the workshop’s final documented conclusions. Together, they provide a historically grounded picture of what researchers were trying to achieve in 2016, what they had already demonstrated, and what remained unresolved.