Lean, formal proofs, and verifiable reasoning
An introduction to Lean, its mathematical history, and how formal proofs help us distinguish correct reasoning from plausible answers.
Machine learning & mathematics
I work on reinforcement learning with verifiable rewards.
I'm a Member of Technical Staff on the Post-training team at Microsoft AI. These days I work on the MAI-Code model family where my focus is on applications to mathematics and science. I enjoy using Lean to build scalable, verifiable RL datasets. Before machine learning, I was a mathematician.
An introduction to Lean, its mathematical history, and how formal proofs help us distinguish correct reasoning from plausible answers.
Computing Schur-functor multiplicities by decomposition puzzles and shape analysis, and the representation stability revealed by the resulting coefficients.