My claim was not that an LLM was a formal, mathematically sound non-monotonic logic engine, but that the problem space is "non-monotonic" and "open world". The fact that an LLM is "unsound" and "informal" is the exact reason why my approach is necessary. Because LLMs are unsound, informal, and probabilistic, as you say, forcing them to interface with Lean 4 is a disaster. Lean 4 demands 100% mathematical soundness, totality, and closed-world perfection at every step. An LLM will just hit a brick wall. Methods like Event-B (which I suggest in my article), however, are designed to tolerate under-specification. It allows the LLM to provide an "unsound" or incomplete sketch, and uses the Proof Obligations to guide the LLM into a sound state via refinement.