feat: kernel-grounded sorry/axiom auditor (lake exe atlas_audit) + first CI

[mvanhorn]

Summary

ATLAS now has a kernel-grounded way to tell which of its 46,203 declarations are actually proved. lake exe atlas_audit walks each Atlas declaration's transitive axiom dependencies and classifies it as proved (benign axioms only), sorry (reaches sorryAx), or other-axiom, then writes audit/proved.json plus a per-book summary. This PR also adds the repo's first GitHub Actions workflow.

Why this matters

Each book's report.json carries a proof_integrity score, but that score is produced by an LLM judge, not the Lean kernel. There is currently no in-repo way to ask the kernel which declarations are genuinely proved:

• 3,579 sorrys live across 874 files inside the default-built Atlas library, with no machine-checkable boundary. The Unproved lean_lib declared in lakefile.toml has no source files yet, so proved and unproved declarations are interleaved in the same target.
• atlas_audit reuses the same Lean.collectAxioms traversal that #print axioms uses, so its verdict is ground truth, and it surfaces any declaration whose axiom set is neither benign (propext, Classical.choice, Quot.sound) nor sorryAx for review.
• Comparable Lean libraries already expose this signal: dwrensha/compfiles carries a per-problem proved flag and google-deepmind/formal-conjectures emits hasSorryFreeProof. ATLAS had neither, and no CI to verify the library builds against the pinned Mathlib.

Demo

Simulated Demo. A real full-corpus run builds ~484K lines of Lean, so the figures shown here are ATLAS's own published statistics used illustratively; the classifier logic itself is covered by the fixture test below.

Changes

• Audit/Audit.lean is the auditor. It imports only Lean, so lake build atlas_audit compiles without building Mathlib or Atlas; the library is loaded at runtime via withImportModules and walked module-by-module, restricted to Atlas.* modules.
• Audit/Test.lean is a self-contained fixture that asserts the classifier labels a genuinely-proved theorem and a sorry-backed one correctly. It runs without building the corpus.
• .github/workflows/audit.yml adds CI as two jobs: a fast classifier-test (runs the fixture on every PR, no Mathlib build) and audit (Mathlib from lake exe cache get, builds Atlas, runs the auditor, uploads proved.json).
• lakefile.toml declares the atlas_audit lean_exe.

Testing

• Audit/Audit.lean and Audit/Test.lean compile cleanly against the pinned leanprover/lean4:v4.29.0: no errors, no warnings, 80-char / 2-space style.
• The fixture passes: the proved theorem reaches no sorryAx; the sorry theorem does.
• The full-corpus lake exe atlas_audit run executes in the audit CI job and uploads the report.

AI was used for assistance.

[niketp03]

Hi Matt! Thanks for the PR, it is a good point and a feature we agree we should have, let me check on the implementation.

[mvanhorn]

Thanks @niketp03, glad it resonates, and no rush on my end. A couple of things that might help the review: lake exe atlas_audit runs standalone, and the CI job I added gates on it, so you can see the pass/fail shape without wiring anything up. Happy to adjust the output format or the sorry/axiom policy to whatever fits the repo best, just let me know if any part is worth reworking.