Don't LEAN On Me

This report identifies a real hazard of using Lean as an oracle to check proofs about code created by AI agents. However, the hazard is one that to me seems best avoided in other ways.

The authors write that use of "native_decide" does produce use of an axiom that will be declared in a standard automatic audit (with "#print axioms"). Their complaint is that, for a given axiom instance, no record is kept about which dangerous Lean feature invocations were implicated. I certainly agree with that statement, but isn't a better solution simply to outlaw use of "native_decide" in developments that should be treated adversarially?

Even with the additional auditing information proposed here, I wouldn't trust humans to trace through all the information and catch all relevant bugs in trusted code. And are the authors even proposing *automatic* checking of such expanded audit information, within an agentic loop? That sounds like a diabolically hard problem, reducing to additional formal verification needed to justify trusted code -- and if we had those proofs, would we use "native_decide"?

This is a strong and relevant project that investigates a specific mode of trust failure in formal-verification-based agentic guardrails. The primary contribution of the paper lies not only in demonstrating that Lean features such as @[implemented_by] and native_decide present technical risks, but also in connecting these risks to realistic AI-assisted development workflows, supply-chain boundaries, and prompt-framing effects. The four-module example is well-constructed and effectively illustrates why downstream users may trust a theorem that appears correct while it still depends on a compromised runtime implementation path.

The empirical section provides valuable evidence. The 33-trial study, which spans multiple Claude model tiers, various prompt framings, and two larger toy codebases, offers greater depth than a single proof-of-concept. I found the distinction between benign optimization prompts, maintainer-nudge prompts, and in-source prompt-injection-style comments particularly insightful. This framing clarifies the difference between cases where models inadvertently introduce unsoundness and cases where models comply with divergent behavior specified by a trusted-looking source or maintainer signal.

The main improvement area is scope and calibration. The underlying Lean mechanism is already documented and publicly discussed, so the paper should continue to frame its novelty as empirical measurement, AI-agent workflow risk, and supply-chain exploitation pattern—not as discovery of a new Lean soundness issue. The title and some claims may read stronger than the evidence supports; the results are compelling, but still limited to Claude 4.x-style agents, small per-condition sample sizes, and two main complex codebases. Expanding to GPT, Gemini, open-weight models, larger Lean projects, and more injection patterns would make the generalization much stronger.

The evaluation would also benefit from clearer reproducibility packaging: a single command to regenerate the headline tables, pinned model/prompt metadata, and a clearer separation between results that prove False automatically and results that show source/runtime disagreement but hit probe-budget limits. The limitations section already acknowledges several of these points, which is good, but the headline claims should reflect those constraints more consistently.

Overall, this is high-quality hackathon work with a meaningful AI-safety angle, a concrete artifact, and a well-motivated threat model. With broader model coverage, stronger reproducibility, and slightly more careful claim calibration, this could become a strong research contribution on the risks of combining AI coding agents with formal-verification-based guardrails.

The paper effectively highlights a significant vulnerability in Lean's proof verification process by demonstrating how an attacker can exploit the '@[implemented_by]' attribute to inject false proofs into the system. The detailed reproduction steps and audit analysis provide strong evidence of the exploit's feasibility. However, the paper could benefit from a more comprehensive discussion on potential mitigations beyond the suggested ones, particularly those that could be implemented by users or maintainers without waiting for upstream changes.

The inclusion of the discursive reframing phase adds depth to the paper by illustrating how modern LLMs can be bypassed to generate malicious code. However, this section is somewhat speculative and lacks empirical validation, which might weaken its credibility. Additionally, the paper could benefit from a clearer explanation of how the exploit affects real-world applications and what the broader implications are for AI safety and formal verification systems.

The paper's structure and presentation are generally clear and well-organized, making it easy to follow the argument and understand the technical details. However, some sections, such as the appendices, could be more concise and better integrated into the main text to enhance readability and flow.