Roadmap

LeanCert's current public claims are documented in the trust model and verification-status table. The items below are convergence work, not features claimed as complete.

Extensible checked enclosures

Current state: downstream modules can register and inspect typed unary ℝ → ℝ enclosure candidates, Boolean checkers, and sorry-free soundness theorems without modifying LeanCert's internal expression datatype. leancert executes imported rules for unary interval bounds, supports nested registered applications, and composes their checked results through ordinary core expressions. Rejected or comparison-inconclusive candidates are retried through checked rational subdivision with retained leaf provenance.

Possible next milestone: extend the protocol beyond enclosure rules only when downstream use cases establish a concrete need for additional rule kinds.

Evidence: an external function certified end to end through an imported rule, with rejected-candidate fallback and complete leancert? provenance.

Checked-backend capability parity

Current state: Rational, Dyadic, and Affine backends deliberately have different supported operations and performance profiles.

Milestone: publish a generated capability matrix and close high-value gaps without hiding backend selection or fallback.

Evidence: backend-specific correctness tests and checked public API examples for each newly supported operation.

Quantitative asymptotics

Current state: eventual_bound checks explicit positive cutoffs and can discover witnesses for existential natural-number upper bounds on nonnegative rational multiples of reciprocal powers. Discovery uses bounded exponential search and binary refinement, then replays the candidate through the same exact-rational checker. The Golden Theorem proves the infinite tail by symbolic monotonicity. The leancert router recognizes this theorem family, and reports preserve the cutoff and search provenance.

Possible next milestone: grow the typed tail-rule language from demonstrated downstream needs, starting with compositional domination rules or carefully scoped logarithmic and exponential tails.

Evidence: fixed-cutoff and discovered-cutoff regression theorems, exact and budget-limited search tests, rejected cutoff tests, semantic-router coverage, and eventual_bound?/leancert? provenance.

Nonlinear-system roots

Current state: system_unique_root generates rational Krawczyk centers and preconditioners for square systems in the checked-AD fragment. It uses singleton point-Jacobian enclosures, pivoted Gauss--Jordan inversion, bounded interval-Newton refinement, and fixed-precision candidate rounding. The semantic router invokes it directly for the canonical ∃! system goal. system_unique_root using cert remains the manual path. Both pass through krawczykCheck and verify_unique_system_root; search data is never trusted.

Possible next milestone: expose the checked system-root operation through the bridge and let external numerical frontends supply stronger candidates. Adaptive box refinement remains separate: it requires existence in one box and root exclusion over the complement to preserve uniqueness in the original box.

Evidence: automatic translated, coupled transcendental, cyclic 3D, generic 4D, and refinement-requiring exponential systems; exact and singular matrix inversion tests; mutation tests for every checker stage; dimension-limit, budget, unsupported-AD, conjunction-order, trust-route, and rollback tests.

Stronger quantified ML theorems

Current state: ML certificate components prove the precise structural and bound properties stated by their theorems; they are not a blanket end-to-end model-correctness claim.

Milestone: connect more model-level specifications to checked layer and quantized-inference bounds.

Evidence: exported quantified theorems over inputs, with explicit assumptions and trust-manifest entries.

Large integration certificates

Current state: exact polynomial integration and checked partition integration are available; large partition certificates can be expensive, especially under kernel-only checking.

Milestone: reduce certificate construction and verification cost while preserving the same Golden-Theorem boundary and explicit trust selection.

Evidence: versioned benchmark baselines with toolchain, machine, revision, and warm/cold metadata.

Downstream applications

Current state: LeanCert includes ANT, QProduct, certified-table, and ML infrastructure plus interface tests derived from downstream use.

Milestone: expand maintained applications while keeping the stable numerical API small and domain assumptions explicit.

Evidence: downstream interface contracts, compiled application examples, and published theorem statements rather than source-line counts.