Version: v0.4.4
This repository contains the Axiom Forge framework as a public, reproducible artifact. It is intended as a portfolio-quality demonstration of an audit-grade, deterministic research governance system built with Lean 4 and mathlib.
It is not a research log and intentionally excludes exploratory mathematics.
Axiom Forge includes a deterministic workflow for testing published RH-equivalent statements by encoding reductions as explicit obligation checklists and capturing verifiable dashboard artifacts.
The Riemann Hypothesis appears in this repository only as a stress test.
This codebase:
- does NOT attempt to prove or disprove the Riemann Hypothesis
- does NOT claim progress toward the Clay Millennium Prize
- does NOT encode analytic number theory arguments
The RH demo exists solely to demonstrate that published RH-equivalent formulations can be decomposed into explicit, auditable obligation inventories under strict determinism.
Active RH research, if any, is conducted separately and is not part of this repository.
Demo goal (LOCKED):
The purpose of this demo is not to advance analytic number theory, but to demonstrate that
RH-equivalent formulations can be reduced to a finite, auditable set of typed analytic
obligations under strict determinism.
See:
docs/rh_testing.mdrh_testing/compilation/SUMMARY.md
- Framework core: stable
- Documentation: Phase 23 complete
- RH demo: structural and intentionally proof-free
- Public use: encouraged for governance and tooling experiments
- Active research: conducted outside this repository