Hello! I recently completed my undergraduate studies at MIT in mathematics and history.

I currently do research in combinatorics, formal verification, and automated theorem proving. I have previously conducted research in robotics, nanosystems, and astrophysics.

You can download my CV here.

Research Experience

  • Fulbright at Czech Technical UniversitySummer '21

    Fulbright Student Researcher

    Worked with mathematicians under a Fulbright student grant to develop tools for automated deductive reasoning in Lean. Focused on using automated-theorem-proving tools in combination with human insight and ingenuity to prove mathematical lemmas, focusing on lemmas crucial to the polynomial method. Code here.

  • MIT Center for Brains, Minds, and MachinesWinter '20 - '21

    Research Assistant

    Developed program synthesis techniques to solve symbolic reasoning problems through applying neuroscience behind how humans logically reason. Worked under Prof. Tomaso Poggio. Paper here.

  • The National Autonomous University of MexicoFall '19

    Research Assistant

    Developed Coq tactics and a reinforcement learning environment to automate proofs in lattice theory. Worked under Prof. Favio Ezequiel Miranda Perea and Prof. Lourdes del Carmen González Huesca. Paper here.

  • MIT Center for Brains, Minds, and MachinesSpring '19

    Research Assistant

    Designed reinforcement learning environment to prove mathematical theorems in group theory. Worked under Prof. Tomaso Poggio. Read more here.

  • MIT Distributed Robotics LabSpring '16, Fall '17–Fall '18

    Research Assistant

    Constructed risk-estimating cost function and developed path-planning algorithms for safer autonomous vehicles. Worked under Prof. Daniela Rus. Paper here.

  • MITRE Nanosystems GroupSummer '16

    Research Assistant

    Developed circuits and algorithms for non-invasive medical device to reduce size, weight, and required power. Worked under Dr. Matthew Dunlop-Gray.

  • MIT Exoplanet Theory LabSummer '15

    Research Assistant

    Algorithmically classified thousands of life-identifying chemical spectra to pave way for detecting life on other planets. Worked under Prof. Sara Seager.

  • NASA Goddard Space Flight Center Summer '14–Summer '15

    Research Assistant

    Developed microlensing-based exoplanet detection algorithms to be deployed on NASA’s WFIRST telescope. Worked under Dr. Richard Barry.


Research Blog

Educational Comics

  • Real Analysis

    A few comics that teach the mathematics of formalizing calculus by asking and answering the philosophical questions that gave rise to each concept.

Illustrated Talks