[loefflerd]

At present the "axiom audit" checker relies on parsing the Lean source to find the names of declarations to test. There are two separate issues with this:

1. the parser does not recognise section with modifiers (@[expose], noncomputable, etc); it ignores these section openings and hence misidentifies the corresponding end as closing the containing scope instead. If this is a namespace block, the result is that it records incorrect full names for subsequent declarations, and the axiom lookup for these fails.
2. In code using Lean's new module system, lemmas are private unless explicitly marked public. The axiom-audit parser does not realise this and attempts to look up these private names in a context where they aren't visible, again resulting in failures.

This PR fixes both problems by dropping the the source-code scan for declaration names and instead reading these from the compiled module metadata (as is already done by the option-manipulation audit). This should be more robust.

Update: the first version failed in CI because of helpers generated for structures with deriving Repr; I have adjusted it to screen out definitions marked as unsafe, with a regression test to check these are not used as back-doors to theorem proofs.

[github-actions]

Proof profile (new / modified Lean files)

No added or modified Lean files under LeanPool/ in this PR. No compile-cost measurements are needed.

Advisory only — never blocks merge.

[greptile-apps]

Advisory cross-file review against Lean Pool's supervisory rubric. This is not by itself a significance, source-verification, or merge verdict.

[Medium impact] The reviewed changes appear safe to merge; no new actionable defect was found.

Summary

The PR replaces source-name parsing with an audit of compiled Lean declarations.

• The axiom audit checks declarations from Lean’s compiled modules.

_{Reviews (3) · Last reviewed commit: "filter out unsafe defs (`deriving Repr` ..." · Reviewed by Greptile}