Hacker News Reader

Comment by d0mine | Hacker News Reader

> we use “malicious” to describe code that goes out of its way to trick or mislead the user, exploit bugs or compromise the system. This includes un-reviewed AI-generated proofs and programs.

It is interesting that AI-generated proofs are described as malicious by Lean docs unless reviewed.

View on HN

LLM's have generated "False" proofs in Lean, so that statement is not far off. Malicious or incompetent? Take your pick.

This is misleading. The proofs you speak of contained non-ZFC axioms and/or statements like "sorry". If the Lean proof conjecture is correct and it doesn't introduce any new axioms or use e.g. "sorry" then it provides a MUCH stronger guarantee of correctness than any peer-review done by humans.

It's a simple binary classification. AI-generated proofs can't be "honest", and the only other possibility is "malicious".

The opposite of malicious is not honest. Nor do I see how motivations fall on a binary. The user submitting an AI proof can be honest, or malicious, or careless, or overzealous, or incompetent, or a whole bunch of other things. As far as the AI's motivations, "malicious" is just as much an anthropomorphism as "honest" and both descriptions are absurd. Nor do I really understand how any proof, regardless of its origin can be called honest. I think their definition of a "malicious" proof makes sense, but I don't see at all why an AI generated proof necessarily meets that definition.

Reply on news.ycombinator.com