Henry Robbins

Hello! I’m a second year PhD student in Management Science & Engineering at Stanford University, advised by Ellen Vitercik and Madeleine Udell. My research focuses on verifiable AI optimization modeling.

Prior to my PhD, I built AI tools for wetlabs as the Founding Engineer at Saddlepoint Labs, and I worked on waiting dynamics and scheduled shared rides as an Applied Scientist on Uber’s Shared Rides team.

During my undergraduate years, I helped develop Cornell’s COVID-19 response. With a small team, I redesigned the course roster and made recommendations for return-to-campus testing policies.

Outside of work, I enjoy reading about computational creativity, making images, and seeing as much live music as I can.

hw.robbins@gmail.com github/henryrobbins linkedin/hwr26

Selected work

2026 · Working paper

FLARE: Verifying MILP Reformulations with LLM-Based Theorem Proving

HR, Connor Lawless, Madeleine Udell, Ellen Vitercik

Verifying MILP reformulations with LLM-based automated theorem proving

paper · github · site

Mixed-Integer Linear Programming (MILP) is a fundamental tool for combinatorial optimization with extensive real-world applications. A central challenge is designing efficient MILP formulations. Large Language Models (LLMs) offer new opportunities to automate the modeling process, from deriving formulations to strengthening them. To ensure correctness, we need robust methods to compare formulations. However, existing approaches evaluate formulations numerically and fail to reason about general problem instances. We resolve this limitation by introducing a constructive notion of MILP reformulation that can be formalized in Lean and machine-checked. We develop FLARE¹ (Formulation-Level Automated Reformulation Evaluation), a method that uses an LLM-based agent and the Lean proof assistant to verify proposed reformulations against a reference. To evaluate our approach, we introduce FormulationBench², a challenging dataset of 20 problems and 109 formulations. FLARE outperforms existing methods, with 100% accuracy on the NP-hard subset of FormulationBench. Furthermore, FLARE produces a machine-checkable certificate for every reformulation it accepts. For cases where formal guarantees are not necessary, we introduce FLARE-NL, a fast and cheap LLM proxy that matches FLARE’s accuracy but produces no certificate.³ These methods enable reliable verification in automated optimization modeling.

FLARE is implemented in the milp-flare Python package; see https://flare.henryrobbins.com. ↩
Download via the formulation-bench Python package; see https://formulation-bench.henryrobbins.com. ↩
All experimental code is available at https://github.com/henryrobbins/flare. ↩

2026

FormulationBench

A dataset of MILP formulations and Lean reformulation proofs

Python utilities for loading and working with the FormulationBench dataset. FormulationBench is a collection of 20 optimization problems with 109 mixed-integer linear programming (MILP) formulations. Each formulation has a natural language description, LaTeX formulation, GurobiPy implementation, and Lean representation. Furthermore, there are 89 pairs of formulations consisting of 63 positive reformulation examples and 26 negative examples. Each positive example has a machine-checked Lean 4 reformulation proof. See the documentation for details.

github · site

2026

OpenATP

A Python package providing a common interface for automated theorem proving

OpenATP is an open-source Python package providing a common interface for automated theorem proving (ATP). OpenATP focuses on recent agentic ATP methods that prove formal statements in Lean. Each method runs in an isolated sandbox, either locally with Docker or remotely with Modal. OpenATP also provides benchmarking utilities to run methods on common datasets.

Supported ATP methods include: Claude Code, Codex, DeepSeek, Grok, Muse Spark, AxProverBase, Leanstral, Kimi Code, Numina, and Aristotle. See the documentation for an up-to-date list.

github · site

2026

showcount

A website for tracking and sharing the concerts you attend

I really like live music. I’ve been tracking the shows I attend on a personal website for several years. Recently, I created showcount.com, a website for tracking and sharing concert attendance. It has all the bells and whistles as my prior website, but anyone can make an account and share their list with friends.

I’m aware there are many other concert and setlist tracking websites (Phantasy Tour, Concert Archives, Songfish, Setlist.fm). I built showcount because I wanted full creative control and full access / ownership of my data. I also didn’t want to manually upload my shows to one of the other platforms — showcount has a built-in AI import option that parses arbitrary data formats.

This was also my first experiment with vibe-coding and harness-engineering (see my HN Post).

Footnotes