README

本资料通过大量的代码示例，详细介绍了既可作为编程语言又可作为定理证明辅助系统的 Lean 语言，以及其主要的库的使用方法。

[!WARNING] 本书目前仍在开发中，各页面的 URL 可能会随时更改，且可能不会设置重定向。

CONTRIBUTING

欢迎指出错误。请在此 GitHub 仓库中创建 issue。我们仅接受用于修正错误的 Pull Request，其他类型的 Pull Request 将不予受理。

您想翻译这本书吗？

感谢您对翻译本书的兴趣！😄 但请注意，由于本书仍在开发中，目前不接受其翻译工作！相关内容尚未稳定。

引用方式

如果您在您的作品中使用了本书，请按以下方式注明出处：

@misc{leanbyexample,
  title = {Lean by {E}xample},
  url = {https://lean-ja.github.io/lean-by-example/},
  author = {Asei Inoue},
  note = {Accessed on Month Day, Year},
}

许可证

本文档在CC BY-NC-SA 4.0 许可证]的约束下发布。

プライバシーポリシー

在本网站中，我们使用 Google Analytics 來分析用户的访问情况。Google Analytics 会通过 Cookie 收集用户使用本网站的信息，但这些信息均为匿名处理，不会收集可用于识别个人身份的资料。 如需了解本网站使用 Google Analytics 的详细信息，请访问以下 Google 官方页面：

• Google Analytics 使用条款

謝辞

感谢为该仓库制作了 SNS 卡以及 lean-ja 徽标的 @aconite 先生/女士]。

スポンサー

该项目得到了 Proxima Technology 的支持。

Proxima Technology（プロキシマテクノロジー）是一家致力于实现数学在社会中的应用的 AI 初创企业，其目标之一便是推动模型预测控制的普及。该企业将运用数理科学的力量来改变社会视为自身的使命。