Class Lean project

In this project, we will write proofs in Lean and contribute them to a shared class repository. Lean checks each step of your proof. GitHub lets you keep your own copy of the project and submit your work for review. Start with one proof to learn the workflow, then continue with other theorems.

Getting started

1. Make a GitHub account. Visit GitHub and sign up if you do not already have an account.
2. Fork the project. Open jonathanwise/math2001_project and click Fork to create a copy under your own account.
3. Open a Codespace with your fork. On your fork's GitHub page, click Code, choose Codespaces, and create a Codespace. It opens a VS Code editor in your browser. See GitHub's Codespace instructions for help.
4. Verify the Lean setup. Wait for setup and downloads to finish. In VS Code's Extensions view, confirm that the Lean 4 extension is installed and enabled. Open zero_plus.lean and place your cursor on sorry. Check that the Lean Infoview shows the goal ⊢ ℕ.zero + n = n. This confirms that Lean and the extension are working together in the project. A warning about sorry is expected until you finish the proof.
5. Complete your first proof. Open zero_plus.lean and replace the unfinished proof with your own. Check that Lean reports no errors in your proof and that no sorry remains in it.
6. Commit and push your proof. Save the file. In VS Code's Source Control view, stage your changes, enter a commit message such as Prove zero_plus, and commit. Push the commit to your fork on GitHub.

7. Create a pull request. After pushing your proof, go to the class repository on GitHub. Click the Pull requests tab, then New pull request. On the comparison page, click compare across forks to show the repository selectors.

   Choose these settings (replace YOUR-USERNAME with your GitHub username):

   Selector	Choose
   base repository	jonathanwise/math2001_project (the class repository)
   base	main (the class branch receiving your proof)
   head repository / head fork	YOUR-USERNAME/math2001_project (your fork)
   compare	main if you worked on your fork's main branch; otherwise, choose the branch you committed and pushed your proof to.

   The base is the destination; the head/compare branch is the source of your changes. Review the diff below the selectors and confirm that it includes your proof. Click Create pull request, enter a title such as Prove zero_plus and a short description, then click Create pull request again to submit it to the class repository for review. See GitHub's pull request instructions for help.

8. Start another theorem. Choose another unfinished proof and follow the same workflow: complete it, check it with Lean, commit and push, then submit a pull request. Use the Lean reference for a quick reminder of proof commands and the Lean guide for explanations and worked examples. Do not contribute AI-generated code to the repository.