An Auditable Harness for AI-Assisted Lean Formalization: Pilot Logs from Finite Differential Privacy

Workflow claims about AI-assisted formal mathematics are hard to evaluate when prompts, raw outputs, compile traces, and theorem statements are not released together. We report a small reproducibility pilot that pairs a kernel-checked Lean 4 formalization of finite pure differential privacy with a 24-trial audit harness. The harness logs, for each attempt, the prompt SHA-256, the verbatim or status-tagged transcript, the extracted Lean file, the lake env lean compile log, an escape-hatch scan, and a statement/context audit that guards against the main compile-only failure mode of proving a weakened theorem under modified definitions. Across six finite-DP lemmas, two gpt-5-family models, and two trials per cell, 21 of 24 attempts compiled and 24 of 24 preserved their assigned theorem statement and local Lean context. We classify the three failures as one hallucinated lemma and two tactic-script errors. We frame this as harness design and audit methodology, not a model evaluation: the trial count is small, the tasks are likely contaminated by public Mathlib and DP textbooks, and only one model family is covered. The contribution is the reproducible logging schema and pipeline, and a worked instantiation that other AI-assisted formalization studies can adapt.