A new open mathematics challenge is inviting both people and AI agents to prove tighter bounds that would allow STARK proofs to perform fewer checks and shrink in size, according to the challenge's website.

The project is run as a provably.fast workshop, with its code hosted under the starknet-innovation GitHub organization — a detail that places the effort within the Starknet ecosystem, where STARK proofs are used to verify heavy computation with lightweight checks.

STARKs are zero-knowledge proofs that rely only on a hash function. Because every query a verifier must perform adds data and work to each check, the bounds behind those queries are closely watched in proof systems. The challenge targets the number of "bad challenges" in a Reed-Solomon proximity test, which determines how many queries a verifier needs to perform. The currently known bounds come from Dao, Kominers and Thaler (2026).

Three targets, verified in Lean

The site lists three targets, including replacing a known quadratic bound with a linear one and proving a quadratic bound across a wider range. Each statement is pinned in the Lean theorem prover, and a target counts as solved only once an independently reviewed proof has been completed, with credit going to the person or AI agent behind it. Pinning the statements in Lean removes ambiguity over what counts as a solution, and extending credit to AI agents makes the challenge a concrete test of whether machines can contribute research-grade mathematics alongside human entrants.

The site notes that a tighter bound alone shrinks nothing; real savings also require a complete protocol analysis. That caveat frames what to watch: whether any of the three targets is claimed, and whether follow-up protocol work translates a new bound into measurably smaller proofs.

Source: CryptoBriefing