You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
{{ message }}
This repository was archived by the owner on Jan 5, 2025. It is now read-only.
Thecoretypetheoryisimplementedinaminimal {tech}[kernel] that does nothing other than check proof terms.
35
47
This core theory and kernel are supported by advanced automation, realized in {ref "tactics"}[an expressive tactic language].
36
48
Each tactic produces a term in the core type theory that is checked by the kernel, so bugs in tactics do not threaten the soundness of Lean as a whole.
37
49
Along with many other parts of Lean, the tactic language is user-extensible, so it can be built up to meet the needs of a given formalization project.
38
50
Tactics are written in Lean itself, and can be used immediately upon definition; rebuilding the prover or loading external modules is not required.
Lean is also a pure *functional programming language*, with features such as a run-time system based on reference counting that can efficiently work with packed array structures, multi-threading, and monadic {name}`IO`.
41
57
As befits a programming language, Lean is primarily implemented in itself, including the language server, build tool, {tech}[elaborator], and tactic system.
42
58
This very book is written in [Verso](https://github.com/leanprover/verso), a documentation authoring tool written in Lean.
Familiarity with Lean's programming features is valuable even for users whose primary interest is in writing proofs, because Lean programs are used to implement new tactics and proof automation.
45
65
Thus, this reference manual does not draw a barrier between the two aspects, but rather describes them together so they can shed light on one another.
Leonardo de Moura launched the Lean project when he was at Microsoft Research in2013, and Lean 0.1 was officially released on June 16, 2014.
50
78
The goal of the Lean project is to combine the high level of trust provided by a small, independently-implementable logical kernel with the convenience and automation of tools like SMT solvers, while scaling to large problems.
51
79
This vision still guides the development of Lean, as we invest in improved automation, improved performance, and user-friendliness; the trusted core proof checker is still minimal and independent implementations exist.
80
+
:::
52
81
82
+
Leonardo de Moura は2013年に Microsoft Research 在籍時に Lean プロジェクトを立ち上げ、2014年6月16日に Lean 0.1 が正式にリリースされました。Lean プロジェクトの目標は、独立に実装可能な小さな論理カーネル提供する高い信頼性と、SMTソルバのようなツールの利便性と自動化を組み合わせ、同時に大規模な問題にも対応できるようにすることです。このビジョンは現在も Lean の開発の指針となっており、自動化の改善・性能の向上・使いやすさの向上に投資されています；信頼されたコアな証明チェッカもまた最小限で、独立な実装が存在します。
83
+
84
+
:::comment
53
85
The initial versions of Lean were primarily configured as C++ libraries in which client code could carry out trustworthy proofs that were independently checkable.
54
86
In these early years, the design of Lean rapidly evolved towards traditional interactive provers, first with tactics written in Lua, and later with a dedicated front-end syntax.
55
87
January 20, 2017 saw the first release of the Lean 3.0 series.
56
88
Lean 3 achieved widespread adoption by mathematicians, and pioneered self-extensibility: tactics, notations, and top-level commands could all be defined in Lean itself.
57
89
The mathematics community built Mathlib, which at the end of Lean 3 had over one million lines of formalized mathematics, with all proofs mechanically checked.
58
90
The system itself, however, was still implemented in C++, which imposed limits on Lean's flexibility and made it more difficult to develop due to the diverse skills required.
Development of Lean 4 began in2018, culminating in the 4.0 release on September 8, 2023.
61
97
Lean 4 represents an important milestone: as of version 4, Lean is self-hosted - approximately 90% of the code that implements Lean is itself written in Lean.
62
98
Lean 4's rich extension API provides users with the ability to adapt it to their needs, rather than relying on the core developers to add necessary features.
63
99
Additionally, self-hosting makes the development process much faster, so features and performance can be delivered more quickly; Lean 4 is faster and scales to larger problems than Lean 3.
64
100
Mathlib was successfully ported to Lean 4in2023 through a community effort supported by the Lean developers, and it has now grown to over 1.5 million lines
65
101
Even though Mathlib has grown by50%, Lean 4 checks it faster than Lean 3 could check its smaller library.
66
102
The development process for Lean 4 was approximately as long as that of all prior versions combined, and we are now delighted with its design—no further rewrites are planned.
Leonardo de Moura and his co-founder, Sebastian Ullrich, launched the Lean Focused Research Organization (FRO) nonprofit in July of 2023 within Convergent Research, with philanthropic support from the Simons Foundation International, the Alfred P. Sloan Foundation, and Richard Merkin.
69
109
The FRO currently has more than ten employees working to support the growth and scalability of Lean and the broader Lean community.
110
+
:::
70
111
112
+
Leonardo de Moura と彼の共同設立者である Sebastian Ullrich は2023年7月、Simons Foundation International・Alfred P. Sloan Foundation・Richard Merkin からの後援を受けて、非営利団体 Lean Focused Research Organization (FRO) を Convergent Research 内に立ち上げました。FRO は現在10人以上の従業員を擁し、Lean やより広範な Lean コミュニティの成長とスケーラビリティの支援に取り組んでいます。
71
113
114
+
:::comment
72
115
# Typographical Conventions
116
+
:::
117
+
118
+
# 表記ルール
73
119
120
+
:::comment
74
121
This document makes use of a number of typographical and layout conventions to indicate various aspects of the information being presented.
122
+
:::
123
+
124
+
本書では提示される情報のさまざまな側面を示すために、多くの表記やレイアウトの慣例を用いています。
75
125
126
+
:::comment
76
127
## Lean Code
128
+
:::
129
+
130
+
## Lean のコード
77
131
132
+
:::comment
78
133
This document contains many Lean code examples.
79
134
They are formatted as follows:
135
+
:::
136
+
137
+
本書には多くの Lean コードの例が含まれています。これらは次のような形式になっています：
80
138
81
139
````lean
82
140
defhello : IO Unit := IO.println "Hello, world!"
83
141
````
84
142
143
+
:::comment
85
144
Compiler output (which may be errors, warnings, or just information) is shown both in the code and separately:
@@ -115,57 +192,109 @@ but is expected to have type
115
192
```
116
193
117
194
195
+
:::comment
118
196
The presence of tactic proof states is indicated by the presence of small lozenges that can be clicked to show the proof state, such as after {tactic}`rfl` below:
0 commit comments