From mathematical theory to a verified numerical library in 9 months

The task

Floating-point arithmetic loses information silently: summing [1e16, 1, −1e16] returns 0, meaningful differences collapse to false zeros, and division by zero throws instead of joining the data model. Pipelines patch this with scattered edge-case workarounds. We set out to build arithmetic where precision loss and singularities are explicit, structured, and auditable — with claimed properties proved and measured.

What we built

• Built a core based on Absolute Compensation Theory (ACT): every operation returns a result plus an explicit compensation term; singular cases become structured states with handling policies.
• Added compensated linear algebra (GEMM/QR/SVD), ML optimizers with a PyTorch wrapper, a finance ledger, and NumPy/pandas integrations on top of the core.
• Proved the public theorem surface in Lean 4 + Mathlib; the build certifies zero unproven statements and zero extra axioms.
• Enforced a claim-closure rule: every numeric claim in the docs is tied to a reproducible benchmark artifact regenerated in the same change set.
• Shipped a stable 1.0.0 release: 854 tests with an 85% coverage gate in CI, dual AGPL/commercial licensing, and an automated package release pipeline.

Outcome

1.0 instead of 0.0

residual preserved on the [1e16, 1, −1e16] aggregation that float silently drops; reproducible benchmark artifact in the repository

≥10x

stability ratio vs float64 on catastrophic cancellation; pinned baseline under regression control in CI

0 unproven statements

machine-checked proofs of arithmetic properties in Lean 4 + Mathlib (zero sorry placeholders); the build certifies no extra axioms

9 months

from first commit to stable 1.0.0 with 854 tests, an 85% coverage gate, and an automated package release pipeline

More cases