Comment by D-Machine
3 days ago
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.
Stop responding to my comments & save yourself the time & keystrokes. It's better that way for everyone involved since you haven't addressed anything of substance in anything I have written & have opted for nonsensical psychoanalysis.
You haven't said anything of substance, because as I and other commenters here have pointed out, you clearly don't even understand Rice's theorem and why it isn't applicable here. You bring up formal verification with Lean on a thread and topic which is about model explainability. You should just stop posting entirely, you are polluting HN with irrelevant nonsense.
I recommend not telling random strangers what to do w/ their time & letting the moderators deal with the problem. You're not a moderator so stop pretending like you are one.