Collin Yuanjie Ren
PhD Candidate in Physics @ MIT
I'm currently a PhD candidate in the Physics Department at MIT, under the supervision of Peter Shor and Aram Harrow.
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.
Research
My research spans three complementary areas at the intersection of quantum information and theoretical physics:
Topological Quantum Codes
Developing quantum error-correcting codes and understanding their connections to topological phases of matter, including universal circuit constructions and phase transitions.
Agent for Math & Physics
Building AI agents that automatically extract mathematical statements from LaTeX, convert them into formally verified Lean 4 code, and translate results back for human review.
Quantum Simulation
Simulating physical systems on quantum computers, including fermionic tensor networks and adaptive quantum circuits.
Job Market
I will be on the job market in the 2025-2026 academic year, looking for a research position in a company or a postdoc position in a university. Please don't hesitate to reach out for academic collaboration or entrepreneurship whenever you share similar interests!
Publications
Education
AI Agent for Math & Physics
I'm building MerLean, an agentic framework for autoformalization in quantum computation, together with Jinzheng Li from NEU and Yidi Qi from NEU.
MerLean automatically extracts mathematical statements from LaTeX documents, converts them into formally verified Lean 4 code using Mathlib, and translates results back to human-readable LaTeX for review — all without human intervention. We demonstrated the framework on a quantum computation paper, generating 1,450 Lean declarations from 48 mathematical statements covering stabilizer formalism, Pauli algebra, transversal gates, gauging graphs, and fault-tolerant measurement.