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.
they're the same, arithmetic circuits are just made out of addition and multiplication gates. They're used all over the place in programmable cryptography (ZKP, FHE, MPC)
In a world where llms read everything… every human contribution is a fishing expedition. At least here humans are trying to push a very hard frontier that llms arent good at yet.
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.
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.
Neat, but I feel like you need to define "circuit" on that page! I thought this was like for silicon design or something.
A matter of perspective. Anyone who works with SNARKs (ZK or otherwise) gets the terminology right away
they're the same, arithmetic circuits are just made out of addition and multiplication gates. They're used all over the place in programmable cryptography (ZKP, FHE, MPC)
Circuit is the standard term used for zero knowledge "programs"
this is super cool, didnt know zk circuits are really generalized version of all sorts of physical circuits
I'm racing to be the first submission, amazing project :)
Saw this earlier on LinkedIn and checked it out. Awesome initiative!
So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?
In a world where llms read everything… every human contribution is a fishing expedition. At least here humans are trying to push a very hard frontier that llms arent good at yet.