Full threadrirze·So... is this a dataset fishing operation essentially? You want to train or collect samples for better Lean proofs?View on HN