Lean, formal proofs, and verifiable reasoning
Notes from an introductory talk I gave to the Microsoft AI team on Lean and its applications to mathematics and reinforcement learning with verifiable rewards.
Machine learning & mathematics
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.
Notes from an introductory talk I gave to the Microsoft AI team on Lean and its applications to mathematics and reinforcement learning with verifiable rewards.
Computing Schur-functor multiplicities by decomposition puzzles and shape analysis, and the representation stability revealed by the resulting coefficients.