How mathematics changes representation

Formalization makes mathematical conventions into explicit interfaces. Before choosing proof syntax, one must choose what counts as a space, a function, an equality and an admissible assumption. Different provers can express much overlapping mathematics, yet those choices change the cost of a development and the shape of its reusable results.

Three foundational families

Set theory makes mathematical objects sets, with additional predicates and structure. Mizar’s MML uses Tarski–Grothendieck set theory, including a universe principle stronger than ordinary ZFC. Its soft types track predicates automatically, while structured articles retain a mathematical prose surface. The extra universe strength is a property of the library’s foundation; it need not be used by every individual theorem.¹²

Classical higher-order logic combines typed functions and quantification with classical reasoning. Isabelle/HOL, HOL Light and HOL4 use this family. A subset of a type can be represented by a predicate; structured objects can be described through records, classes and theories. Isabelle itself is a generic framework, and other Isabelle logics exist. Confusing the framework with HOL conceals a real foundational choice.³⁴⁵

Dependent type theory lets types depend on values and interprets proofs through typed terms. Lean and Rocq descend from the Calculus of Inductive Constructions; Agda comes from the Martin-Löf tradition. Arend uses a homotopy-type-theoretic system with an interval. These are related foundations, rather than interchangeable implementations of one logic.⁶⁷⁸⁹

In dependent foundations, universes stratify types to avoid treating one unrestricted collection of all types as an ordinary type of itself. In higher-order logic, polymorphic types provide another discipline. In set theory, size can be handled through sets and stronger universe axioms. These distinctions become practically important when a development quantifies over mathematical structures or categories. “Can formalize category theory” is therefore too coarse a comparison: ask which sizes, constructions and assumptions its particular library supports.

A mathematical object has several useful presentations

Consider a finite-dimensional vector space and a linear map $𝑇:𝑉\to 𝑊$. One development may work with abstract spaces and a bundled map containing its linearity proof. Another may choose bases and represent $𝑇$ as a matrix. The underlying mathematics relates the presentations, but a lemma about matrix multiplication does not immediately apply to an abstract operator. The library needs the connecting definitions and theorems.

The same issue appears in analysis. A function considered pointwise and an equivalence class of functions equal almost everywhere are different formal objects. The familiar practice of ignoring null sets must become a precise quotient construction or another explicit representation. One must also distinguish equality of functions, pointwise equality, and equality of classes.

From these examples I infer a useful selection rule: inspect the representations of your nearest existing theorem before judging a prover by its syntax. Two well-developed libraries can make different mathematical interfaces convenient. Moving a proof between them may require rebuilding those interfaces even when their foundations can express the same result.

Equality and univalence

In intensional type theory, definitional equality means that the checker treats expressions as the same through its computation rules. Propositional equality is an equality for which a proof is supplied. The distinction explains why a mathematically obvious rewrite can still require a lemma. It also explains why adding a computation rule differs from assuming a new proposition.

Lean’s ordinary mathematical practice uses proof-irrelevant propositions, quotients and classical axioms. Mathlib is broadly classical even though Lean can also express constructive arguments. An object obtained through classical choice may be mathematically useful while lacking an executable construction.¹⁰

Rocq supports several distinct foundational practices. MathComp’s odd-order development uses constructive reasoning with decidable finite structures and reflection. UniMath and the HoTT library develop univalent mathematics with their own conventions and accepted assumptions. Sharing a prover does not make these libraries freely interchangeable. This survey did not audit the current UniMath universe-checking configuration.¹¹¹²¹³

An identity type is a type whose elements witness an equality; its witnesses can themselves carry mathematical structure. An equivalence is an invertible map, with the inverse laws expressed through the theory’s notion of equality. For types $𝐴$ and $𝐵$ in a universe, univalence says that the canonical map from their identity type to their type of equivalences is itself an equivalence. It turns an equivalence into a usable identification of types. For structured objects such as groups, the corresponding treatment of structure requires further definitions and results. An arbitrary bijection between the underlying sets is not a group isomorphism.

Three implementations matter here:

1. Ordinary Agda can state univalence as an explicit hypothesis. TypeTopology does this in safe code. Such a theorem is conditional on that hypothesis; it does not derive univalence or obtain cubical computation by declaring the parameter.¹⁴
2. Cubical Agda supplies interval and path primitives, transport that moves elements along paths of types, and the Glue type that glues types along specified equivalences. Computational univalence is derived from these primitives. It supports higher inductive types: types declared with points and specified paths, and potentially higher paths. Computation still has precise limits; not every familiar equality becomes definitional.¹⁵
3. Arend has built-in univalence with some reduction rules. Its authors explicitly distinguish this from a fully computational theory: not every closed natural-number term reduces to a numeral. This failure of full canonicity is a computational limitation, not by itself a proof of inconsistency.¹⁶

Libraries embody mathematical histories

Lean / mathlib emphasizes a shared structure hierarchy and interdependent classical mathematics. The Liquid Tensor Experiment completed its specified central theorem in July 2022; sphere eversion follows from a formalized h-principle. These are substantial mathematics, with different scope and historical code versions.¹⁷¹⁸¹⁹

Rocq / MathComp grew through the four-color and odd-order projects. The odd-order formalization, completed in 2012 and published in 2013, built reusable finite-group, linear-algebra and Galois-theory infrastructure. Its method makes certified computation central to mathematical proof organization.²⁰

Isabelle/HOL / AFP combines distribution libraries with reviewed developments in a journal-like archive. The 2018 analytic prime-number theorem uses complex-analytic infrastructure and a Tauberian theorem. Locales let a theory state assumptions about a structure and derive results usable in later interpretations.²¹²²

Mizar / MML accumulates reviewed articles in a common set-theoretic environment. Its long history includes Hahn–Banach, the fundamental theorem of algebra and collaborative Jordan-curve work. Article preparation and library curation are part of its mathematical practice, not mere publication overhead.²³²⁴

Agda’s libraries cover distinct mathematical approaches. TypeTopology connects constructive mathematics with research on types and spaces. The cubical library formalizes cohomology rings and constructive schemes. The schemes paper uses univalent set-level mathematics and does not rely directly on the cubical interval; its location in a cubical library is not a description of every proof technique.²⁵²⁶²⁷

Arend / arend-lib includes constructive algebra and topology alongside synthetic homotopy theory. Isaev’s complete-spaces paper states that its results are formalized in Arend. The dated August 2026 release includes further algebraic-geometry and analysis developments. This establishes mathematical activity without supplying a cross-system adoption ranking.²⁸²⁹

HOL Light’s Flyspeck and HOL4′s analysis and probability libraries supply further established alternatives. Metamath’s proof language is foundation-independent; its principal set.mm database uses ZFC. Do not identify a proof language with the axioms of its best-known library.³⁰³¹³²

Formalization and mathematical explanation

An intermediate formal lemma can be weaker than a manuscript lemma and still suffice for a different route to the final theorem. It can also fail to suffice. The dependency structure decides; the checker does not compare itself with the manuscript. This is the key mathematical issue in the current Navier–Stokes translation discussion, examined in report 4.

Isar and Mizar can make the visible proof structure closer to a written argument. Dependent programming can expose constructions and invariants. Univalent foundations can change how equivalences are used. These affordances support explanation, but explanation still needs a reader who checks what the definitions and lemmas say.

Problem space

• Choose a representation: inspect a nearby formal theorem and its mathematical interfaces.
• Commit to a project: report 4 adds library-gap, maintenance and translation audits.
• Terminus: foundations alone do not select a prover; the next decision depends on the intended mathematics and collaborators.