@tao@mathstodon.xyz I don't understand why we don't hear more about serious efforts to use OpenAI-scale compute to essentially brute-force valid LEAN proofs, then feed them into generative AI model training.