Comment by nopurpose

Is Lean so bullet-proof that it never has soundness problems? Something LLM can exploit deep down without anyone noticing.