/research-work
4/21/2026
work
- Erdős 872, L(n) = o(n) claimed proof: theorem writeup (July 24, 2026)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 formalizationlean 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 recordthe full research record and verification chain. archived: doi:10.5281/zenodo.21545890.
- paperImproved 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 harnesslean proofs and research rounds using the erdos co-researcher harness that led to the erdős problem 872 partial result.
- erdos co-researcherthe public co-researcher agent/harness i built to help automate math research, anyone can clone it.
posts
- autonomous researchwhy 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 and terence tao. 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 :)