ZkGolf platform invites developers to optimize zero-knowledge proof circuits via LLMs

Researchers launched zk.golf, an open competition to produce formally verified, optimized zero-knowledge proof circuits using large language models. Zero-knowledge proofs require computations to be expressed as circuits — systems of polynomial equations — which are costly to generate and traditionally hand-optimized by experts. The team first tested the approach on SHA-256 compression, writing a formal specification in Lean and prompting Claude Opus to write and iteratively optimize the circuit. The LLM autonomously discarded unsound optimizations it could not formally prove, ultimately producing a circuit that outperformed the current human-optimized state of the art in constraint count. The project aims to lower the barrier to ZKP adoption by combining LLM-driven development with rigorous formal verification.