On September 11, 2026, I reached #1 on the better.codes soundness leaderboard under my GitHub handle, partylikeits1983. The accepted submission scored 68.06 bits, improving on the previous best of 68.04.
That ranking is a snapshot from September 11. The leaderboard will likely have changed by the time you read this. In my view, it's one of the most competitive research competitions in the world, and submissions move quickly.
The leaderboard in September 2026. The first-place entry includes my work and credits me under partylikeits1983.
The Proximity Prize studies a concrete problem involving interleaved Reed-Solomon codes. A Reed-Solomon code represents data as evaluations of a low-degree polynomial; list decoding studies the valid codewords within a specified distance of a received word. The challenge asks for Lean proofs of tighter bounds on a reduction used in proximity testing. The score measures a spot-check bound derived from a certified radius.
I gave the agent a private repository I had already been developing to formalize the grand list decoding prize problem, along with extensive HackMD notes from studying Reed-Solomon codes. That preparation gave it definitions, context, and existing work to build on. I also got lucky with the model: GPT-6 Astra was exceptionally capable on this task.
I still reviewed the changes and manually simplified the Lean code. Much of my feedback was basic engineering: this proof is too verbose; this argument can be simplified. One improvement in my submission, PR #549, used discrete convexity to replace exhaustive checks with boundary checks, while proving that those checks covered the full domain.
The competition is intense. While my PR was waiting for CI verification, its code was reused and optimized in another submission. 76 of the 81 submission files in the accepted PR #551 are byte-for-byte identical to files in my earlier PR. Most of the accepted submission was the code I had submitted. My PR was eventually verified at the same score, then closed because that score had already been promoted.
I received recognition for the work, which is what matters to me. Thank you to i34-9 for acknowledging my contribution and preserving the attribution; the accepted PR also credits 0xLucqs. I would still prefer submissions to remain private until verification finishes, so credit is less dependent on the CI queue.
I'm happy to have reached the top. Mathematical preparation, a capable agent, and careful code review all played a part.