Ongoing Research

The Bayesian World

Actively under development: this describes the system as currently implemented, and much of it is still changing.

• Scanner orbit demo
• Parameter fitting demo (simulated data)

What the system is

The Bayesian World is a Python package, with a Lean project alongside it, for working with physical devices as mathematical objects. A catalog holds parts, reusable models and interfaces. An assembly file (a "contraption") combines these with wiring, controllers, placement and verification claims, and the loader resolves it into one hash-identified system. Simulation, fitting, observers, the C99 and Verilog generators, and the Lean translator all consume that same object.

My goal is an agent that designs a device, simulates and proves properties of it, and improves its models from real experiments. What exists today is the foundation for that, not the loop itself. This page describes the code as of October 2026.

The PMDL-2 language

PMDL-2, the second version of my physical-model language, is a closed JSON format. A model denotes an explicit ordinary differential equation (ODE) system: dx_i/dt = F_i(t, x, u, p) and y_j = G_j(t, x, u, p), where F_i and G_j are the model's expressions, t is time, x are the states, u are external inputs, p are parameters fixed for one trajectory, and y are outputs such as sensor readings. Its main rules are:

• The semantics are mathematical. A model means what its equations mean over the real numbers; a solver only approximates that.
• Numbers and units are exact. Every constant is a reduced rational, and floating-point literals are invalid. Units are exact, and no conversion is ever inserted implicitly.
• There are no escape hatches. Expressions form a closed, typed syntax tree with no embedded code or callbacks.
• Partial operations must state their domain. Each division, root or logarithm names a condition. If the condition is false, the model is inapplicable; it does not produce a not-a-number value.
• Each state has exactly one derivative. Mode switching and implicit equations belong to separate, explicitly selected extension formats.
• Unsupported input is rejected. Unit mismatches, stale hashes and algebraic loops all cause errors.

As a small real example, the reference integrator model declares one dimensionless state x and one input rate, and its entire law is this entry:

{"state": "x", "expression": {"kind": "symbol", "name": "rate"}}

That is, dx/dt = rate.

Lean conversion and proof checking

The translator takes the exact resolved ODE model, re-checks its SHA-256 hash, and emits Lean definitions over the real numbers for its equations, domains and declared claims, plus classified proof obligations. Separately written Lean proofs are then admitted through a gate, pinned to Lean and Mathlib 4.33.1, which:

• rejects proof escapes such as sorry, user axioms and unsafe definitions;
• checks that the theorem has exactly the generated claim's type;
• requires that the proof adds no axioms beyond the three that the real-number statement already depends on (propext, Classical.choice, Quot.sound);
• requires a companion certificate, with no axioms at all, tying the proof to the model, claim and source hashes.

Five small examples currently pass this gate; I re-ran it on 30 October 2026. Two claims follow from the base equations and bounds: an inductor energy bound and a passive optical attenuation bound. Three (an RC circuit, a DC motor, and a planar body) depend on invariants or contracts declared by the model's author, and record that dependency.

The limits matter more than the mechanism. All five are conditional theorems of the form "any trajectory satisfying this model also satisfies this property." In all five, existence of a solution is an open obligation and uniqueness is not claimed. So the theorems could in principle be vacuous, and the tool reports them as semantically incomplete. Models with mode switching or implicit equations are refused. Proofs about ideal real-number models say nothing about rounding in generated code, and no composition theorem covers a whole contraption. A proof is relative to the declared model; it does not show that the model describes a real device. The proofs are written separately; the system does not generate them.

Composition, simulation and fidelity

Assembly connects output ports to input ports only when units, domains and port kinds match exactly. A cycle of purely instantaneous connections is rejected as an algebraic loop rather than solved implicitly.

The simulator compiles the resolved model with JAX in 64-bit floating point. It supports fixed-step and adaptive integrators and exposes derivatives with respect to state, inputs and parameters. Generated C99 and Verilog are tested with external toolchains, though full-scanner hardware synthesis did not finish in bounded local runs.

Mechanics has two fidelity levels for each of four domains: gravity, rigid-body motion, friction and elasticity. The "ODE" level uses lightweight approximations such as small-slope gravity; the "refined" level uses finite-slope gravity and a bristle-type contact model with a viscoelastic tread. Friction and elasticity share a contact state and must match, which gives eight allowed combinations. Collision discovery and impact laws are not implemented; contacts must be declared in advance.

The agentic part importer

The importer turns a source file from an open catalog, such as a KiCad symbol or a FreeCAD part, into catalog entries using language models. Deterministic code owns provenance, license checks, paths and hashes. The models make the physical judgments: whether the part is in scope, what equations describe it, and what its parameters and uncertainties are. Output must pass validators and full compilation, with bounded retries, and then a model-based physical review.

The main branch contains an earlier version of this pipeline. The results below come from a newer staged pipeline on a development branch, which is explicitly experimental and not merged.

Current throughput

The importer does not yet work at a useful scale. The early successes were narrow: in August 2026, 20 of 20 parts were imported for about $0.08 in total, but all were resistors and thermistors, and that figure excludes about $0.04 of development runs just before it. A 24-part evaluation with diverse parts on the older pipeline had produced no passing campaign, after repeated attempts, as of my last written audit of that pipeline, around the start of September.

In October I measured the staged pipeline with an audit outside the pipeline, which compared accepted candidates with their original sources. "Eligible" excludes parts whose main function is outside the supported physics. The table shows the main batches, not every run. Charges are figures from my own spending ledger, mostly estimated from provider token counts rather than checked against invoices.

Among these batches, my target of at least one third useful acceptance was reached only on the 3 October development sample, and that run still failed other gates. Runs outside the table vary widely on small or repeated sets: an earlier run of the fixed 64-part KiCad set passed 8 of 61, with one accepted part contradicted by manufacturer data, and a rerun of the 32 KiCad parts passed none of 31. On the most recent fully audited fresh sample the yield was one part, a transistor, with a source-weighted point estimate of 5.4% over a frame of 25,763 source items. That is one sample, not a population measurement. The 4 October fresh sample's four successes were all bounded axial mechanical parts reusing an existing engine, with no newly created model passing. The review stage is not yet reliable either: of the 10 parts accepted in the 4 October KiCad run, the audit found three with inaccurate laws and one missing its primary function.

In the table, cost per audited success ranged from about $0.20 to about $3. Elapsed time between the first and last charge ranged from about 30 minutes to about four hours per batch. That depends on concurrency and interruptions, so it is not a per-part rate. Total recorded provider charges since August, including failed experiments, are about $123.

In the 6 October sample, most failures were at pipeline stages (19), scope classification (5), or before any model call (5), and 33 of 144 charged calls returned invalid output.

The evidence has gaps: a 48-part follow-up on 6 October was interrupted early with no result, another 32-part run that day has no completed audit, and a small repair tried afterward produced no acceptance. The ledger shows no paid importer runs since then. None of the October accepted parts has been promoted into the main catalog, which still holds 27 physical part records. A person still authorizes spending and promotion, resolves interfaces the agent reports as blocking, and decides what to do when audit and pipeline disagree. Passing the audit means a bounded model is consistent with source documents, not that it matches a measured part.

Simulation fitting

The fitter estimates a chosen vector of uncertain model parameters θ from observed output traces, using the same compiled simulator. Each candidate is scored on the complete dataset through standardized residuals r = (y − g(θ)) / σ, where y is a measurement, g(θ) is the simulated output and σ is that channel's declared noise scale. Observation noise is assumed to be independent and Gaussian.

1. Exploration. By default, 2,048 deterministic low-discrepancy draws are taken from the normal prior truncated to the parameter bounds.
2. Local refinement. Several distinct best candidates are refined with forward sensitivities and bounded least-squares steps.
3. Convergence check. A fit must meet a numerical stopping certificate. Running out of iterations with a low residual does not count, and without a certificate the update fails.
4. Posterior. With prior mean m and diagonal covariance S, likelihood optimum θ̂, and exact likelihood Hessian H at θ̂, the posterior covariance is C = (S⁻¹ + H)⁻¹ and its mean is m + C H (θ̂ − m).

This is a local Gaussian (Laplace) approximation. It is not Markov chain Monte Carlo or sequential Monte Carlo sampling, and it does not represent a multimodal posterior. It does not establish that every mode was found, and it does not model discrepancy between model and reality, so a tightly concentrated posterior can still be wrong. Fitting currently runs only on CPU.

Evidence so far comes from simulated recovery. The demo's acceptance test requires the posterior mean to reduce absolute error against the known truth by at least 90% from the prior mean for every parameter, which is only possible on synthetic data. Small experiments for each mechanics domain at ODE fidelity serve as the release checks; refined-fidelity fitting is not part of that gate.

Known unresolved problem: a combined 14-parameter calibration of the scanner on uneven terrain has not met full-data fitting acceptance. I have set it aside as a research fixture, and it remains open.

The two demos

Scanner orbit. This is a recorded simulation of a small wheeled camera robot, based on the Pololu Romi platform, driving around a target for 43.5 simulated seconds with rendered camera views. The browser only replays saved frames; no physics runs in the browser. All five orbit criteria passed on this single trajectory, but the probabilistic requirement of 95% was not established by one sample, so the recorded verification reports "not accepted". Seven dynamics gates remain open, including payload inertia and caster contact. The recording dates from an earlier version of the code.

Parameter fitting from simulated data. This is a report from a run of the current JAX fitter, with synthetic noisy data and known truth. It recovers three parameters of a simulated wheeled chassis from 1,001 observations covering 0.5 simulated seconds, using automatic differentiation and a Bayesian (Laplace) update. The page replays the trajectories simulated with the true, prior and fitted parameters next to the noisy observations:

The run was computed offline under Python 3.11, the version the project's tests use. Under Python 3.12 the loader currently rejects this assembly because a sum of part masses differs in its last binary digit, a portability bug I still need to fix. In the top-down view the three trajectories nearly overlap; the differences show more clearly in the sensor-channel plots. The result shows recovery under the assumed model and says nothing about a real robot.

Validation status

Everything on this page is simulated, formally checked relative to a model, or checked against source documents. No result here uses measurements from physical hardware. Sensor noise figures in the demos are assumptions, and the scanner is a laboratory fixture with explicitly incomplete dynamics.

Actively under development

Parts of this project are currently broken or unmerged, as noted above. Open work includes raising importer yield and merging the staged pipeline; a searchable part registry; more physics, including collision; reusable contraption-level and existence proofs; repairing the current fitting demo; resolving the combined scanner calibration; and physical experiments that can update or reject a model. These are goals, not shipped features.

• Scanner orbit demo
• Parameter fitting demo (simulated data)

Part data sources

The scanner's part records are my own factual and model records, informed by the sources below. Vendor and product names only identify the parts being modeled, and don't imply affiliation or endorsement. The demos contain no vendor CAD, images, or logos.