diff --git a/CONTRIBUTING.md b/CONTRIBUTING.md
new file mode 100644
index 0000000..5afb857
--- /dev/null
+++ b/CONTRIBUTING.md
@@ -0,0 +1,7 @@
+## Contribution Guidelines
+Follow Lean's [Commit Convention](https://github.com/leanprover/lean4/blob/master/doc/dev/commit_convention.md).
+
+For more information see the [PR Submission](https://github.com/leanprover/lean4/blob/master/CONTRIBUTING.md#pr-submission) section in lean4's CONTRIBUTING.md.
+
+Note this key detail:
+> Follow the commit convention: Pull requests are squash merged, and the commit message is taken from the pull request title and body, so make sure they adhere to the commit convention. Put questions and extra information, which should not be part of the final commit message, into a first comment rather than the Pull Request description. Because the change will be squashed, there is no need to polish the commit messages and history on the branch.