Reasons for making this change:

Add .gitignore for repositories using the Lean formal proof verification system.

Links to documentation supporting these rule changes:

The ignore file patterns are extracted by examining the following well-known Lean projects and only the patterns that are general are added:

• https://github.com/leanprover-community/tutorials
• https://github.com/leanprover-community/mathlib
• https://github.com/leanprover-community/lean-perfectoid-spaces
• https://github.com/mpedramfar/Lean-game-maker

Also, the logic in the following well-known Lean related tools is also examined:

• https://github.com/leanprover-community/lean/tree/master/leanpkg
• https://github.com/leanprover-community/mathlib-tools
• https://github.com/leanprover-community/format_lean

If this is a new template:

• Link to application or project’s homepage:
• Community-maintained Lean 3 (active): https://leanprover-community.github.io/
• Official Lean 3 (archived): https://leanprover.github.io/