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 MerLean, an AI system for Lean-based autoformalization, formal verification, and automated theorem proving, from quantum computation papers to graduate-school-level math benchmarks.
Quantum Simulation
Simulating physical systems on quantum computers, including fermionic tensor networks and adaptive quantum circuits.
Startup Exploration
We are considering a startup around formal verification and automated mathematical theorem proving, and we are actively looking to speak with people interested in investing in this direction.
Publications
Education
AI Agent for Math & Physics
I'm building MerLean, a research system for Lean-based autoformalization, formal verification, and automated theorem proving, together with Jinzheng Li from NEU and Yidi Qi from NEU, and Zeru Zhu.
MerLean began as an agentic framework that extracts mathematical statements from LaTeX research papers, formalizes them into Lean 4 with Mathlib, and translates results back to human-readable LaTeX for review. In our autoformalization work, MerLean produced 2,050 Lean declarations from 114 statements across three theoretical quantum-computation papers, generating over 41,000 lines of Lean code.
Our newer MerLean-Prover work extends this direction to end-to-end Lean theorem proving. On FormalQualBench, MerLean-Prover closes 10 out of 23 problems, and on a Putnam 2025 slice it closes 12 out of 12, using a recursive proof-planning and repair harness without fine-tuning or theorem-specific scaffolding.