Guide to using Lean

1. Try a small proof

Open the Lean web playground and paste this example. It says that adding zero on the left leaves a natural number unchanged; no extra library is needed.

theorem zero_on_the_left (n : Nat) : 0 + n = n := by
  exact Nat.zero_add n

#print axioms zero_on_the_left

Read the editor’s messages. sorry marks an unfinished proof; #print axioms reports the assumptions a theorem depends on. The playground may run another Lean version, so record the version used for any submitted evidence.

2. Check with Comparator

Lean Comparator is recommended for formal verification. Keep the agreed statement in Challenge.lean and the proof in a separate Solution.lean. Configure Comparator to check every target theorem with the exact versions recorded in the submission, and save its output. It checks that the proof matches the formal statement, uses only permitted axioms, and is accepted by Lean’s kernel.

Someone must still compare the challenge with the original mathematics. For more detail, see Lean’s guide to validating proofs.

3. Record the evidence

Provide the proof at a fixed revision, its versions and checking logs, and the scope actually verified. Follow the AIM repository’s status and evidence guidance for claims about an AIM problem. Credit the source mathematics and any existing formalisation or checking work you use. Run unfamiliar proof projects only in an organiser-vetted isolated environment without private credentials.

Optional AI assistance

You can work through every step above without AI. If you choose to use an AI tool to help write Lean code, this optional prompt can help structure the work. Check its suggested statements, code and references, and describe any assistance and how you checked it. AI assurances are not verification; the same evidence requirements apply whatever tools you use.

Help me verify my proof in the exact Lean version and pinned dependencies recorded for this project. Ask for the statement and proof if you do not have them, and guide me through the process as someone new to Lean.

1. Write down every claim, assumption, domain, constant and conclusion. Compare these with the source and preserve the full intended result.
2. Reuse relevant existing Lean proofs with attribution.
3. Use kernel-checked tools for numerical bounds where appropriate; record versions and commands.
4. Use independent checks for statement fidelity, proof correctness and clarity, and identify AI reviews as such.
5. Use Lean Comparator against a separately reviewed Challenge.lean, with proofs in Solution.lean. Permit only propext, Classical.choice and Quot.sound (or a subset). No sorry, unproved custom axioms or native-execution trust may support the solution.
6. Include #print axioms reports, actual checking commands and output, and formalization.yaml. State exactly what was verified and what was not.