Comment on Show HN: zkGolf – Competitive optimization of formally verified circuitsComments−rirze2moSo... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?−chews2moIn 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.
Comments
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.