May 25, 2026
Don't LEAN On Me
Arka Dash, Yatharth Maheshwari, Carlos José Duarte Casillas, Aditya Bansal, Rishab Kumar Jha
Don't LEAN On Me reproduces a cross-module soundness break on Lean v4.30.0-rc2 in which a malicious dependency uses `@[implemented_by]` and `native_decide` to hand a downstream consumer a kernel-certified theorem that contradicts the kernel's own reduction of the same term, while `#print axioms`, `lake build`, and source review all return clean. The mechanism is documented and tracked as P-low by the Lean team; the contribution is reframing it as a supply-chain attack on the "Lean-as-AI-safety-trust-anchor" architectures recently proposed in MA-LoT, AlphaProof, and the Lean-Agent Protocol, where the population consuming proofs is shifting away from the experts who can decode the one signal the audit surface emits. We provide a four-module worked exploit (BLUE/RED toy payload, no real harm), an audit-surface analysis showing every standard consumer-side check returns benign, and three concrete upstream mitigations centered on making attribute-driven trust admissions legible in `#print axioms`.
No reviews are available yet
Cite this work
@misc {
title={
(HckPrj) Don't LEAN On Me
},
author={
Arka Dash, Yatharth Maheshwari, Carlos José Duarte Casillas, Aditya Bansal, Rishab Kumar Jha
},
date={
5/25/26
},
organization={Apart Research},
note={Research submission to the research sprint hosted by Apart.},
howpublished={https://apartresearch.com}
}


