For ordinary proof issues, open an issue with the affected Lean declaration, the command used to reproduce the result, and a fresh #print axioms output.

For a report that should not initially be public, use GitHub's private vulnerability-reporting feature for the repository. Do not include private credentials, unpublished third-party data, or copyrighted paper copies in a report.

Soundness reports involving vacuous hypotheses, false finite certificates, stale object files, or unexpected axioms are treated as high priority.