Scientific computing / R&D
From mathematical theory to a verified numerical library in 9 months
Compensated-computation library: precision loss is visible and checkable, the model’s algebra is proved in Lean 4, each numeric claim has a reproducible benchmark.
- Status
- Research project
- Timeline
- 9 months
- Stack
- Python
- NumPy
- PyTorch
- Pydantic
- Lean 4 + Mathlib
- GitHub Actions
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 workarounds. We set out to build arithmetic where precision loss and singular cases are explicit, structured and checkable, 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 theorems in Lean 4 + Mathlib; the build confirms there are no gaps (sorry) and only Lean’s three standard axioms are used. The proofs cover the model’s algebra over the reals, not float64 behaviour.
- Enforced a claim-closure rule: every numeric claim in the docs is tied to a reproducible benchmark regenerated in the same change set. Losses are published next to wins: exact operations are slower than plain ones, and that is measured too.
- Shipped a public PyPI release (currently 1.1.0) under AGPL-3.0 or a commercial licence, with an automated package release pipeline. In the version under development, 870 tests pass (as of 05.10.2026); line coverage is 76%.
Outcome
- 1.0 instead of 0.0
- residual preserved on the [1e16, 1, −1e16] sum that float silently drops; reproducible benchmark generated by a script in the repository
- 6 of 6
- scenarios of the published benchmark in which the exact dot-product kernel matched the exact reference; numpy.dot matched in 0 of 6. The C kernel is not yet released on PyPI, and the cancellation scenario was built on purpose
- 0 gaps
- in the Lean 4 + Mathlib proofs of the model’s algebra (zero sorry), using only the three standard axioms; float64 behaviour is not formalised
- 9 months
- from first commit to the first stable PyPI release, per repository tags and commits (current version: 1.1.0)
Services
More cases
Manufacturing · Building materials
MVP in operationPanel specs from CAD drawings in seconds, not hours
Reads DWG/DXF layouts and builds the Excel spec: 10–30 seconds instead of 2–15 hours by hand. All 784 panels of one real project matched the manual spec line by line.
- 784/784 and 189/189
- panels on one project and wall panels on another matched the manual specs line by line, size groups included; area within 0.001 m²
- 2–15 h → 10–30 s
- to produce a project spec: manual work vs app processing, measured on real projects
Real estate · PropTech marketplace
MVP in operationLand-plot marketplace with a next-step plan: MVP in 2 months
From a mock-up to a working platform: plot → works → contractor → request. Rule-based next-step engine, three dashboards, personal-data compliance. MVP in 2 months.
- 2 months
- from approved spec to a pre-release MVP on an HTTPS stand: week 9 against the plan’s own 10–13 week estimate
- 7 days
- from spec to the first full-implementation commit: 168 files, 21.5k lines, then two months of hardening to pre-release
Marketplace e-commerce · Pricing
PilotRule-based repricing: a pilot whose contract terms are enforced in code
Competitor prices tracked per SKU, a price computed by rules inside an agreed corridor and applied only after confirmation. Pilot: 10 SKUs, setup within 14 days.
- 10 SKUs · 2 scenarios
- pilot scope; the SKU cap and both scenarios are enforced in code and verified by contract tests, so the cap cannot be exceeded
- up to 14 days
- contractual setup window from client inputs to launch, then a 1-month pilot; the service tracks the dates and closes access when the period ends
Estimate the payback of a similar process
AVA lets you work out the economics of your process on your own figures, with no form and no price from us. It shows what the manual work costs, what cash effect automation would give and what budget would pay back. If the effect does not even cover running costs, it says so.
Estimate the paybackDiscuss a similar problem
Describe the process and the data you have. Before any work starts we will tell you what can be measured in money, what cannot, and whether it is worth doing.