ANSHULA GANDHI
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 automatedtheoremproving 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 riskestimating cost function and developed pathplanning algorithms for safer autonomous vehicles. Worked under Prof. Daniela Rus. Paper here.

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

MIT Exoplanet Theory LabSummer '15
Research Assistant
Algorithmically classified thousands of lifeidentifying 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 microlensingbased exoplanet detection algorithms to be deployed on NASA’s WFIRST telescope. Worked under Dr. Richard Barry.
Publications

NeurIPS 2020 LMCA Workshop.
Authors: Andrzej Banburski, Anshula Gandhi, Simon Alford, Sylee Dandekar, Sang Chin, and Tomaso Poggio.

Supervised Learning with Assemblies
NeurIPS 2020 Beyond Backprop Workshop.
Authors: Akshay Rangamani and Anshula Gandhi.

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

Language Learning and Program Synthesis Dec '20
On a connection between language learning and program synthesis.

Automating proofs of lattice inequalities in Coq Dec '19
On developing a reinforcement learning agent and equipping it with a duality tactic suited for efficiently proving theorems in lattice theory.

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

Getting started with proving math theorems through reinforcement learningSept '19
On laying a framework for machinelearning automated theorem proving at MIT's Brains, Minds, and Machines Lab.
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

Hats & Hamming DistanceSpring '22
Illustrated expository talk based on Noga Alon's paper about a strategy to figure out what color hat is on your head using the probabilistic method and Hamming distance.

The Polynomial Method in CombinatoricsSpring '21
Illustrated expository talk on the polynomial method and its applications to the finite field Nikodym problem and the capset problem. Talk given at the Czech Institute of Informatics, Robotics and Cybernetics.

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

Shamir's Secret Sharing and ZeroKnowledge ProofsSummer '18
Illustrated expository talk on two topics in cryptography: secret sharing and zeroknowledge proofs. Talk given at the cybersecurity company BitSight.