ANSHULA GANDHI
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

The National Autonomous University of MexicoFall '19
Research Assistant
Developed techniques to automate proofs in lattice theory.

MIT Center for Brains, Minds, and MachinesSpring '19
Research Assistant
Designed reinforcement learning environment to prove mathematical theorems in linear algebra.

MIT Distributed Robotics LabSpring '16, Fall '17–Fall '18
Research Assistant
Constructed riskestimating cost function and developed pathplanning algorithms for safer autonomous vehicles.

MITRE Nanosystems GroupSummer '16
Research Assistant
Developed circuits and algorithms for noninvasive medical device to reduce size, weight, and required power.

MIT Exoplanet Theory LabSummer '15
Research Assistant
Algorithmically classified thousands of lifeidentifying chemical spectra to pave way for detecting life on other planets.

NASA Goddard Space Flight Center Summer '14–Summer '15
Research Assistant
Developed microlensingbased exoplanet detection algorithms to be deployed on NASA’s WFIRST telescope.
Publications

Dynamic Risk Density for Autonomous Navigation in Cluttered Environments without Object Detection
ICRA 2019.
Authors: Alyssa Pierson, Cristian Ioan Vasile, Anshula Gandhi, Wilko Schwarting, Sertac Karaman, and Daniela Rus.
Research Blog

Guaranteeing proof terminationOct '19
On dealing with infinite proof search in reinforcementlearning automated proofs.

Getting started with proving math theorems through reinforcement learningSept '19
Laying a framework for machinelearning automated theorem proving at MIT's Brains, Minds, and Machines Lab.
Educational Comics

Real Analysis Comics
I have written 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

Additive Latin Transversals using Combinatorial NullstellensatzSpring '19
Illustrated expository talk based on Noga Alon's paper given in MIT’s Seminar on Combinatorics course.