Reuse across theories
IMPS organizes mathematical work in small axiomatic theories connected by interpretations. Its logic supports partial functions and subtypes, so definedness and domain information participate in reasoning. A theorem is established in a home theory and can be used elsewhere through a suitable interpretation. Little Theories
This is direct prior work for the claim that a mathematical library can help determine the next reasoning step. Applicability is part of the system’s mathematical machinery. Axeyum should credit that history when describing its own plans.
An abstract result with concrete obligations
Consider a proposed Axeyum test involving an associative operation with an identity. A theorem about repeated use of that operation could apply to several concrete operations. Each application needs an assignment for the abstract operation and identity, together with evidence for the required laws.
A planner cannot infer validity from the resemblance between two formulas. It needs to know which hypotheses remain open. If a target operation fails the required law, the transport should fail even when the expression matcher succeeds.
For Axeyum, the useful artifact would contain the original theorem, the symbol assignments, and the evidence for the target conditions. That would let another task reuse an accepted interpretation rather than rediscover its obligations. This is a proposed test; it is not a claim that the current Axeyum selector implements general theorem transport.
A theorem can add a procedure
IMPS also connects installed theorems to procedures called macetes. They support organized theorem application, including use across theory boundaries. Its deduction graph records proof attempts and subgoals, while strategies act through the core inference machinery. IMPS system description
The architectural lesson is specific. Adding a theorem can change what operations the system can perform. That connection predates modern language models. An Axeyum method-learning experiment should therefore demonstrate what it adds to theorem-derived procedures: how the method is proposed, how its applications are checked, and how later tasks benefit.
The method’s usefulness and its mathematical acceptance are separate measurements. A valid application can be expensive. A heuristic can fail to find an application even when one exists. A failed search should remain a search result, not a mathematical obstruction.
Comparison with Axeyum
Axeyum’s current frontier implementation reads readiness and producer contracts from its mathematical records. The broader plan is to make those choices sensitive to the hypotheses, constructions, and evidence routes that a task permits. Pinned selector source
IMPS provides a reference for applicability and transport. Axeyum’s constructive statement families provide a distinct test population: approximate and exact conclusions, explicit quantitative hypotheses, and native or imported evidence. A useful evaluation would show which applications become possible after installing a checked mapping or method, and which remain rejected.
The compared foundations also differ. The IMPS library includes axiomatic real-number theories; Axeyum’s selected analysis results use constructed setoid reals. The actual statements and inference rules explain that difference; a raw axiom count does not rank reliability. IMPS library overview
The historical documentation remains accessible, including IMPS download instructions. This review did not test those instructions on a current machine. IMPS home page