Mathematical work supported
Theorema supports definitions and axioms, computation, theorem proving, and the development of mathematical theories in notebooks. The same mathematical language expresses formulas and algorithms. Users choose the goal, available knowledge, prover, and enabled built-in operations. Proof presentation is part of the workflow. Theory exploration is an explicit project aim. Paper.
Architecture and trust
The implementation uses Wolfram Language and the Mathematica notebook interface. That does not mean Theorema expressions automatically inherit Mathematica semantics. Theorema 2.0 renames symbols in its expressions to prevent unintended evaluation by host operators. Its computational semantics uses selected built-ins, and the user can control which are active. Paper, §2.2.1.
The prover produces a structured proof object even for a partial attempt. The user interface distinguishes completed and incomplete attempts. User-selected knowledge and inference rules govern proof construction. In the reported Gröbner-basis development, specialized rules reduce long object-level derivations. The paper states that these provers are coded in Mathematica and their correctness is justified by handwritten arguments; they were not verified inside Theorema 2.0. Paper, §§2.1 and 6.2.
A separately documented LCF-like extension complicates any categorical claim that Theorema has no kernel architecture. The add-on page explicitly distinguishes add-ons from the official system. Its availability does not establish that every standard prover or built-in uses it. Add-ons.
Comparison with Axeyum
Theorema establishes a substantial precedent for integrating proof, computation, and theory development. Axeyum’s Rust solver/CAS/kernel components and explicit evidence routes differ from Theorema’s notebook and configurable prover environment. They do not establish that Axeyum invented integrated mathematical work.
The strongest technical comparison concerns acceptance contracts: which built-ins are active, what a produced proof object establishes, and whether it has been reconstructed in a smaller kernel. Theorema’s separation of its object language from host-language evaluation is particularly relevant to Axeyum’s translation boundaries. A source-system result must retain its intended semantics when used by another component.
Keeping an operation’s meaning explicit
Suppose a mathematical development introduces an operation written with a plus sign. A host algebra system may treat its own addition operator as associative and commutative. Those properties may be exactly what the development is trying to establish, or they may be false for the new operation.
Theorema’s expression separation prevents the host’s built-in interpretation from silently deciding that question. Selected definitions and rules supply the intended mathematical behavior. Computation can then use the operations whose semantics have been enabled. The paper discusses this problem directly when explaining the redesign of its language handling. Paper, §2.2.1.
That problem also occurs when two reasoning components exchange expressions. Matching notation or serialization is insufficient. They must agree on the mathematical operation and its assumptions. A successful source computation only supports a target theorem when the translation preserves the relevant meaning.
Lessons for a mathematical work environment
A complete example should retain the definitions, computational experiment, proposed theorem, and accepted proof. It should also show which earlier results were used. Theorema makes the user’s choice of available knowledge part of the interface. Axeyum can apply that lesson to the record of each automated attempt: the theory, active methods, and evidence policy should be recoverable.
OpenDreamKit studies related interoperability problems between mathematical systems. Axeyum’s constructive mathematics page gives concrete examples where different hypotheses and conclusions affect which result can be reused.
The Axeyum comparison refers to its documented source snapshot. Repository structure and paper descriptions were reviewed; no comparative benchmark was run.