[rirze]

So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?

[chews]

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.