Highlighted projects

Topics include formalized mathematics, information theory, distributed learning, and space communications.

Capacity Atlas: formalizing the map of information theory

Capacity Atlas is a (hopefully) community-maintained registry of channel-capacity problems. It has records of know bounds, and can have Lean formalizations that accompany them. We also reference the primary sources for each proof.

This was inspired by Thomas Bloom’s Erdős Problems website, erdosproblems.com, which was very lively in the mathematics community in 2026. Ideally, this will bring the same energy to the information-theory community, where many problems are still open.

AI for mathematics and formalized mathematics

My current work focuses on AI for theorem proving and formalized mathematics. At Princeton, I work on research and tool development in AI for mathematics.

I previously organized a group for people in the greater Los Angeles area to learn how to write mathematical proofs in Lean. I have contributed to Compfiles, Sphere-Packing, and OrderedSemigroups, among other projects.

Parameter-free decentralized learning

Tuning learning rates is a major pain point in online learning. In the decentralized setting, the problem is harder because nodes must coordinate with one another and may have different optimal learning rates.

In our first paper, we proposed a decentralized online learning method that does not require learning rates and achieves sublinear network regret bounds. To do this, we extended the parameter-free framework from Francesco Orabona and Dávid Pál with a gossip consensus scheme. We also developed a new betting-function framework that is easier to analyze and that we believe is of independent interest.

Follow-up work introduced DECO-EF, which combines parameter-free coin-betting predictions with compressed, difference-based gossip. It gives the first expected sublinear network-regret guarantees for parameter-free decentralized online learning under compressed communication, to the best of our knowledge.

The first paper’s analysis requires a linear gossip schedule—in learning round t, we perform t rounds of gossip—to achieve sublinear regret bounds, which is impractical. In every experiment, however, a constant number of gossip rounds works well. We conjecture that the linear schedule is an artifact of our analysis and that a constant schedule is sufficient, but proving this remains an open problem.

The code for this project is available on GitHub.

Privacy-preserving error feedback for distributed learning

Practical distributed learning often uses aggressive, biased compression for communication from clients to the server. Guaranteeing convergence, however, typically requires client-specific control variates for error feedback.

Per-client control variates undermine privacy guarantees and scale poorly with the number of clients. To address this, we proposed a framework that uses previous aggregated client updates for feedback. This permits highly aggressive compression without the privacy and scaling problems of client-specific control variates. The open-source code is available on GitHub.

Truly decentralized learning on directed graphs

Decentralized optimization algorithms typically require bidirectional communication between nodes.

For directed networks and non-convex losses, existing algorithms required each node to know how many listeners it had—its out-degree. We proposed a line of work that avoids this requirement.

The framework also naturally accommodates network delays: we can add imaginary nodes to model delayed communication and use the same analysis to obtain convergence guarantees.

Asynchronous federated learning meets compression

In 2021, Meta announced FedBuff, a system for asynchronous federated learning with buffered aggregation. In plain terms, the server waits for a certain number of client updates and then averages the updates in the buffer.

Its analysis did not consider communication compression, a key component of practical federated learning systems. We proposed an algorithm with a similar buffered asynchronous structure and a hidden-state feedback mechanism that supports highly aggressive communication compression.

We proved that the algorithm behaves nicely with respect to the compression parameter: the asynchrony and compression error cross-terms are negligible in the convergence rate.

Our analysis also revealed and fixed a bug in the original FedBuff convergence proof, without requiring its bounded-gradient assumption. Independently, Mohammad Taha Toghani and César A. Uribe proposed another fix, though without considering compression.

Error-correcting codes from generalized quadrangles

Together with Simeon Ball, we developed a method to construct point-line incidence matrices for several families of generalized quadrangles in polynomial time. The running times have degrees 4, 6, and 11 depending on the family—high, but still an improvement over existing exponential methods.

Using these constructions, we built what is, to our knowledge, the largest repository of point-line incidence matrices for generalized quadrangles. The matrices are also quasi-cyclic, a desirable property when constructing error-correcting codes from generalized quadrangles. The repository includes matrices in the .alist format for running LDPC simulations.

Maintaining communication while entering the Martian atmosphere

During the Entry, Descent, and Landing phase of rover missions to Mars, communication is lost because of the large Doppler shift caused by the spacecraft’s rapid deceleration in the Martian atmosphere. During my time at JPL, we proposed a system that tracks this Doppler shift to maintain communications throughout the phase.

This system will be implemented in the next generation of NASA’s spacecraft radios.

As part of this work, we also derived an analytical approximation for the frequency-error standard deviation of phase-locked loops, which is of independent interest.

Things I built for fun

• A Snake game in Java.

• Commonly Cited, a tool that gives the most commonly cited authors in a given paper’s references. It has a web interface and a command-line interface.

• claim, a claim registry for mathematics, where you can post a hash of some math work while you work on the exposition.

• arxiv-latex-cleaner, a web-based interface to clean up LaTeX source files for arXiv submissions. It’s a fork of the original arxiv-latex-cleaner by Google research.

• pdf-canary, a tool to insert canary strings into PDFs, with both web and client interfaces.

• A nicer version of Princeton’s Math Department Calendar, with speaker names instead of just the talk titles.