Show HN: zkGolf – Competitive optimization of formally verified circuits
68 points by rot256
by pvillano
0 subcomment
I look forward to the coming era of human-optional formally verified programming competitions.
I wonder what other optimization+verification problems are out there that will make good LLM feedback loops.
Maybe something with query planners.
by baby
0 subcomment
I'm racing to be the first submission, amazing project :)
by IshKebab
3 subcomments
Neat, but I feel like you need to define "circuit" on that page! I thought this was like for silicon design or something.
by tancop
0 subcomment
someone named "zrschresearch" is cheating. looks like they found a way to only measure cost on specific best case inputs where its trivially 0. its using a correct implementation so the proof checks out but the cost is obviously fake.
by TheFirstNubian
0 subcomment
Saw this earlier on LinkedIn and checked it out. Awesome initiative!
by rirze
1 subcomments
So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?
Hacker News