RL-trained Lean provers mode-collapse at inference time: on miniF2F-test, doubling DeepSeek-Prover-V1.5-RL's sampling budget from k=32 to k=64 solves zero additional theorems. A fixed schedule of 15 tactic skeletons breaks the plateau (+12.3 ± 4.2 theorems across 3 seeds), and a controlled ablation shows the gain comes from tactic structure, not prompt diversity.

Multi-institution benchmark measuring alignment between LLM judges and human experts on university-level mathematical proofs. PhD-level expert evaluator (probability, discrete mathematics, algorithms).

A pre-registered test of whether post-training on abstract visual reasoning (Raven's matrices) improves math. Eight matched-eval SFT and GRPO conditions were all negative on MATH-500 (base 66.8% → 44.0–61.6%); the damage traces to completion compression rather than format failure. Extended to from-scratch 162M pretraining, where a 1% formal-language (Dyck) warm-up cut tokens-to-threshold on compositional algebra by 12.3% against a scrambled control (3/3 seeds).

A systematic study of representation bottlenecks in symbolic algebra, testing where RL breaks on high school math.

An expository derivation using Poissonization and Laplace asymptotics to analyze random walks on lattices.

Ingests a Python codebase, proposes what must be true for it to be correct, translates functions into Lean 4 models, differentially tests each model against the real code, and proves or refutes the claims with the Lean kernel. Screens out sorry, vacuous hypotheses, and unreachable counterexamples, and reports the full trust chain behind every finding.

Live RLHF platform for interactive policy personalization on an RL agent over motion-planning gadget structures. Flask + SQLAlchemy backend serving Maskable PPO models with top-K action inference over a 217-dim action space, custom PyTorch reward model trained on per-action accept/reject feedback, Cytoscape.js trace visualization frontend.

Local LLM self-training loop with step-by-step feedback, written with Rust & Tauri.

A browser-based football career sim: start as a 10-year-old academy trialist and play through scholarships, contracts, transfers, and internationals. In-match decisions feed a deterministic, seeded match engine.

Autoformalization of classical NP-completeness reductions in Lean 4, built on Mathlib and CSLib. Formalizes Karp reductions (SAT ≤ 3SAT ≤ 3-COLORING, with more planned) as machine-checked proofs.

17.279 (Political Misinformation in the Age of Social Media) Final Paper - independent empirical study (n=174, randomized) on AI disclosure effects on belief formation in political conspiracy-framing content.

Autocomplete for math handwriting.

A reflection on my experience navigating race at a UK boarding school.

Isn't it obvious?

A physics microlecture on electromagnetism.