Theorem reuse
IMPS and little theories
Theorem transport, applicability, and reusable proof procedures in an interactive system.
Reviewed 2026-09-07
Mathematical systems
Systems for doing mathematics
Mathematical software can organize theories, coordinate computation and proof, or learn from earlier work. These guides explain established systems on their own terms and compare their designs with Axeyum.
An operating system for mathematics
The phrase describes an ambition with a history. PlanetMath used it for collaborative mathematical knowledge. Other projects built theory networks, proof planners, and interfaces between mathematical programs. The useful comparison is which responsibilities each system takes on and what evidence supports its results.
In Axeyum's research vision, mathematical applicability and evidence guide the choice of work. A root approximation, an exact algebraic value, and a classical existence proof serve different tasks. The constructive library examples show those distinctions; the systems below supply precedents and design lessons.
Lifelong learning
LeanAgent
A growing Lean database and a retriever that learns across mathematical repositories.
Reviewed 2026-09-07
Mathematical data and provenance
MathDataHub and mathematical data schemas
Mathematical types and database encodings are different. MathDataHub studies how schemas can connect them and generate useful interfaces.
Reviewed 2026-09-07
Theory organization
MMT, OMDoc, and MathHub
Mathematical theories, mappings between foundations, and shared library services.
Reviewed 2026-09-07
Semantic interoperability
OpenDreamKit and Math-in-the-Middle
Semantic interfaces for computation across mathematical software systems.
Reviewed 2026-09-07
Collaborative mathematical knowledge
PlanetMath and Planetary
A precedent for organizing collaborative mathematical knowledge as an extensible system of documents and services.
Reviewed 2026-09-07
Software verification
Software verification, Rust, and AI
Keeping executable code, mathematical specifications, and checked evidence connected.
Reviewed 2026-09-07
Theory development
Theorema
A mathematical notebook environment for computation, proof, and theory development.
Reviewed 2026-09-07
Proof planning
Ωmega
Proof planning, external reasoners, and retained proof expansions.
Reviewed 2026-09-07
How to read the comparisons
Knowledge representation, proof validation, and planning are separate responsibilities. A semantic alignment between systems does not automatically establish a sound proof translation. A provenance record does not itself check a result. A planner's proposed method still needs an accepted proof or an explicitly identified computation route.
Each guide links primary papers or project documentation and separates the reported implementation from proposals. These are architectural comparisons, not head-to-head performance benchmarks. Historical systems can supply useful designs even when their original software has not been replayed here.