Krishi Attri

Aligning independently captured 3D Gaussian-Splatting scans usually means falling back to point-cloud registration that throws away the splat structure. splatreg registers natively on the Gaussian representation (a Gaussian-SDF residual with a closed-form Jacobian over SE(3)/Sim(3)), then merges, or aligns without merging: the CLI bakes the recovered pose into the source so both scans stay separate PLYs in one frame. Baked-in transforms rotate the higher-order spherical-harmonic colour with the splat (real-basis Wigner-D); photometric refinement with exposure compensation handles the poses geometry cannot see; every builtin solve reports pose covariance for pose-graph weighting, never faked. The MAC maximal-clique seed handles contaminated correspondence sets, with the honest measured verdict kept: a wash on the official 3DMatch split, a decisive win on structured decoys.

official 3DMatch registration recall, 1279 pairs

91.5%

SH Wigner-rotation error vs an independent evaluator

2.4e-15

splat-merge Chamfer vs naïve concat

10.3 → 2.0 mm

photometric refine where geometry under-constrains

5° → 0.36°

Language models hallucinate theorems, and prose is not verification. mathlas is an MCP server of 12 deterministic, data-returning tools an AI agent drives: search over a 3.68M-document index (dense + BM25 + rank fusion), PSLQ constant identification, OEIS sequence lookup, and real Lean-kernel checks that now verify full proofs, returning the kernel's error verbatim so the agent can repair and re-call. A quantized laptop tier serves the same index from 1.9 GB at 2.4 s/query on 4 CPU threads, measured recall-lossless. The discipline is airtight-or-nothing: every verification tier returns an independently checkable fact or an honest nothing, with zero false positives measured across all tiers.

the same agent on 18 math tasks, with vs without mathlas

18/18 vs 15/18

Hit@20 vs TheoremSearch, on its own 110 human queries

59.1 vs 45.0

documents indexed; 1.9 GB quantized tier, recall-lossless

3.68M

A robot replanning through a world whose costs drift never knows how good its current route is once the map goes stale; classical planners silently trust the stale map. CERT-FLOW answers with a proof every round: a high-probability certificate LB ≤ OPT ≤ UB on the optimal route cost, built from age-weighted non-exchangeable conformal prediction over drift-adjusted residuals, and it spends paid sensing exactly where the certificate says the gap shrinks fastest. When the certificate proves the map tight, that proof licenses ns-to-µs preprocessed queries that self-expire the instant drift exceeds tolerance. Seven theorems (coverage through an impossibility result on lower bounds), validated on 17 synthetic regimes, game maps, and real traffic (METR-LA, PEMS-BAY); the failed hypotheses stay documented in the record.

coverage on every condition ever run; classical replanning 0.02 – 0.59

0.95 – 1.00

certificate-gated static cost query; 3.7 ms p50 full certified round, one CPU core

269 ns

lower sensing regret than freshness, uncertainty, or random at equal budget

2 – 3×

Feature caches skip the network on most denoising steps and forecast the cached features instead. HiCache++ ships the exponential (Dynamic Mode Decomposition / Prony) basis, exact on the local feature-ODE class where polynomial bases (TaylorSeer, Hermite) diverge, and the honest finding the benchmarks forced: no single forecast basis wins across diffusion families. The exponential basis wins on flow-matching 3D generators; polynomials hold DiT-class denoising. So the product is the selector: backend auto backcasts a held-out snapshot with both bases at every compute step and serves whichever demonstrably wins, at zero extra model calls. Deployed through per-model adapters across TRELLIS, Hunyuan3D, and SAM 3D, plus three ComfyUI nodes (Hunyuan3D, TRELLIS, TRELLIS.2; beta, Comfy Registry submission held until GPU validation).

F-score at skip-interval 5, exponential vs polynomial arm, Hunyuan3D-2.1

0.860 vs 0.735

geometry-lossless (F1 = 1.000) through interval 6, SAM 3D Objects

1.56×

holdout auto detects basis misfit and serves the winning arm

120/120