A reasoning system that builds on its own work

We want Axeyum to coordinate mathematical work: identify what a task needs, choose an applicable method, check the result, and make it available to later tasks. The library should help decide what the system can do next.

Provenance records where a result came from and what it depends on. In this vision, that information guides execution. A task requiring an approximate root can use an approximation theorem. An exact root needs a different result, with its own hypotheses. A classical import is available only when the task permits its assumptions. Each choice must preserve the mathematical meaning of the original request.

This ambition has substantial predecessors. Ωmega coordinates proof plans and external reasoners. IMPS makes theorem reuse across theories an explicit operation. MMT represents theories and their mappings. Our mathematical systems guides explain these designs and the experiments they suggest for Axeyum.

A system that builds on its own work needs a clear basis for accepting each result. Axeyum's design separates the methods that search for an answer from the procedures that check its evidence. A new search method must still produce evidence those checks can accept.

That separation gives the system room to experiment. A language model can propose a proof step. An algebraic algorithm can suggest an identity. Each proposal faces the checking requirements for the claim it makes, and accepted results retain their assumptions when later work uses them.

Trust also depends on preserving the question. A checked proof establishes a formal statement. Connecting that statement to the intended mathematical problem requires explicit definitions and review of the translation. The complete workflow must account for both.

Lean combines computation and automated proof methods with a library of formal mathematics called mathlib. Lean's grind uses techniques from SMT solving and produces proofs. Isabelle's Sledgehammer and Lean-SMT connect external solvers to checked proofs.

Axeyum develops its own SAT and SMT solvers, symbolic algorithms, and proof kernel alongside its library and task-selection machinery. The goal is to let proof requirements guide the computational algorithms, and let missing library results guide which algorithms to build. A missing proof method can become a target for development; a checked method can become a tool for later attempts. That feedback is central to the design.

Consider a system of linear inequalities that cannot all hold. A solver can search for a weighted combination that exposes the contradiction. The weights form a Farkas certificate, which can be checked using exact arithmetic.

Axeyum can reconstruct supported certificates as formal proofs. It can also express the algebraic laws used by a proof as explicit hypotheses. The resulting theorem applies to structures satisfying those laws, rather than depending on a particular implementation of a number system.

The library supplies the definitions and proved laws needed to use that theorem. Search finds the certificate; reconstruction supplies the formal argument. The ordered-ring implementation shows how the solver and library can contribute to the same formal argument.

The method has close precedents, including mathlib's linarith.

The library's dependency graph records which results need which others. Combined with knowledge of the available methods, it can guide the search toward work that makes a larger goal reachable.

The intermediate value development combines repeated bisection, a decay bound, and a continuity bound. The extreme value development combines earlier laws about a supremum. Their dependencies form a directed acyclic graph: a proof rests on earlier results, with no circular chain of justification.

The research cycle repeats as that graph grows. A prerequisite can support several later results: the decay bound used by IVT also supports a geometric-series estimate. We want this feedback to guide the development of reusable methods as well as individual proofs. A procedure that produces checked results across a family of problems expands what the system can attempt. Its own development becomes part of the research process.

Large language models can propose a lemma, a supporting result used in a proof. They can also suggest how to split a difficult argument into smaller steps. Aristotle combines informal reasoning with Lean proof search and a geometry solver. DeepSeek-Prover uses subgoal decomposition. Formal proof search is also being applied to open research problems.

Other work explores different parts of the process. AlphaEvolve searches for programs and mathematical constructions using automated evaluators. LEGO-Prover builds a growing library of verified lemmas for later proofs.

Axeyum's goal is to give a model access to this whole cycle. It can propose a supporting result, choose a computational method, and use checked feedback to revise its next attempt. Accepted results enter the library, where later tasks can find them without reconstructing the argument from scratch.

The library and computational methods provide a persistent basis for improvement across attempts. The aim is for an agent to leave behind useful mathematics and procedures that another agent, or a human researcher, can inspect and build on.

Axeyum's constructed reals use Bishop-style setoids: rational approximation sequences equipped with a defined equivalence relation. The library proves that its operations respect that relation and carries explicit accuracy data into the IVT and EVT developments.

The library records an axiom footprint: the axioms a checked declaration depends on. Some Axeyum declarations have an empty footprint. Their proofs still rely on the kernel's rules, and conditional theorems still have hypotheses.

Classical results remain useful, and Lean can inspect axiom dependencies too. The useful comparison is between specific statements. A proof about Axeyum's constructed real numbers does not automatically prove the corresponding theorem about mathlib's reals. Connecting them requires a justified translation of the definitions and hypotheses.

Success means that accepted knowledge helps the system solve further problems and develop better methods for solving them. A growing library matters through the work it makes possible. The long-term objective is a system that can sustain this process, with people guiding its mathematical aims and examining the results.

We also want developers to keep executable code connected to the mathematics that supports it. The system should supply reusable translations between program values, solver terms, and checked statements, so each application does not need to rebuild those connections. The software verification guide examines this goal alongside Verus, SAW, and other existing systems. AI-generated changes would face the same obligations, with the original contract and its evidence retained.