Skip to content
Apart Research
Apart Research
Contact us
Sprint projectMay 25, 2026Bengaluru, India

sorryaudit: Transitive Sorry Taint Detection for AI-Assisted Lean 4 Proofs

Anshuman Singh · Team sorryaudit

Submitted to The Secure Program Synthesis Hackathon. Sprint projects are early-stage work by participants, not Apart Research publications.

Read the report

Report: sorryaudit: Transitive Sorry Taint Detection for AI-Assisted Lean 4 Proofs

Open in a new tab (opens in new tab)
Code (opens in new tab)
Share

AI proof assistants (Lean Copilot, LLMs) routinely use `sorry` as a placeholder for proof steps they cannot complete. The file compiles clean, CI passes, and the "formally verified" label gets attached. The problem is transitive: if theorem B depends on theorem A, and A uses sorry anywhere in its proof chain, B is also unsound - but Lean only warns at the point of sorry, not at every downstream dependent.

sorryaudit runs two passes on any Lean 4 codebase. First, a syntactic pass that detects sorry/admit/native_decide/Unsafe.cast by line, stripping comments and string literals to avoid false positives. Second, a semantic pass that runs Lean's own `#print axioms` command on every theorem and checks whether sorryAx appears in the transitive axiom set. Both passes merge into a per-theorem trustworthiness report with an overall project score.

Tested on lean-tcb (117 theorems, 23 files): correctly identified sorryThm (1+1=3) as the only UNSOUND theorem, with 115 trusted. On AI-generated proofs, caught a theorem with no sorry in its own body that was silently unsound due to a dependency - a case the syntactic pass alone misses entirely.

Reviews

Judging this Sprint?

Review this project

Your public critique appears on this page without your name. Your private critique is not published; only the Apart team reads it. If you agree below, we share your review with grantmaking.ai (opens in new tab) and the Transformative AI Fund so strong projects can be funded.

Not shown on this page.

Shown on this page, without your name.

Only the Apart team reads this, and funders if you agree below.

Share my name publicly on grantmaking.ai *
Share my private critique with funders *

How much would this matter for AI safety if it worked? How innovative is it? For scores of 4-5: is this actually new to the field, or replicating recent work?

Scoring guide
  1. 1Negligible. No clear problem addressed, or no meaningful novelty.
  2. 2Limited. Addresses a real problem but with a generic or well-trodden approach. Incremental at best.
  3. 3Moderate. Clear problem with a reasonable approach; some novelty in framing or method beyond routine application of existing tools.
  4. 4Significant. Important problem with an original approach, or identifies a neglected problem area. A valuable contribution others could build on.
  5. 5Exceptional. Tackles a critical AI safety problem with a genuinely novel approach, or opens a new research direction. Clear theory of change. You'd be excited to share this with researchers in the area.

How sound are methodology, implementation, and findings?

Scoring guide
  1. 1Seriously flawed. Methodology broken, results uninterpretable, or implementation doesn't work.
  2. 2Weak. Approach has significant gaps: missing validation, flawed experimental design, or incomplete implementation.
  3. 3Competent. Technically solid given the short duration. Methodology makes sense, results are interpretable, limitations acknowledged, work builds toward clear conclusions.
  4. 4Strong. Thorough methodology with convincing validation. Results clearly support conclusions. Immediately useful for future work.
  5. 5Exceptional. Ambitious scope executed rigorously. Surprising findings, novel methods, or unusually robust validation.

How clearly are work, findings, and impact potential communicated?

Scoring guide
  1. 1Incomprehensible. Cannot determine what the project is actually claiming or doing.
  2. 2Hard to follow. Key information buried, missing, or diluted by excessive length. Significant effort to extract main points.
  3. 3Clear enough. Can understand the problem, approach, and results without undue effort. Core content clearly present: problem, method, findings, limitations.
  4. 4Well presented. Easy to follow, well-structured, appropriate level of detail. Target audience would get it quickly.
  5. 5Exceptionally clear. A pleasure to read. Complex ideas made accessible. Could serve as a model for how to present this type of work.

  1. Detecting cheating is a critical challenge in model training. This work identifies cheating by syntactically flagging problematic keywords and semantically tracking dependencies to catch lemmas that rely on incomplete proofs. Although the approach incorporates a semantic pass to improve reliability, it still relies on syntactic matching. Integrating a tool like LeanREPL would enable more robust analysis of Lean code and facilitate the detection of a wider variety of cheating strategies."

  2. sorryaudit is a working Python tool that pairs a syntactic scan for sorry, admit, native_decide, and Unsafe.cast with a semantic pass over Lean's #print axioms output, then aggregates the results into a per-theorem trust report. The artifact runs end-to-end, the repository layout is understandable, and the demo correctly surfaces the load-bearing case: a theorem that appears clean at the source level but is unsound through a transitive dependency. That is a meaningful workflow contribution.

    To strengthen the work, please consider the following:

    1. Tighten the novelty framing. Lean 4's #print axioms already supports auditing the axiom dependencies of declarations, including detecting dependence on sorryAx. The contribution here is automation, project-scale surfacing, and presentation — not a new soundness primitive. Revising the framing to credit the existing Lean mechanism and positioning sorryaudit explicitly as the workflow layer on top would make the claim more defensible.

    2. Strengthen validation beyond a planted canary. The lean-tcb example is useful, but the deliberately unsound theorem is designed to be caught by soundness-checking workflows. A more convincing evaluation would run on mathlib4 or a comparably large real-world Lean 4 project, and on an actual corpus of AI-generated proofs, such as Lean Copilot output or LLM-generated lemmas, since AI-assisted proofs are the stated motivation.

    3. Deepen the evaluation set. The current evaluation appears too small to support broad generalization claims. Adding precision and recall against a planted-fault corpus, plus false-positive rates on known-clean projects, would make the results more convincing.

    4. Clarify the trust-score model. The project reports an overall project score, but the scoring policy would be stronger if the raw signals, weighting logic, and aggregation behavior were clearly documented. This would let downstream users decide whether to treat sorryAx, native_decide, unsafe constructs, and non-standard axioms as hard failures, warnings, or policy-specific risks.

    5. Reconcile the headline number across artifacts. The project page and repository appear to report slightly different trusted/unsound/suspect counts for the same lean-tcb evaluation. The qualitative finding survives, but a single reproducible headline figure pinned to one command would improve reader trust.

    6. Improve repository hygiene. Adding an OSI license, a small test suite covering the comment/string stripper and the #print axioms parser, and a pyproject.toml or pinned requirements file would meaningfully improve credibility and reproducibility.

    Overall, this is solid hackathon work with a correct diagnosis and a usable artifact. With tighter framing, evaluation on AI-generated proofs at larger scale, clearer scoring semantics, and minimal repository hygiene improvements, the project could move meaningfully above solid hackathon quality.

    Read full reviewShow less

Cite this project

@misc{singh2026sorryaudit,
  title = {{sorryaudit: Transitive Sorry Taint Detection for AI-Assisted Lean 4 Proofs}},
  author = {Anshuman Singh},
  year = {2026},
  month = may,
  note = {Submitted to The Secure Program Synthesis Hackathon, an Apart Research Sprint},
  howpublished = {\url{https://apartresearch.com/sprints/projects/sorryaudit-transitive-sorry-taint-detection-for-aiassisted-lean-4-proofs-k8gp}},
  url = {https://apartresearch.com/sprints/projects/sorryaudit-transitive-sorry-taint-detection-for-aiassisted-lean-4-proofs-k8gp}
}

More from The Secure Program Synthesis Hackathon

All 61 entriesBrowse all projects

Build something like this at the next Sprint

AI Collusion Research Sprint · Oct 23 - 25, 2026