Show HN: zkGolf – Competitive optimization of formally verified circuits

6 comments

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