Projects

A collection of projects I've worked on, ranging from academic research to personal explorations. If you think it would be useful or interesting to collaborate on a project, please contact me to discuss.

Featured Projects

Generative AI and Stochastic Thermodynamics

- Present

A book with Max Welling and Lars Holdijk on the free-energy unification of generative AI and stochastic thermodynamics. Cambridge University Press, July 2026.

Generative AIStochastic thermodynamicsFree energy
Website

TNLean: tensor networks, formally verified

- Present

Formalizing tensor-network theory and quantum results in Lean 4 / Mathlib, with machine-checked proofs. Code releasing soon at sirui-lu.com/TNLean.

Lean 4MathlibTensor networksFormal methods

TeXRA: Multi-agent AI for theorists

- Present

Multi-agent AI research assistant (VS Code / Cursor / CLI) that grounds LLM reasoning in Wolfram algebra and Lean 4 formal proof.

LLM agentsTypeScriptLean 4WolframVS Code
Website

Other Projects

Agentic Publication Protocol

- Present

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. Releasing soon.

ProtocolAI agentsReproducibility

Lean-verified quantum error-correcting codes

- Present

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.

Lean 4Quantum error correctionFormal methods
Code

GitHub Activity

My GitHub ↗ contributions over the past year. Colored squares represent days with commits.

GitHub contribution chart