贡献指南
欢迎各种形式的贡献，无论你是对 Lean 感兴趣的初学者，有经验的数学爱好者，程序开发者，或者其他任何对形式化证明感兴趣的朋友。
- 数学形式化方面，可以参与 Lean 教材和文档的翻译，分享个人学习笔记和心得，编写入门教程或示例等等。
- 如果你更偏向编程技术，可以参与编写 Lean 项目教程，从学习别人项目开始，到逐步开发自己项目，从发现项目的不足，再到参与代码贡献等等。
目前 Lean 社区值得实践了解的项目非常多，包括交互式工具、证明分析、集成外部工具、在线 Lean 服务等等。
在项目开发方面，这里提供了一个参考示例，演示从项目创建，管理依赖，到编写元策略，Lean 终端交互，再到测试自动化和发布的过程。
除了直接与 Lean 相关的贡献，也可以帮助优化基础设置，比如优化 Markdown book 的中文搜索，完善仓库的 i18n-next 自动化等。
希望通过开源协作，共同学习与进步！