ANSHULA GANDHI

University of Cambridge Winter '23 -

Mathematics PhD Student

Working to examine conflict-driven reasoning in mathematical proof discovery. Focusing on how mathematicians learn from failure when searching for mathematical proofs, how and why they strengthen statements, and what happens when they fail to prove those strengthenings. Supervised by Prof. Timothy Gowers.

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.

Algorithms to Generalize ProofsSummer '24

Illustrated research talk presenting an algorithm to generalize mathematical proofs, discussing the tactic's implementation in Lean, and more broadly, the role of generalization in learning from failure in mathematics. Presented at the Women in Formal Mathematics workshop at the Hausdorff Research Institute for Mathematics.

(Slides) (Video with subtitles)

Hats & Hamming DistanceSpring '22

Illustrated expository talk based on Noga Alon's Problems and Results in Extremal Combinatorics* about a strategy to figure out what color hat is on your head using the probabilistic method and Hamming distance.

(Video)

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.

(Slides)

Additive Latin Transversals using Combinatorial NullstellensatzSpring '19

Illustrated expository talk based on Noga Alon's Additive Latin Transversals*. Talk given in MIT’s Seminar on Combinatorics course.

(Slides)

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.

(Slides)

CompactnessWinter '24

A few comics that teach the topological notion of compactness by asking and answering important philosophical questions about pancakes.

Real AnalysisSpring '17-'20

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

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.