Research
These programs describe methods, experiments, and open engineering questions. Concrete uses appear under Problems; bibliographic records appear under Publications.
Axeyum selects an open fact, gathers applicable facts and procedures, proposes evidence, checks the result, records its dependencies, and recomputes which facts are ready. The complete process has run, but repeated autonomous production remains limited.
Research recordThis work studies which SAT, SMT, and computer algebra results can carry evidence that a smaller or independent procedure can replay. Each route has its own evidence format and trust boundary.
Proof stackAxeyum develops arithmetic, algebra, analysis, and related definitions in a base whose kernel-checked declarations can have an empty axiom footprint. Classical imports are labeled separately.
Foundations comparisonThe fact graph records prerequisites and dependents. Research work uses that graph to select useful missing facts and to measure whether an admitted result makes later work available.
Dependency planThe Rules-as-Code Lab checks bounded consistency, coverage, thresholds, allocation, authorization, and workflow reachability in human-authored formal models. It does not perform automatic legal interpretation.
Rules-as-Code Lab