Lean theorem challenges · auto-checked on GitHub Actions

Submit a Lean proof. The judge runs the real compiler.

You write only the body inside by .... The platform generates the surrounding Lean file from a fixed template, pushes it to a public judge repository, and lets GitHub Actions type-check it with a pinned lean-toolchain. Accepted submissions earn Seeds — reputation only.

See challenges →How the judge works

Seeds are non-monetary reputation points — no cash, no token, no transfer, no redemption.

-- AUTO-GENERATED by ProofGarden. Do not edit by hand.
-- Challenge: C0001

import ProofGarden.Challenges.C0001.Statement

namespace ProofGarden.Challenges.C0001

theorem solution (n : Nat) : n + 0 = n := by
  exact Nat.add_zero n        -- ← your submission

#print axioms solution

end ProofGarden.Challenges.C0001

Published challenges

Total submissions

Accepted

How it works

From proof body to verified type-check

You submit a proof body

Only the tactic block. No imports, no namespaces, no theorem header — those are fixed by the challenge.

Static filter rejects obvious cheats

A first-pass check forbids sorry, admit, axiom, def, theorem, #eval, native_decide and other tokens that don't belong in a tactic block.

Lean file is auto-generated

The app produces Submission_<id>.lean from the challenge template + your proof body, hashes it, and stores the hash for audit.

Pushed to a new branch

The file is committed to submission/<id> in the public judge repository. The app never touches main.

GitHub Actions runs lake build

A pinned lean-toolchain ensures the same compiler runs every time. The workflow is the source of truth — the web server never executes Lean.

Seeds awarded once

If — and only if — the workflow conclusion is success on the recorded commit SHA, the submission becomes Accepted and Seeds are credited via an append-only ledger.