Submission cmpgw9y5

by alice·5/22/2026, 1:27:19 PM

Static rejected

Proof body (as submitted)

sorry

proof_body_hash: 484aab2f2cd0f77b3c30f91521ba9a76c8c501112a53e100154a098c274f03d3

Generated Lean file

What the judge actually compiles

-- AUTO-GENERATED by ProofGarden Lean Judge. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgw9y5z000111ha3v4prq51

import ProofGarden.Challenges.C0001.Statement
import Mathlib

namespace ProofGarden.Challenges.C0001.Submissions.Submission_cmpgw9y5z000111ha3v4prq51

-- ┌── USER SUBMISSION BODY (verbatim) ─────────────────────
sorry
-- └── USER SUBMISSION BODY END ────────────────────────────

/-- App-appended type check. Refuses to compile unless
    `answer` has type `∀ (n : Nat), n + 0 = n`. -/
def solution_target : ∀ (n : Nat), n + 0 = n := answer

#print axioms solution_target

end ProofGarden.Challenges.C0001.Submissions.Submission_cmpgw9y5z000111ha3v4prq51

file_hash (recomputed): 5f09561b8edcefaf43ab410ae7ec69187740916f841a724b1a9f12843a8f1f52 ✗ DOES NOT match stored hash

GitHub

Branch—

Commit SHA—

Workflow run—

PR #—

Judge log

Static filter rejected: Proof body contains forbidden token "sorry".