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 Leanforces. Do not edit by hand.
-- Challenge: C0001
-- Submission: cmpgw9y5z000111ha3v4prq51

import Leanforces.Challenges.C0001.Statement
import Mathlib

namespace Leanforces.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 Leanforces.Challenges.C0001.Submissions.Submission_cmpgw9y5z000111ha3v4prq51

file_hash (recomputed): a754d7defa051c1bc3e9c15a73042564070c201388ca3776ab590b57d896ba1f ✗ DOES NOT match stored hash

GitHub

Branch—

Commit SHA—

Workflow run—

PR #—

Judge log

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