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

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

You can download my CV here.

Research Experience

  • MIT Center for Brains, Minds, and MachinesSpring '20 -

    Research Assistant

    Developing program synthesis techniques to solve symbolic reasoning problems through applying neuroscience behind how humans logically reason. 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. Paper here.

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

    Research Assistant

    Designed reinforcement learning environment to prove mathematical theorems in group theory. 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. Paper here.

  • MITRE Nanosystems GroupSummer '16

    Research Assistant

    Developed circuits and algorithms for non-invasive medical device to reduce size, weight, and required power.

  • MIT Exoplanet Theory LabSummer '15

    Research Assistant

    Algorithmically classified thousands of life-identifying chemical spectra to pave way for detecting life on other planets.

  • 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.


Research Blog

Educational Comics

  • Real Analysis Comics

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

Illustrated Talks