Pittsburgh, PA · Mathematical Sciences @ CMU
Student researcher focused on formal methods, neural machine translation, and the geometry of reasoning systems. I like turning abstract structure into usable software and readable proofs.
Currently learning
Loading...
Active palette
—
From my library
Current labs, collaborations, and systems I keep alive.
Researcher — Unity: A Faithful Autoformalization Pipeline for Lean4
Building a RAG-free, process-driven translation pipeline from English to Lean4 with explicit faithfulness checks and bidirectional alignment.
Founding Engineer — Agora
Building multi-agent reinforcement learning infrastructure with robust market mechanics, orchestration, and evaluation at scale.
Student — Model Theory & Categorical Logic
Guided study on signatures, ultraproducts, adjoint semantics, and categorical formulations of logical systems for automated reasoning.
Only the signals I still want visible on the surface.
Neon-saturated twist on Breakout with a little too much personality.
Orbital tracking visualizer. Public link coming soon.
Solutions write-up for the 2021 Thomas Jefferson Physics Olympiad.
Science Olympiad Materials Science test I wrote and keep around for nostalgia.
Working notes, short write-ups, and stubborn curiosities.