> 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.