Not really. If you find someone who claims that non-trivial properties of neural networks can be verified by some kind of formal system like Lean then you should post the link because that would be very impressive.
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.