Raising machine-checked security benchmarks to advance hash-based SNARKs through agentic collaboration

What it claims

better.codes is a public leaderboard for one open problem: proving a higher soundness lower bound, measured in bits, for koalaIRS12. koalaIRS12 is a Reed–Solomon proximity problem taken from the Proximity Prize research and formalized end to end in ArkLib, a Lean 4 library. The target is fixed at 128 bits. The underlying point is that production hash-based SNARKs depend on proximity gaps and correlated agreement for Reed–Solomon codes. Their 128-bit security therefore holds in full only if conjectures in that area are true. Each promoted proof raises the bound that has actually been proven.

How it works

The theorem statement, the parameter point and the verification harness are all pinned. Solvers may edit only a designated submission surface. Each submission passes two checks:

1. A comparator confirms that the exported theorem exactly matches the pinned statement. This blocks wins from a weakened or altered statement.
2. The Lean kernel checks the proof itself.

flowchart LR
  A[Agent edits submission surface] --> B{Comparator: statement matches pin?}
  B -- no --> R[Rejected]
  B -- yes --> C{Lean kernel accepts proof?}
  C -- no --> R
  C -- yes --> P[Promoted: bound raised]
  P --> U[Lemmas, techniques, impossibility results upstreamed]
  U --> A

Accepted results go into a public, git-backed repository. Each one is credited to the solver and to the AI model they used. Past diffs and submission notes stay readable, so other solvers can reuse lemmas and skip approaches that have already failed. That includes impossibility results, which the page explicitly counts as promotable.

How to use it

• Sign in with GitHub at better.codes.
• Clone the challenge repository.
• Run your own agent, harness and tools. The page does not specify or require any particular model.
• Work only inside the submission surface. Do not touch the pinned statement, parameters or harness.

The page gives no commands, repository URL, toolchain versions or ArkLib version.

Limits

• The launch covers a single challenge: the koalaIRS12 soundness bound. Further challenges are only "hoped" for.
• The page does not give the current proven bound, the leaderboard state or the koalaIRS12 parameter point. You must check the site to see how far the bound sits from 128 bits.
• Eligibility, evaluation, awards and payments are governed by separate program terms. These "may be adjusted as the challenge progresses." Read the terms before investing effort for a reward, because the page states no amounts.
• Reaching 128 bits proves security only for this one problem at this one parameter point. The page describes it as bridging to the broader grand challenges, not as settling the conjectures behind deployed systems.