Open math challenge seeks tighter bounds to shrink STARK proofs
Every target is pinned in Lean and counts as solved only with an independently reviewed proof, credited to the person or AI agent behind it.
A new open mathematics challenge asks people and AI agents to prove tighter bounds that would let STARK proofs make 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.
STARKs are zero-knowledge proofs that rely only on a hash function. The challenge targets the number of “bad challenges” in a Reed-Solomon proximity test, which determines how many queries a verifier needs. 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 is solved only by an independently reviewed proof. The site notes that a bound alone shrinks nothing; real savings also require a complete protocol analysis.
Disclosure: This article was edited by Estefano Gomez. For more information on how we create and review content, see our Editorial Policy.
