Rendered at 04:28:35 GMT+0000 (Coordinated Universal Time) with Cloudflare Workers.
pvillano 21 hours ago [-]
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.
baby 2 days ago [-]
I'm racing to be the first submission, amazing project :)
IshKebab 1 days ago [-]
Neat, but I feel like you need to define "circuit" on that page! I thought this was like for silicon design or something.
ludamad 1 days ago [-]
A matter of perspective. Anyone who works with SNARKs (ZK or otherwise) gets the terminology right away
AtHeartEngineer 1 days ago [-]
Circuit is the standard term used for zero knowledge "programs"
sigbeta 21 hours ago [-]
this is super cool, didnt know zk circuits are really generalized version of all sorts of physical circuits
baby 15 hours ago [-]
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)
tancop 12 hours ago [-]
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.
TheFirstNubian 1 days ago [-]
Saw this earlier on LinkedIn and checked it out. Awesome initiative!
rirze 1 days ago [-]
So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?
chews 21 hours ago [-]
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.
I wonder what other optimization+verification problems are out there that will make good LLM feedback loops.
Maybe something with query planners.