arXiv:2610.17708 · Preprint · 2026
Quantum Hoare logic QHL+ in Lean 4: program semantics, sound proof rules and verified classical–quantum programs.
Formal MethodsQuantum ComputationProgram VerificationAutomated Theorem Proving
Collin Yuanjie Ren
PhD in Physics, MIT · September 2026
I completed my PhD in Physics at MIT in September 2026, under the supervision of Peter Shor and Aram Harrow. Previously, I earned my MA in Physics at Stony Brook University, where I was advised by Axel Drees.
My research focuses on quantum codes, topological order, and quantum simulation of physical systems. I'm also learning about open quantum systems, quantum complexity theory, as well as quantum algorithms.
In my free time, I think about and experiment with how machine learning can help derive and prove mathematical theorems (auto-formalization) and how large language models can facilitate the design of better video games.
Ideas & connections
Research
Across mathematics, formal methods and quantum computation.
All papers
12 papers
arXiv:2610.03920 · Preprint · 2026
Fault-tolerant measurements of logical Clifford operators in QLDPC codes, enabling magic-state preparation and non-Clifford operations.
Quantum ComputationQuantum Error Correction
arXiv:2609.09608, preprint (2026)
Convex-Gaussian decompositions of interacting fermionic Gibbs states, with perturbative bounds and applications to the Fermi–Hubbard model.
MathQuantum ComputationFermionic SystemsStatistical Mechanics
arXiv:2608.07360, preprint (2026)
An extremal bound on algebraic connectivity, with a MerLean-generated Lean 4 formalization checked by the Lean kernel.
MathFormal MethodsSpectral Graph TheoryAutomated Theorem ProvingAutoformalization
arXiv:2605.26959, preprint (2026)
A recursive planning and proof-generation harness that produces kernel-checkable Lean 4 proofs.
MathFormal MethodsAutomated Theorem Proving
arXiv:2605.21933, preprint (2026)
A mathematical framework relating learning dynamics, time-reversal asymmetry and stochastic-thermodynamic entropy production.
MathStatistical MechanicsMachine Learning
2026
An agentic workflow from mathematical statements in quantum-computing papers to Lean 4, with back-translation for semantic review.
MathFormal MethodsQuantum ComputationAutoformalizationAutomated Theorem Proving
2025
A graphical calculus for fermionic tensors, Gaussian states, Majorana operations, fermionization and fermionic codes.
MathQuantum ComputationFermionic SystemsGraphical CalculusQuantum Error Correction
npj Quantum Inf. 11, 112 (2025)
Explicit circuits and anyon-charge measurements for universal computation with the S₃ quantum double, including error-correction protocols.
Quantum ComputationQuantum Error CorrectionTopological Order
Phys. Rev. X 15, 031060 (2025)
Adaptive finite-depth circuits for preparing solvable anyon theories and implementing long string operators through gauging and ungauging.
MathQuantum ComputationTopological Order
2023
Anyon tunneling, non-Abelian Floquet codes and logical gates enabled by transitions between topological phases.
MathQuantum ComputationTopological OrderQuantum Error Correction
Phys. Rev. C 104 054902 (2021)
Universal behavior of the η/π⁰ ratio in collision data, using empirical fits and Gaussian process regression to constrain photon backgrounds.
Nuclear PhysicsMachine Learning
Education
Doctor of Philosophy (Quantum Computation) GPA: 5.0/5.0
Massachusetts Institute of Technology (September 2020 – September 2026)
Main Courses: Quantum Information Science II & III, Quantum Field Theory II & III, General Relativity, Algebraic Topology, Manifold Analysis, Holography, String Theory
Master of Arts (Nuclear Physics) GPA: 3.95/4.00
Stony Brook University (2018 – 2020)
Main Courses: String Theory I & II, Mathematical Physics, Nuclear Physics, Quantum Field Theory I, Group Theory
Atomic Inference
At Atomic Inference, we focus on formal reasoning and formal verification for quantum and classical computation. Formal verification uses mathematical proofs to establish that programs meet precise specifications, helping identify logical errors and provide rigorous guarantees about their behavior.
We are currently raising funds. If you are interested, please contact me by email or on LinkedIn.
