Thanks for your reply Kevin. just to share what I was thinking while out walking this morning. I doubt very much we'd see much come out of ML in the capacity

Thanks for your reply Kevin. just to share what I was thinking while out walking this morning. I doubt very much we'd see much come out of ML in the capacity of exhaustive search or pattern seeking vis a vis "large models", because maths is to language as intergalactic space is to a teacup. Doesn't feel like there's a generative potential for stumbling upon "proofy-like" things the way it works with natural language. But I imagine AI in a few years being able to train on a great corpus of known proofs. We show it how to do constructive, deconstructive, contradiction, induction, equivalence... And hopefully what it gives us is a meta insight into the nature of proofs themselves, perhaps by finding new techniques, or revealing refutations... that sort of thing. Those would be tools useful to mathematicians, but I think the BIG finds will still be by made humans who think for 10,000 hours about a problem.