UCLA undergraduate in Data Theory, Cognitive Science and Political Science, class of 2028. I work on reliable AI for human and multi-agent decision systems, and I also build interactive simulations.
- proofnet-ir — verified correctness checking for proof nets in multiplicative linear logic, in Lean 4. v0.10.0 decides correctness with Guerrini's sequential procedure, with proved termination and a quadratic cost bound; 1,191 audited declarations use only Lean's three standard axioms.
- proof-graphs — order redundancy of Lean tactic proofs: preregistered experiments continuing ProofNet-IR.
- Human–AI grading (UCLA Political Science, in progress) — generative models as both student and grader, measured against a human baseline.
- MCM2026ProblemB — MCM 2026 Problem B, Finalist and MAA Award: MILP and Monte Carlo for lunar logistics with space elevators.
- Simplification-of-Arifovic-Strings-Simulation — an interactive simulation of a minimum-effort coordination game with death–birth dynamics, built for PS 189.
Each one runs in the browser with no build step.
| ripplefield | a 2D ripple tank: interference, diffraction, reflection, refraction |
| gravity-garden | N-body gravity and orbital mechanics |
| murmuration | flocking: tune the steering rules, watch a flock emerge |
| epicyclon | draw a shape, watch rotating circles retrace it via the DFT |
| pathlight | grid pathfinding algorithms, step by step |
| chromalens | colour-vision-deficiency simulation for images |
- veridone — an evidence-first acceptance desk for AI-assisted software work.
- ai-eval-micro-lab — small, auditable experiments for evaluating AI model outputs.
- quant-research-micro-lab and useful-automation-lab — transparent tools for quantitative research and for repetitive local tasks.
- parquet-drift — catch schema drift across Parquet shards before readers do.