# Axeyum > Axeyum is an integrated Rust system for solving, proving, and checking. It connects automated solvers, computer algebra, proof checking, and a formal library so accepted results can support later reasoning. Axeyum is implemented in Rust. It includes its own SAT solver, SMT solver, computer algebra system, proof kernel, and formal library. Z3, cvc5, Bitwuzla, Mathematica, SymPy, Lean, and mathlib appear here as technical reference points for comparison, tests, and selected import material; they are not Axeyum runtime components. Autogenesis selects an open statement, runs a proof producer, checks the result, records the accepted fact, and updates the dependency graph. The full process has run. Reusable autonomous production remains limited. Source: https://github.com/mjbommar/axeyum License: MIT or Apache-2.0 Distribution: source only Language: Rust; the default build has no C or C++ dependency ## Pages - [Vision](https://axeyum.com/vision) - [Learn](https://axeyum.com/learn) - [Concepts](https://axeyum.com/concepts) - [Components](https://axeyum.com/components) - [Problems](https://axeyum.com/problems) - [Results](https://axeyum.com/status) - [Artifacts](https://axeyum.com/artifacts) - [Reference](https://axeyum.com/reference) - [Research](https://axeyum.com/research) - [Publications](https://axeyum.com/publications) - [Search](https://axeyum.com/search) - [Get started](https://axeyum.com/start) ## Components - [Axeyum SAT Solver](https://axeyum.com/components/sat): A native CDCL solver with AIG and CNF lowering and certificate support. - [Axeyum SMT Solver](https://axeyum.com/components/smt): A typed SMT implementation with rewriting, theory solving, bit-blasting, models, and certificates. - [Axeyum CAS](https://axeyum.com/components/cas): A proof-carrying computer algebra system for exact symbolic operations. - [Axeyum Kernel](https://axeyum.com/components/kernel): An independent Rust checker for a selected Lean-core term language. - [Axeyum Library](https://axeyum.com/components/library): A dependency-aware library of checked facts with explicit evidence and assumptions. ## Lessons - [Lesson 1: How a rule becomes a checkable problem](https://axeyum.com/learn/claims-constraints-and-evidence): A reasoning system cannot check an intention. It needs a formal claim, the rules that give its symbols meaning, and a stated form of evidence. - [Lesson 2: From yes-or-no rules to Boolean formulas](https://axeyum.com/learn/boolean-logic): Boolean logic represents each basic statement as true or false, then combines those values with connectives whose meanings do not change from one problem to the next. - [Lesson 3: How a SAT solver searches](https://axeyum.com/learn/sat-solving): A modern Boolean satisfiability (SAT) solver propagates forced values, analyzes conflicts, learns clauses, and returns to the earliest choice responsible for a contradiction. - [Lesson 4: Adding arithmetic and machine values](https://axeyum.com/learn/smt-solving): Satisfiability modulo theories retains the meaning of operations such as addition and comparison while using Boolean search to coordinate the resulting constraints. - [Lesson 5: Expressions as mathematical objects](https://axeyum.com/learn/symbolic-computation): Symbolic computation preserves the structure of an expression. One exact transformation can then describe a whole family of numerical cases. - [Lesson 6: How Axeyum checks symbolic results](https://axeyum.com/learn/checked-computer-algebra): A computer algebra algorithm finds a result. An operation-specific checker tests the exact property claimed by that result, and selected results can also be reconstructed for the proof kernel. - [Lesson 7: Why a proof can be a term](https://axeyum.com/learn/formal-proofs-and-types): In dependent type theory, propositions can be types and proofs can be terms. Checking a proof becomes the precise task of checking that a term has its declared type. - [Lesson 8: What the Axeyum Kernel checks](https://axeyum.com/learn/proof-kernel): The Axeyum Kernel is an independent Rust checker for a selected Lean-core term language. It checks explicit declarations; it does not provide Lean's full interactive environment. - [Lesson 9: How a formal library reuses checked facts](https://axeyum.com/learn/formal-libraries): A formal library stores exact declarations and their dependencies. Axeyum's fact ledger also records evidence routes, provenance, status, and assumptions for results produced by several components. - [Lesson 10: Constructive and classical assumptions](https://axeyum.com/learn/constructive-and-classical): Constructive and classical foundations accept different general principles. Axeyum reports those assumptions per declaration instead of assigning one label to an entire library. - [Lesson 11: How the Axeyum components work together](https://axeyum.com/learn/integrated-reasoning): Axeyum gives each result a typed statement, an evidence route, and a place in the fact ledger. The components remain distinct because each kind of claim needs a different check. ## Field guides - [Number theory](https://axeyum.com/learn/fields/number-theory): Axeyum contains a substantial constructive development of elementary number theory over natural numbers and integers built inside its kernel. - [Constructive analysis](https://axeyum.com/learn/fields/constructive-analysis): Axeyum builds real numbers from regular rational sequences and carries explicit approximation data through its analysis library. - [Classical analysis](https://axeyum.com/learn/fields/classical-analysis): Axeyum provides a concrete place to compare classical existence theorems with constructive algorithms and explicit assumptions. - [Algebra](https://axeyum.com/learn/fields/algebra): Axeyum has a checked structure hierarchy and concrete algebraic instances, with quotient-based algebra as a clear next frontier. - [Geometry](https://axeyum.com/learn/fields/geometry): Axeyum has a substantial coordinate-geometry library over its constructed real numbers, with both kernel proofs and computer algebra certificates. - [Topology](https://axeyum.com/learn/fields/topology): Axeyum currently treats continuity and compact-interval arguments through explicit real analysis rather than through a general theory of spaces. - [Combinatorics](https://axeyum.com/learn/fields/combinatorics): Axeyum combines a constructive finite-carrier library with proof-producing search and certificate-producing symbolic computation. - [Probability and statistics](https://axeyum.com/learn/fields/probability-statistics): Axeyum now has a finite, rational-valued probability development with expectation, variance, covariance, concentration, and a weak law of large numbers. - [Category theory](https://axeyum.com/learn/fields/category-theory): Axeyum offers a clear experiment in adding abstraction above independently constructed carriers and measured trust boundaries. - [Logic and foundations](https://axeyum.com/learn/fields/logic-foundations): Axeyum's kernel, trust accounting, and constructive models make the foundations of each result available for direct inspection. - [Applied and computational reasoning](https://axeyum.com/learn/fields/applied-computational): Axeyum implements SAT, SMT, computer algebra, proof checking, and a fact ledger in one Rust system with explicit evidence between stages. - [Project evaluation](https://axeyum.com/learn/fields/project-evaluation): Axeyum publishes countable claims about proof status, trust, evidence routes, comparison coverage, and automated production. ## Problems - [An exact Mean Value Theorem witness](https://axeyum.com/problems/mean-value-theorem-cubic): For p(x) = x^3 on [0,3], find an interior point where the derivative equals the secant slope. - [Certified polynomial integration](https://axeyum.com/problems/certified-polynomial-integration): Compute an antiderivative of 3x^2 + 2x and check the result without trusting the integration procedure. - [Primality of 2^89 - 1](https://axeyum.com/problems/mersenne-89-primality): Can an independently checked certificate establish that the Mersenne number 2^89 - 1 is prime? - [Two four-color Rado numbers](https://axeyum.com/problems/four-color-rado-numbers): What are the four-color Rado numbers for 5(x-y) = 3z and 5(x-y) = 4z? - [Optimal sorting networks on three to six channels](https://axeyum.com/problems/optimal-sorting-networks): What is the minimum number of comparators needed to sort every Boolean input on three, four, five, or six channels? - [A BCNF decomposition counterexample](https://axeyum.com/problems/bcnf-decomposition): Can a BCNF decomposition preserve a lossless join while failing to preserve a functional dependency? - [The cause of an infeasible ICU roster](https://axeyum.com/problems/icu-roster-infeasibility): Which constraints make a 102-row ICU night roster infeasible? - [The cause of an impossible project deadline](https://axeyum.com/problems/project-deadline-infeasibility): Which constraints make a 60-row project schedule incompatible with its delivery deadline? ## Machine-readable indexes - [Complete site map](https://axeyum.com/sitemap-index.xml): every indexable page, including fact records. - [Artifact index](https://axeyum.com/artifacts): search and filter the fact ledger. - [Expanded guide](https://axeyum.com/llms-full.txt): the same route map with use and evidence notes. ## Autogenesis record - Admitted fact: F:ml430-nat-fib-coprime-fib-succ-162fc738 - Newly ready descendant: F:ml430-nat-gcd-fib-add-self-5a92d5e3 - Direct theorem dependencies: 8 - Transitive replay rows: 115 - Axiom footprint: empty - Source: docs/autogenesis/76-exact-fibonacci-coprimality-admission.md @ a103b3db3 ## Measurements All site figures use Axeyum commit a103b3db3, measured on 2026-09-03. - Fact ledger: 2714 facts checked; 2425 distinct propositions established; 262 open; 4 refuted. 2341 of 2343 kernel-route facts have an empty axiom footprint. Source: python3 scripts/validate-facts.py @ a103b3db3, 2026-09-03. - Regression scoreboard: 762 of 992 files decided across 24 logic fragments. 674 decisions were compared with z3 4.13.3, with 0 disagreements. Source: bench-results/SCOREBOARD.md @ a103b3db3. - QF_BV evidence run: 93 of 130 unsat results have an accepted certificate. 37 have no certificate from that run. Source: PARITY.md QF_BV evidence mode, c799be2f7, 2026-08-17. ## Parity ledger Each row uses 200 committed files, 24 seconds, and 8 GiB per file. - QF_SLIA: Axeyum 193/200; cvc5 1.3.4 193/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. - QF_BV: Axeyum 187/200; bitwuzla 0.9.1 194/200; 0 disagreements; Axeyum c799be2f7 on 2026-08-17. - UF: Axeyum 83/200; cvc5 1.3.4 93/200; 0 disagreements; Axeyum 9333f779d on 2026-08-21. - QF_LIA: Axeyum 113/200; cvc5 1.3.4 139/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. - QF_RDL: Axeyum 102/200; cvc5 1.3.4 148/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. - QF_LRA: Axeyum 88/200; cvc5 1.3.4 134/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. - QF_UFLIA: Axeyum 113/200; cvc5 1.3.4 180/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. - QF_IDL: Axeyum 66/200; cvc5 1.3.4 118/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. - QF_NIA: Axeyum 39/200; cvc5 1.3.4 83/200; 0 disagreements; Axeyum cb4a391c9 on 2026-08-21. ## Limits - Solver coverage and performance remain below mature solvers in several divisions. - The kernel implements a selected Lean-core profile. It has no general Lean elaborator or tactic environment. - The library is much smaller than mathlib. - Evidence claims are specific to their proof route.