It's a fair concern that ML model generates misleading definitions and statements which hides bugs and is hard to detect, but it also depends on how the user ut

It's a fair concern that ML model generates misleading definitions and statements which hides bugs and is hard to detect, but it also depends on how the user utilizes this kind of tools. For any serious use case, before attempting to prove any statements, a responsible user should always carefully define any *top level statements* manually or hire a domain expert to write or review the definition. Once we have high confidence on the definition of the top level statements, the user might start to break down the proving approach into a couple of auxiliary lemmas. From this moment, they can freely play with machine generated code without too much safety concern, because: * the ultimate goal is to prove the original top level statement, which is already human inspected; * if the machine generates a misleading lemma, it won't help proving the top level statement, but it won't lead to a false claim as well, since the proof checker will reject any incomplete or incorrect proof. The worst case is to be fooled by misleading lemmas and waste a lot of time exploring an unhelpful proof approach, which could be sad and costly but won't be a critical safety issue. If ML assisted interactive theorem provers inspired by Lean Chat becomes productivity tools, users should be educated to always do their best to ensure the top level statement is exactly what they want to define, this should be an industry common practice. For critical usage, a theorem prover UI can even enforce this practice by disable auto code generation for top level statements.