8 comments

  • pvillano 13 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.

  • tancop 4 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.
  • baby 1 day ago
    I'm racing to be the first submission, amazing project :)
  • IshKebab 22 hours 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 17 hours ago
      A matter of perspective. Anyone who works with SNARKs (ZK or otherwise) gets the terminology right away
    • baby 7 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)
    • AtHeartEngineer 21 hours ago
      Circuit is the standard term used for zero knowledge "programs"
      • sigbeta 13 hours ago
        this is super cool, didnt know zk circuits are really generalized version of all sorts of physical circuits
  • TheFirstNubian 16 hours ago
    Saw this earlier on LinkedIn and checked it out. Awesome initiative!
  • rirze 18 hours ago
    So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?
    • chews 13 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.
  • rnagulapalle 14 hours ago
    [flagged]
  • Kaizzen 11 hours ago
    [flagged]