Nothing in this thread was about Lean.

Nothing you said responds to anything I said.

Rice's theorem (which you are clearly citing, but won't clearly mention, for some reason) has almost zero actual practical relevance to AI explainability.

You make low-quality and low-effort AI-denialism posts whenever you pattern match "all non-trivial semantic properties of programs are undecidable" to... anything you think matches the folk/common understanding of those terms, without considering how irrelevant these statements are to actual real-world applications and engineering.

You ask for links, but post nothing of substance and post no references or even mention relevant details for your own claims.