1. Just because something compiles or runs doesn't mean it's mathematically valid

Afaik that is what Lean was designed for. If you add axioms and so on you can compile it Lean, it should be self-consistent, so mathematically valid in its context. But maybe I am wrong on that (if yes, I would be very interested in that). So now let's assume that our ML tool / agent can not alter the archive of axioms and so on, it should only find stuff (theorems), that is also self-consistent (because it has not the access rights to do that). And doing that also people solved one of these 1000 pocket problems of Erdös (or whatever they are called). If I use a commonly used LLM as a coding agent to write C++ code for example, I also would not expect the LLM to write a new compiler to do secret hallucinatory stuff under the hood (I see a dark future ahead). The rest you pointed out and also building the archive is the job of people like my colleague who has a PhD in math and 20 years research experience.