Dirk Englund
Research Projects
Selected work on photonics, quantum systems, and AI-augmented science.
3DOptix AI Optimizer: Automated Optical System Design
AI-driven optical system optimization using 3DOptix ray tracing with Claude as the design agent. Iteratively optimizes mirror alignments, lens configurations, and beam paths.
NV Diamond Lean Tutorial: Formally Verified Quantum Sensing
Interactive tutorial formalizing NV-center diamond physics in Lean 4. Proves spin Hamiltonian properties, Zeeman splitting, and ODMR contrast using Mathlib.
VVUQ: Validation, Verification, and Uncertainty Quantification for AI Science
A visual language model platform that evaluates figure reproduction fidelity against reference papers. Enables rigorous VVUQ for AI-generated scientific content.
Fides: agentic paper reproduction
An AI lab that reproduces published papers from their own equations and data. It freezes verifiable numeric targets before any code exists, re-implements the method, runs physics checks (gates), and issues a verdict it cannot write by hand. An adversarial critic then reviews every run. Runs on our own fleet models (GLM-5.3-Flash, DeepSeek-V4.1-Flash).
Lean for Science
Formal verification meets interactive exploration
Diamond Quantum Sensing: Interactive Digital Twin
Interactive Marimo notebooks reproducing NV-center magnetometry experiments from first principles. Digital twin of diamond quantum sensing with live parameter exploration.
Nonlocally: Interactive Physics & Quantum Computing Notebooks (MIT)
Interactive Marimo notebooks for physics and quantum computing, hosted at MIT. Reactive Python environments for exploring quantum systems, photonics, and machine learning.
PhysLib: Formal Verification of Physics with Lean 4
Building a formally verified physics library in Lean 4. PhysLib connects 12K+ Mathlib declarations to physical concepts, enabling machine-checked proofs of scientific claims.
Technology Transition & Startups
Commercializing quantum photonics and AI