Curriculum Vitæ

• Developing auto-formalization infrastructure with FAIR’s Core Learning and Reasoning group; maintainer of AutoformBot.

• Contributions to Mathlib4, the world’s largest formalization library.

• Solved and designed graduate-level problems in differential geometry and stochastic differential equations to train AI models for clients including Alphabet Inc. and OpenAI; promoted to senior reviewer on reinforcement-learning datasets.

• Graded homework and exams for three undergraduate Arithmetic & Algebra courses.

• Taught five high-school classes — Algebra I, Algebra II, Computer Science, and Discrete Mathematics — at the oldest boarding school in the United States.
• Spearheaded an AI mentorship program; led nine students to a Capture-the-Flag hackathon, where they outscored two undergraduate teams.

Math Formalization in Lean. Co-organizer of the weekly NYC Lean meetup. Author of a complete, sorry-free Lean 4 formalization of the classification of compact surfaces. Contributor to open-source formalization projects including Michael R. Douglas’s Jacobian Challenge, Rémy Degenne’s Brownian Motion, Mathlib’s manifold geometry library, and an ongoing formalization of Stokes’ Theorem. Author of Marathon, a human-driven autoformalization framework for Aristotle and Claude; maintainer of WikiLean, an AI-moderated, annotated mirror of WikiProject Mathematics for Mathlib declarations. Delivered the talk “4 Reasons You Should Care About Math Formalization” at Wikipedia Day 2026.

Medical Device Engineer · Northeast Ohio Medical University. Lead engineer on a granted research team; designed, prototyped, and presented a patented medical device to improve post-operation care for cancer patients. Winner of the legacy team award at Neovations 2025.

AI and Statistical Models. Implemented image-classification CNNs, FFNs, and genetic algorithms in TensorFlow, and Brownian-bridge stochastic simulations in MATLAB. Wrote ADAM backpropagation from scratch in NumPy.

Self-Studying Mathematics. Passed the Stony Brook PhD comprehensive exam. Scored 11 on the 2025 Putnam exam. Contributor to WikiProject Mathematics. Seminar attendee: Einstein Chair (CUNY), Symplectic Geometry (Stony Brook), (Fun)damental AI and Math (Columbia), and the Simons Center colloquium. Worked through every problem in seven textbooks, including Friedberg–Insel–Spence’s Linear Algebra, Needham’s Visual Differential Geometry, and Lee’s Introduction to Smooth Manifolds.