I build agent harnesses for theoretical research, using symbolic computation and Lean proofs to check agents’ work. Physics PhD candidate at MPQ / TU Munich, advised by J. Ignacio Cirac.
Looking for research scientist / research engineer roles in reasoning, agents, and AI for science. Email me.
- TeXRA: I designed and built a multi-agent harness with Wolfram algebra and Lean proof checking. TypeScript; editor extensions and CLI; specialist agents for derivation, computation, and review.
- FormalFlow / MIPStarRE: with collaborators, formalized quantum soundness of the classical low individual-degree test, a core theorem underlying MIP* = RE. 63-day proof effort; 126,367 lines of Lean in the later study snapshot. Paper
- Quantum-code discovery: co-designed 14,116 Lean-certified quantum error-correcting codes using agents, symbolic computation, and search. Paper
- TNLean / QICLean: tensor-network and quantum-information theory in Lean 4/Mathlib, including the fundamental theorem of matrix-product states. Paper
- Agentic Publication Protocol: papers packaged with code, data, and instructions for research agents. With Xiao-Liang Qi.
I study quantum cooling, finite-energy quantum simulation, and neural and tensor-network representations.
With Max Welling and Lars Holdijk, I co-authored Generative AI and Stochastic Thermodynamics: A Tale of Free Energies (Cambridge University Press, 2026).