Agent harnesses, formal proofs, and physics-inspired AI. Research projects that connect theoretical ideas to computation, verification, and discovery.
01 / Agent harness for theoretical research
A multi-agent harness for theoretical research that connects language models to Wolfram algebra and Lean 4 formal proof, with computation and verification feeding back into the research process.
02 / Machine-checked many-body mathematics
Multi-agent autoformalization of tensor-network theory in Lean 4 / Mathlib: the fundamental theorem of matrix-product states, machine-checked.
03 / AI discovery with formal certificates
A multi-agent search plus a Lean 4 library certifying Knill-Laflamme constraints for exact nonadditive quantum codes, with a distance-2 catalogue and BD16 distance-3 examples.
04 / Physics for generative AI
A book with Max Welling and Lars Holdijk on the free-energy unification of generative AI and stochastic thermodynamics. Cambridge University Press, July 2026.
05 / Agent-readable scientific publishing
An open protocol for publishing papers as AI agents: bundle a paper with code, data, and an AGENTS.md so any agent can explain it, reproduce results, and support follow-up. Preprint out now.
My GitHub ↗ contributions over the past year. Colored squares represent days with commits.