Current

Zero-knowledge proofs for cryptographic verification of claims about LLM training, inference, and deployment, as a MARS V fellow with the Cambridge AI Safety Hub, mentored by James Petrie (FLI). The profiler, calibration suite, and corrected traffic model are merged upstream; current work is the multi-GPU prover — a stage-aware weight-split model, a verifier-transparent weight split of the enrolled block, and streamed worker openings — on both the mathematics and the engineering. The linked case study is an informal account of the work so far; the technical write-up is expected Q4 2026, for review and publication.

Routing proof goals out of Lean 4 and Rocq to untrusted external provers — SMT solvers, ATPs, LLMs — grading and checking what returns, and closing the goal with a proof term the home kernel verifies for itself. R4 shipped 5 September 2026 — 19 of 19 targeted obligations close in an unmodified VerInf Lean file — and R5 consolidated the specification into v1.1 with an R-series roadmap. Next is finite-field certificates for VerInf's uniqueness queries, stronger certificate reconstruction, and Rocq parity.

Mathematics preprint proving a square-root cop bound for actual stopping-rule degree-reduction towers over bases satisfying fixed multistage expansion and accessibility hypotheses. Port placement and synchronized guarding remove the cloud-order factor. The follow-up gives an explicit whole-tower lower-transfer proof and an exact criterion for guarding adjacent-cloud unions. The remaining full-ball Hall requirement still blocks the proposed shrinking-base route to Meyniel's conjecture.

Mathematics preprint determining the bounded annealed critical window for growing-radius domination in random regular graphs — its universal scaling function and a scalar coupon-root asymptotic expansion. A bounded literature pass closed 5 September 2026, with the Duckworth–Mans attribution corrected and the relative overlap estimate completed. Typical existence in the growing-radius window remains open. A separate timed cloud-guarding paper now resolves the cloud-order loss in the conditional multistage pursuit transfer.

Mathematics preprint on path-tube persistence, exhaustive static coverage, conditional sampling thresholds, and information loss in d-regular tree-balls. Audit corrections landed 5 September 2026: the root-degree statement corrected, admissible-root coverage clarified with a counterexample to residual domination.

Reinforcement-learning agent under active development on top of arcana, a Rust rules engine built as the substrate for it; expected late 2026.

Compute is available at DTU for the duration of my enrollment; paused because it is not a current priority rather than for want of hardware.

Under review at JAMIA (Journal of the American Medical Informatics Association), after moving from JAMA Network Open. Calculator deployed at levineuwirth.github.io/icd_embeddings.

v1.1.0 shipped with prebuilt binaries; 4476 tests across 120 suites since. Rust core and embedded Lua VM, split into a long-lived instance and thin TUI and GPU frontends that attach over a typed protocol and edit CRDT-backed buffers concurrently. An audit on 5 September 2026 put it a few dozen small changes short of a daily driver on both frontends.

A Python-successor language designed adversarially: statically inferred without annotations, no GIL, no MRO. Spec, reference machine, language server, and debugger exist, .levo files run, and 1061 tests across 182 suites hold the line — but with no I/O and no standard library it is still a conformance machine, not a runtime.

Wayland-targeted productivity and research shell, in daily use as my main environment, with project resume as the hero verb. Recent work adds a reading-library surface — paper records filled from OpenAlex, PDFs opened in place — and a live window over the daemon's state.

FOSS music-notation platform: a deterministic, CRDT-based score model whose LaTeX specification suite is the source of truth. Spec and editor tracks advancing in parallel.