# /research-work

*4/21/2026*

> in my free time I try to help with and learn from math and astrophysics research using research agent harnesses

## work

- [Erdős 872, L(n) = o(n) claimed proof: theorem writeup (July 24, 2026)](https://github.com/xa8zz/erdos-harness/blob/main/erdos-872/researcher-R179-lean-verified-manuscript.md) — the claimed L(n) = o(n) proof for Erdős Problem 872, answering two of Erdős's three questions in the negative via a new quotient-cone recursion theorem for divisibility saturation games; the true order of L(n) remains open. submitted to erdosproblems.com July 30, 2026, under community audit. archived preprint: doi:10.5281/zenodo.21545919.
- [Erdős 872 claimed proof: lean formalization](https://github.com/xa8zz/erdos-harness/tree/main/erdos-872/lean/r177_verification) — lean formalization of the claimed proof: the game-theoretic core is kernel-checked; one analytic sieve lemma (Lemma 2.3) is proved in the manuscript and not yet formalized.
- [Erdős 872 claimed proof: research record](https://github.com/xa8zz/erdos-harness) — the full research record and verification chain. archived: doi:10.5281/zenodo.21545890.
- [paper](/papers/erdos-872.pdf) — Improved Bounds for the Primitive-Set Saturation Game (Erdős Problem 872), a partial contribution to a 34-year-old unresolved Erdős problem. (Update July 2026: the claimed o(n) proof above answers two of Erdős's three questions; the true order of L(n) remains open.)
- [erdos harness](https://github.com/xa8zz/erdos-harness) — lean proofs and research rounds using the erdos co-researcher harness that led to the erdős problem 872 partial result.
- [erdos co-researcher](https://github.com/xa8zz/erdos-co-researcher) — the public co-researcher agent/harness i built to help automate math research, anyone can clone it.

## posts

- [autonomous research](https://sensho.xyz/autonomous-research) — why fully autonomous research systems are inevitable, notes from doing AI-driven math research.

my results on erdős problem 872 are posted under Om_Buddhdev_sensho and were credited by both [thomas bloom](https://www.erdosproblems.com/872) and [terence tao](https://github.com/teorth/erdosproblems/wiki/AI-contributions-to-Erd%C5%91s-problems). they've done amazing work advancing and tracking AI's progress on hillclimbing math as a domain, it was actually a tao podcast that nudged me to get involved in the first place, so the whole thing's been a bit full-circle :)

---