1) Then more math should get formalised in lean.

2) How is a solution by LLMs supposed to be verified without such a formalisation?