ANSHULA GANDHI

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

• 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 reinforcement-learning automated proofs.

• Getting started with proving math theorems through reinforcement learningSept '19

  On laying a framework for machine-learning 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 cap-set 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 Zero-Knowledge ProofsSummer '18

  Illustrated expository talk on two topics in cryptography: secret sharing and zero-knowledge proofs. Talk given at the cybersecurity company BitSight.