Roadmap
Direction of travel. This is intent, not a dated commitment — priorities follow real use.
Near term
- Promote alpha extensions toward beta as their CI suites and APIs settle —
starting with the most-used (
curvature,verify). - Broaden the certified surface: more enclosure recipes (PDE residuals, spectral gaps, reachable sets) with first-class certificates.
- Keras parity for more layers, keeping activation-level math bit-identical.
- More tutorials and cookbook recipes, especially proof-carrying workflows.
Later
- Deepen the formal loop: widen the class of finite obligations the
Mathlib-free Lean kernel checks, while keeping the infinite analytic
obligations honestly
sorry. - Richer multivariate-jet tooling for mixed high-order partials at scale.
- Documentation versioning snapshots cut alongside each release.
Explicit non-goals
What we will not do
- We will not rebrand non-closed-form methods (fractional, spectral) as closed form.
- We will not set
theorem_prover_verifiedwithout a genuine kernel pass. - We will not claim to solve the hard analytic problems whose obligations
remain
sorry. omnibias is proof-preparation infrastructure.
These non-goals are stable; they are part of what the project is. See scope boundaries.
Influencing the roadmap
The fastest way to move something up the list is a concrete use case with a minimal reproduction and the exactness category you need. Real workloads set priority.