Curriculum Vitæ

• Develop autoformalization infrastructure with FAIR’s Core Learning and Reasoning group.
• Maintain AutoformBot.

• Contribute to Mathlib4, the world’s largest formalization library, with the Formal Frontiers team.

• 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 across Algebra I, Algebra II, Computer Science, and Discrete Mathematics at the oldest boarding school in the United States.
• Spearheaded an AI mentorship program and led nine students to a capture-the-flag hackathon, where they outscored two undergraduate teams.

• Co-organizer of the weekly NYC Lean meetup.
• Author of a complete, sorry-free Lean 4 formalization of the classification of compact surfaces.
• Author of Marathon, a human-driven autoformalization framework for Aristotle and Claude.
• Maintainer of WikiLean, an AI-moderated mirror of WikiProject Mathematics annotated with links to Mathlib declarations.
• 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.
• Gave the talk “4 Reasons You Should Care About Math Formalization” at Wikipedia Day NYC 2026.

• Lead engineer on a research team; designed, prototyped, and presented a patented medical device to improve post-operative care for cancer patients.
• The team won a Legacy Award at NEOvations 2025.

• Implemented image-classification CNNs, FFNs, and genetic algorithms in TensorFlow, and Brownian-bridge stochastic simulations in MATLAB.
• Wrote backpropagation with the Adam optimizer from scratch in NumPy.

• Scored 11 on the 2025 Putnam Competition.
• Contributor to WikiProject Mathematics.
• 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.
• Attendee of the Einstein Chair (CUNY), Symplectic Geometry (Stony Brook), and (Fun)damental AI and Math (Columbia) seminars, and the Simons Center colloquium.

AI for Verifiable Coding workshop