Lean 4 · Verification guide

From formal statement
to verified proof.

Each problem has a Lean 4 section for its formal statement, source files, submitted proofs and verification results. This guide explains how to contribute and check them.

Lean 4.19.0 · StdVerifier not configured · proofs can be saved

From statement to proof

01Attach the formalization. A problem can include a complete Lean source file and a link to its upstream version. Mathlib source can be displayed here too.
02Set the target. Supply a self-contained proposition supported by the current verifier. The target is copied into each proof submission so its meaning cannot silently change.
03Submit and verify. Add a proof under Submit progress and save it. In the problem’s Lean 4 section, choose “Verify with Lean 4.” The proof, result, diagnostics and environment are recorded together.

A minimal example

Demonstration only

import Std

-- A small demonstration theorem, not an open problem.
theorem add_zero_demo : ∀ n : Nat, n + 0 = n := by
  intro n
  rfl

The target field contains ∀ n : Nat, n + 0 = n. The proof field contains only the by block. This example exercises the verifier; it does not claim progress on an open problem.

What “verified” means

The pinned Lean compiler accepted a proof of the saved proposition, with a complete axiom report. The allowed foundational axioms are propext, Classical.choice and Quot.sound. A proof using sorry, extra axioms or native evaluation cannot earn this status.

A verified proof establishes the formal target. Editors still assess whether that target faithfully represents the original question and whether the submission resolves it. Verification never automatically changes a problem to “solved.”

Current proof profile

Start with by on its own line. Supported tactics: intro, intros, exact, apply, refine, rw, simp, simp_all, dsimp, constructor, rfl, trivial, assumption, decide, omega, left and right. Indent branches with spaces and ·.

Use one tactic per line. Rewriting and simplification accept a list of lemma names such as rw [Nat.add_comm]. Custom imports, declarations, comments, strings, tactic combinators and executable metaprograms are outside this first profile. Mathlib dependencies require a separate pinned profile; attach those files for review in the meantime.

lean4-core-4.19.0-v1 · 20 seconds · 512 MB · 5 attempts / minute / account