SAT and SMT
SMT-LIB coverage and speed
762 of 992 files decided
Limit: Coverage and speed differ by fragment
Read reportResults
Measured results by system
Each report states its benchmark or ledger population, source snapshot, and main limit. Keeping the reports separate prevents unlike proof routes and benchmark sets from being combined.
Engine
a103b3db3 Measured Source All site figures Computer algebra
CAS routes and checks
60 certificate-route facts
Limit: No general Mathematica or SymPy compatibility
Read reportProof checking
Lean and the Rust kernel
2,343 kernel-route facts
Limit: Selected Lean-core profile
Read reportFormal library
mathlib and the fact ledger
2,425 distinct propositions established
Limit: Far smaller than mathlib
Read reportIntegrated process
Producing and reusing a checked result
Axeyum has completed the full selection, production, checking, admission, and rescheduling process. Reusable autonomous production remains limited.
Recorded admission
accepted- Selected fact
- F:ml430-nat-fib-coprime-fib-succ-162fc738
- Direct dependencies
- 8
- Axiom footprint
- empty
- Newly ready
- F:ml430-nat-gcd-fib-add-self-5a92d5e3
- Source
- docs/autogenesis/76-exact-fibonacci-coprimality-admission.md @ a103b3db3