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 check submissions with the accepted version above.

2. Check with Comparator.

We highly encourage using Lean Comparator. Keep the agreed statement in Challenge.lean and the proof in a separate Solution.lean. Configure Comparator to check every target theorem, using the pinned NLA setup above, 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. Ask AI to help you verify a proof.

Share your mathematical statement and proof with the AI, then use this prompt to ask for help verifying them in Lean:

Show the copyable AI prompt 
Help me verify my proof in Lean 4.33.1, with compatible, pinned dependencies. Ask for the statement and proof if you do not have them, and guide me through the process as someone new to Lean.

1. First write down every numerical claim, assumption, domain, dimension, constant and conclusion. Compare these with the source and wait for my agreement before proving them. Preserve the full intended result.

2. Study relevant existing Lean proofs for useful structure, definitions and lemmas. Reuse suitable work with attribution.

3. Use LeanCert for numerical bounds where appropriate, selecting kernel checking with leancert (trust := kernel).

4. Minimise computation before running interval arithmetic: simplify algebraically, exploit symmetry and monotonicity, and reduce precision and subdivisions where justified. Use tight intervals with proved coverage; never shrink the claimed domain to make a proof pass.

5. Apply the Tau Ceti referee rubrics in proportion to this project. Use multiple independent referees for statement fidelity, proof correctness and clarity; resolve their findings and identify any AI reviews as such.

6. Use Lean Comparator to check every final theorem against a separately reviewed Challenge.lean, with proofs in Solution.lean that do not import Challenge. Permit only propext, Classical.choice and Quot.sound (or a subset). No sorry, unproved custom axioms or native-execution trust may support the solution. Include #print axioms reports and the actual checking commands and output; never claim a check ran when it did not.

7. Add formalization.yaml following its published standard. Record sources, authors, versions and exactly what was verified, distinguishing supporting lemmas from the complete result.

References: LeanCert · Tau Ceti referee rubrics · formalization.yaml.

Share the proof at a fixed revision, its versions and checking logs, and the scope actually verified. Follow the original project’s formal-verification requirements for claims about an NLA problem. Run unfamiliar proof projects only in an organiser-vetted isolated environment without private credentials.