I’m not trying to understate the stuff you can do with LLMs or formal proof tooling that could be attached to randomly try things till it reaches a solution to a novel problem, but some solutions you see to lesser problems are sometimes so pie-in-the-sky I think stumbling on one is barely better than a random walk. And I think mathematicians like Tao are far better at narrowing that down. As an aide I can see it’s use, I just don’t believe we’re going to have LLMs & tooling solve these grand problems until compute power is orders of magnitudes better, and even then I’m still sceptical. BUT I’m not a mathematician and this is based on my intuition from pub talks :)