[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}

[Vilin97]

Reviewed all six complete changed files at e9e4f76, including the compiled audit fixture and parser/cache changes. Compiled enumeration addresses generated names and visibility while private dependencies remain in the transitive axiom check. The pinned Lean import defaults and narrow axiom-cache initialization support the no-project-initializer boundary. Output validation and failing subprocess exits fail closed. Unsafe independent roots are excluded, with a rejected-safe-proof fixture and the existing all-declaration backdoor audit retained. I found no isolated-head soundness defect from static review.

Replacing declaration discovery and adding a required workflow fixture changes protected gates, so this needs direct scoped authorization under the repository rules. When composing with #712, retain both fixture suites and update its exact-selector assertion; the extended selector currently breaks that assertion despite selecting the proof-plugin tests. I have not executed the compiler fixtures or qualified hosted CI. No queue or auto-merge was enabled.