ARPA-H and RAMMP

I've used a powered wheelchair my whole life, so the research I'd put first isn't mathematics, and it isn't mine alone. ATDev, the company I co-founded in 2020, co-leads RAMMP, a five-year, $41M program funded by ARPA-H, the Advanced Research Projects Agency for Health. The University of Pittsburgh leads it under Dr. Rory Cooper, alongside Carnegie Mellon, Cornell, Northeastern, Purdue, Kinova and LUCI.

My part is ATOS, the open platform layer. A powered wheelchair today is a closed appliance from a single vendor, so who controls its software isn't an abstract question to me. ATOS is wheelchair and mobility middleware on ESP-IDF, built so the chair can be an open platform under an independent foundation instead. Open, not owned. The engineering, and why the governance matters as much as the code, are on the assistive technology page.

Mathematics and security

One rule runs through all of this: a result doesn't count until something has tried to kill it. zeta-function is the one that gets worked on. A computational research program in Python and Lean 4, run by six specified agent roles under a compute budget. So far it has produced 218 documented findings. Negative results are first-class output. Dead ends get filed, not buried.

tor-wf-lab holds two investigations into Tor website fingerprinting: whether a guard relay can effectively buy the start of your page load just by being fast, and whether robustness to network mismatch and robustness to temporal drift are actually two separate axes rather than one.

hadwiger-nelson is research on the chromatic number of the plane, the Hadwiger-Nelson problem.

assay is the newest and by far the smallest: a research loop built to refuse its own results, putting calibration gates, non-vacuity probes and independent verification between an autonomous mathematical process and anything it wants to claim. It says no to itself first.

Mathlib 4

The work that has taken the most outside scrutiny went into somebody else's project. Two contributions to Mathlib 4, the Lean 4 mathematics library, have been merged: riemannZeta_conj, the conjugation symmetry of the Riemann zeta function, and a result covering the digamma function's iterated recurrence, harmonic-number values, and duplication formula. They took 8 and 14 review comments to land. A third, the rational root theorem with multiplicity, is still in review. I'm not counting it until it lands.

Parked

A set of repositories is parked, and I won't call it live work. They're aimed at Millennium Prize problems: P versus NP, Navier-Stokes, Yang-Mills, Hodge and Birch and Swinnerton-Dyer, plus a formalization of the Poincaré conjecture, which is already solved. Each one is a study of the problem plus a substrate meant to support further work on it. I'm not currently active in them. They stay public because the write-ups are still worth reading, not because anything is moving. Parked means parked.

Background

Mathematics coursework at UC Berkeley, 2009 to 2012, is where most of this started.

I haven't solved anything famous. What I do have is honest negative results and verification: exactly what was tried, what failed, and why, so a failure is on the record instead of silent. That's the whole claim.