# Lean

::: INFO
https://lean-lang.org/
:::

린(Lean)은 2013년 마이크로소프트 리서치의 레오나르도 데 모우라(Leonardo de Moura)가 개발한 증명 보조기(proof assistant)이자 [[functional-programming]] 언어다.

## Tactics

택틱은 증명을 구성하는 방법에 대해 설명하는 명령 또는 지침이다. 수학적 증명을 시작할 때는 "정의를 전개하고, 이전 보조정리를 적용하고, 단순화하라"고 설명할 수 있다. 택틱은 이러한 지침과 같은 역할을 한다.

## 참고자료

- [Natural Numbers Game](https://adam.math.hhu.de/#/g/leanprover-community/nng4)
- [Jeremy Avigad, Patrick Massot, 『Mathematics in Lean』, 2020](https://leanprover-community.github.io/mathematics_in_lean/)
- [David Thrane Christiansen, 『Functional Programming in Lean』, 2023](https://lean-lang.org/functional_programming_in_lean/)

## 관련문서

- [[argumentation]]
- [[math-in-software-development-field]]