1. Top
  2. mathematics_in_lean
  3. Files
  4. html
  5. C01_Introduction.html
mathematics_in_lean

My solutions for this book

  1. 1
  2. 2
  3. 3
  4. 4
  5. 5
  6. 6
  7. 7
  8. 8
  9. 9
  10. 10
  11. 11
  12. 12
  13. 13
  14. 14
  15. 15
  16. 16
  17. 17
  18. 18
  19. 19
  20. 20
  21. 21
  22. 22
  23. 23
  24. 24
  25. 25
  26. 26
  27. 27
  28. 28
  29. 29
  30. 30
  31. 31
  32. 32
  33. 33
  34. 34
  35. 35
  36. 36
  37. 37
  38. 38
  39. 39
  40. 40
  41. 41
  42. 42
  43. 43
  44. 44
  45. 45
  46. 46
  47. 47
  48. 48
  49. 49
  50. 50
  51. 51
  52. 52
  53. 53
  54. 54
  55. 55
  56. 56
  57. 57
  58. 58
  59. 59
  60. 60
  61. 61
  62. 62
  63. 63
  64. 64
  65. 65
  66. 66
  67. 67
  68. 68
  69. 69
  70. 70
  71. 71
  72. 72
  73. 73
  74. 74
  75. 75
  76. 76
  77. 77
  78. 78
  79. 79
  80. 80
  81. 81
  82. 82
  83. 83
  84. 84
  85. 85
  86. 86
  87. 87
  88. 88
  89. 89
  90. 90
  91. 91
  92. 92
  93. 93
  94. 94
  95. 95
  96. 96
  97. 97
  98. 98
  99. 99
  100. 100
  101. 101
  102. 102
  103. 103
  104. 104
  105. 105
  106. 106
  107. 107
  108. 108
  109. 109
  110. 110
  111. 111
  112. 112
  113. 113
  114. 114
  115. 115
  116. 116
  117. 117
  118. 118
  119. 119
  120. 120
  121. 121
  122. 122
  123. 123
  124. 124
  125. 125
  126. 126
  127. 127
  128. 128
  129. 129
  130. 130
  131. 131
  132. 132
  133. 133
  134. 134
  135. 135
  136. 136
  137. 137
  138. 138
  139. 139
  140. 140
  141. 141
  142. 142
  143. 143
  144. 144
  145. 145
  146. 146
  147. 147
  148. 148
  149. 149
  150. 150
  151. 151
  152. 152
  153. 153
  154. 154
  155. 155
  156. 156
  157. 157
  158. 158
  159. 159
  160. 160
  161. 161
  162. 162
  163. 163
  164. 164
  165. 165
  166. 166
  167. 167
  168. 168
  169. 169
  170. 170
  171. 171
  172. 172
  173. 173
  174. 174
  175. 175
  176. 176
  177. 177
  178. 178
  179. 179
  180. 180
  181. 181
  182. 182
  183. 183
  184. 184
  185. 185
  186. 186
  187. 187
  188. 188
  189. 189
  190. 190
  191. 191
  192. 192
  193. 193
  194. 194
  195. 195
  196. 196
  197. 197
  198. 198
  199. 199
  200. 200
  201. 201
  202. 202
  203. 203
  204. 204
  205. 205
  206. 206
  207. 207
  208. 208
  209. 209
  210. 210
  211. 211
  212. 212
  213. 213
  214. 214
  215. 215
  216. 216
  217. 217
  218. 218
  219. 219
  220. 220
  221. 221
  222. 222
  223. 223
  224. 224
  225. 225
  226. 226
  227. 227
  228. 228
  229. 229
  230. 230
  231. 231
  232. 232
  233. 233
  234. 234
  235. 235
  236. 236
  237. 237
  238. 238
  239. 239
  240. 240
  241. 241
  242. 242
  243. 243
  244. 244
  245. 245
  246. 246
  247. 247
  248. 248
  249. 249
  250. 250
  251. 251
  252. 252
  253. 253
  254. 254
  255. 255
  256. 256
  257. 257
  258. 258
  259. 259
  260. 260
  261. 261
  262. 262
  263. 263
  264. 264
  265. 265
  266. 266
  267. 267
  268. 268
  269. 269
  270. 270
  271. 271
  272. 272
  273. 273
  274. 274
  275. 275
  276. 276
  277. 277
  278. 278
  279. 279
  280. 280
  281. 281
  282. 282
  283. 283
  284. 284
  285. 285
  286. 286
  287. 287
  288. 288
  289. 289
  290. 290
  291. 291
  292. 292
  293. 293
  294. 294
  295. 295
  296. 296
  297. 297
  298. 298
  299. 299
  300. 300
  301. 301
  302. 302
  303. 303
  304. 304
  305. 305
  306. 306
  307. 307
  308. 308
  309. 309
  310. 310
  311. 311
  312. 312
  313. 313
  314. 314
  315. 315
  316. 316
  317. 317
  318. 318
  319. 319
  320. 320
  321. 321
  322. 322
  323. 323
  324. 324
  325. 325
  326. 326
  327. 327
  328. 328
  329. 329
  330. 330
  331. 331
  332. 332
  333. 333
  334. 334
  335. 335
  336. 336
  337. 337
  338. 338
  339. 339
  340. 340
  341. 341
  342. 342
  343. 343
  344. 344
  345. 345
  346. 346
  347. 347
  348. 348
  349. 349
  350. 350
  351. 351
  352. 352
  353. 353
  354. 354
  355. 355
  356. 356
  357. 357
  358. 358
  359. 359
  360. 360
  361. 361
  362. 362
  363. 363
  364. 364
  365. 365
  366. 366
  367. 367
  368. 368
  369. 369
  370. 370
  371. 371
  372. 372
  373. 373
  374. 374
  375. 375
  376. 376
  377. 377
  378. 378
  379. 379
  380. 380
  381. 381
  382. 382
  383. 383
  384. 384
  385. 385
  386. 386
  387. 387
  388. 388
  389. 389
  390. 390
  391. 391
  392. 392
  393. 393
  394. 394
  395. 395
  396. 396
  397. 397
  398. 398
  399. 399
  400. 400
  401. 401
  402. 402
  403. 403
  404. 404
  405. 405 


<!DOCTYPE html>
<html class="writer-html5" lang="en" data-content_root="./">
<head>
  <meta charset="utf-8" /><meta name="viewport" content="width=device-width, initial-scale=1" />

  <meta name="viewport" content="width=device-width, initial-scale=1.0" />
  <title>1. Introduction &mdash; Mathematics in Lean v4.19.0 documentation</title>
      <link rel="stylesheet" type="text/css" href="_static/pygments.css?v=b86133f3" />
      <link rel="stylesheet" type="text/css" href="_static/css/theme.css?v=e59714d7" />
      <link rel="stylesheet" type="text/css" href="_static/css/custom.css?v=0731ccc3" />

  
    <link rel="shortcut icon" href="_static/favicon.ico"/>
      <script src="_static/jquery.js?v=5d32c60e"></script>
      <script src="_static/_sphinx_javascript_frameworks_compat.js?v=2cd50e6c"></script>
      <script src="_static/documentation_options.js?v=7048e04d"></script>
      <script src="_static/doctools.js?v=9bcbadda"></script>
      <script src="_static/sphinx_highlight.js?v=dc90522c"></script>
    <script src="_static/js/theme.js"></script>
    <link rel="index" title="Index" href="genindex.html" />
    <link rel="search" title="Search" href="search.html" />
    <link rel="next" title="2. Basics" href="C02_Basics.html" />
    <link rel="prev" title="Mathematics in Lean" href="index.html" /> 
</head>

<body class="wy-body-for-nav"> 
  <div class="wy-grid-for-nav">
    <nav data-toggle="wy-nav-shift" class="wy-nav-side">
      <div class="wy-side-scroll">
        <div class="wy-side-nav-search" >

          
          
          <a href="index.html" class="icon icon-home">
            Mathematics in Lean
          </a>
<div role="search">
  <form id="rtd-search-form" class="wy-form" action="search.html" method="get">
    <input type="text" name="q" placeholder="Search docs" aria-label="Search docs" />
    <input type="hidden" name="check_keywords" value="yes" />
    <input type="hidden" name="area" value="default" />
  </form>
</div>
        </div><div class="wy-menu wy-menu-vertical" data-spy="affix" role="navigation" aria-label="Navigation menu">
              <ul class="current">
<li class="toctree-l1 current"><a class="current reference internal" href="#">1. Introduction</a><ul>
<li class="toctree-l2"><a class="reference internal" href="#getting-started">1.1. Getting Started</a></li>
<li class="toctree-l2"><a class="reference internal" href="#overview">1.2. Overview</a></li>
</ul>
</li>
<li class="toctree-l1"><a class="reference internal" href="C02_Basics.html">2. Basics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C03_Logic.html">3. Logic</a></li>
<li class="toctree-l1"><a class="reference internal" href="C04_Sets_and_Functions.html">4. Sets and Functions</a></li>
<li class="toctree-l1"><a class="reference internal" href="C05_Elementary_Number_Theory.html">5. Elementary Number Theory</a></li>
<li class="toctree-l1"><a class="reference internal" href="C06_Discrete_Mathematics.html">6. Discrete Mathematics</a></li>
<li class="toctree-l1"><a class="reference internal" href="C07_Structures.html">7. Structures</a></li>
<li class="toctree-l1"><a class="reference internal" href="C08_Hierarchies.html">8. Hierarchies</a></li>
<li class="toctree-l1"><a class="reference internal" href="C09_Groups_and_Rings.html">9. Groups and Rings</a></li>
<li class="toctree-l1"><a class="reference internal" href="C10_Linear_Algebra.html">10. Linear algebra</a></li>
<li class="toctree-l1"><a class="reference internal" href="C11_Topology.html">11. Topology</a></li>
<li class="toctree-l1"><a class="reference internal" href="C12_Differential_Calculus.html">12. Differential Calculus</a></li>
<li class="toctree-l1"><a class="reference internal" href="C13_Integration_and_Measure_Theory.html">13. Integration and Measure Theory</a></li>
</ul>
<ul>
<li class="toctree-l1"><a class="reference internal" href="genindex.html">Index</a></li>
</ul>

        </div>
      </div>
    </nav>

    <section data-toggle="wy-nav-shift" class="wy-nav-content-wrap"><nav class="wy-nav-top" aria-label="Mobile navigation menu" >
          <i data-toggle="wy-nav-top" class="fa fa-bars"></i>
          <a href="index.html">Mathematics in Lean</a>
      </nav>

      <div class="wy-nav-content">
        <div class="rst-content">
          <div role="navigation" aria-label="Page navigation">
  <ul class="wy-breadcrumbs">
      <li><a href="index.html" class="icon icon-home" aria-label="Home"></a></li>
      <li class="breadcrumb-item active"><span class="section-number">1. </span>Introduction</li>
      <li class="wy-breadcrumbs-aside">
            <a href="_sources/C01_Introduction.rst.txt" rel="nofollow"> View page source</a>
      </li>
  </ul>
  <hr/>
</div>
          <div role="main" class="document" itemscope="itemscope" itemtype="http://schema.org/Article">
           <div itemprop="articleBody">
             
  <section id="introduction">
<span id="id1"></span><h1><span class="section-number">1. </span>Introduction<a class="headerlink" href="#introduction" title="Link to this heading">&#61633;</a></h1>
<section id="getting-started">
<h2><span class="section-number">1.1. </span>Getting Started<a class="headerlink" href="#getting-started" title="Link to this heading">&#61633;</a></h2>
<p>The goal of this book is to teach you to formalize mathematics using the
Lean 4 interactive proof assistant.
It assumes that you know some mathematics, but it does not require much.
Although we will cover examples ranging from number theory
to measure theory and analysis,
we will focus on elementary aspects of those fields,
in the hopes that if they are not familiar to you,
you can pick them up as you go.
We also don&#8217;t presuppose any background with formal methods.
Formalization can be seen as a kind of computer programming:
we will write mathematical definitions, theorems, and proofs in
a regimented language, like a programming language,
that Lean can understand.
In return, Lean provides feedback and information,
interprets expressions and guarantees that they are well-formed,
and ultimately certifies the correctness of our proofs.</p>
<p>You can learn more about Lean from the
<a class="reference external" href="https://leanprover.github.io">Lean project page</a>
and the
<a class="reference external" href="https://leanprover-community.github.io/">Lean community web pages</a>.
This tutorial is based on Lean&#8217;s large and ever-growing library, <em>Mathlib</em>.
We also strongly recommend joining the
<a class="reference external" href="https://leanprover.zulipchat.com/">Lean Zulip online chat group</a>
if you haven&#8217;t already.
You&#8217;ll find a lively and welcoming community of Lean enthusiasts there,
happy to answer questions and offer moral support.</p>
<p>Although you can read a pdf or html version of this book online,
it is designed to be read interactively,
running Lean from inside the VS Code editor.
To get started:</p>
<ol class="arabic simple">
<li><p>Install Lean 4 and VS Code following
these <a class="reference external" href="https://leanprover-community.github.io/get_started.html">installation instructions</a>.</p></li>
<li><p>Make sure you have <a class="reference external" href="https://git-scm.com/">git</a> installed.</p></li>
<li><p>Follow these <a class="reference external" href="https://leanprover-community.github.io/install/project.html#working-on-an-existing-project">instructions</a>
to fetch the <code class="docutils literal notranslate"><span class="pre">mathematics_in_lean</span></code> repository and open it up in VS Code.</p></li>
<li><p>Each section in this book has an associated Lean file with examples and exercises.
You can find them in the folder <code class="docutils literal notranslate"><span class="pre">MIL</span></code>, organized by chapter.
We strongly recommend making a copy of that folder and experimenting and doing the
exercises in that copy.
This leaves the originals intact, and it also makes it easier to update the repository as it changes (see below).
You can call the copy <code class="docutils literal notranslate"><span class="pre">my_files</span></code> or whatever you want and use it to create
your own Lean files as well.</p></li>
</ol>
<p>At that point, you can open the textbook in a side panel in VS Code as follows:</p>
<ol class="arabic simple">
<li><p>Type <code class="docutils literal notranslate"><span class="pre">ctrl-shift-P</span></code> (<code class="docutils literal notranslate"><span class="pre">command-shift-P</span></code> in macOS).</p></li>
<li><p>Type <code class="docutils literal notranslate"><span class="pre">Lean</span> <span class="pre">4:</span> <span class="pre">Docs:</span> <span class="pre">Show</span> <span class="pre">Documentation</span> <span class="pre">Resources</span></code> in the bar that appears, and then
press return. (You can press return to select it as soon as it is highlighted
in the menu.)</p></li>
<li><p>In the window that opens, click on <code class="docutils literal notranslate"><span class="pre">Mathematics</span> <span class="pre">in</span> <span class="pre">Lean</span></code>.</p></li>
</ol>
<p>Alternatively, you can run Lean and VS Code in the cloud,
using <a class="reference external" href="https://gitpod.io/">Gitpod</a>.
You can find instructions as to how to do that on the Mathematics in Lean
<a class="reference external" href="https://github.com/leanprover-community/mathematics_in_lean">project page</a>
on Github. We still recommend working in a copy of the <cite>MIL</cite> folder,
as described above.</p>
<p>This textbook and the associated repository are still a work in progress.
You can update the repository by typing <code class="docutils literal notranslate"><span class="pre">git</span> <span class="pre">pull</span></code>
followed by <code class="docutils literal notranslate"><span class="pre">lake</span> <span class="pre">exe</span> <span class="pre">cache</span> <span class="pre">get</span></code> inside the <code class="docutils literal notranslate"><span class="pre">mathematics_in_lean</span></code> folder.
(This assumes that you have not changed the contents of the <code class="docutils literal notranslate"><span class="pre">MIL</span></code> folder,
which is why we suggested making a copy.)</p>
<p>We intend for you to work on the exercises in the <code class="docutils literal notranslate"><span class="pre">MIL</span></code> folder while reading the
textbook, which contains explanations, instructions, and hints.
The text will often include examples, like this one:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#eval</span><span class="w"> </span><span class="s2">&quot;Hello, World!&quot;</span>
</pre></div>
</div>
<p>You should be able to find the corresponding example in the associated
Lean file.
If you click on the line, VS Code will show you Lean&#8217;s feedback in
the <code class="docutils literal notranslate"><span class="pre">Lean</span> <span class="pre">Goal</span></code> window, and if you hover
your cursor over the <code class="docutils literal notranslate"><span class="pre">#eval</span></code> command VS Code will show you Lean&#8217;s response
to this command in a pop-up window.
You are encouraged to edit the file and try examples of your own.</p>
<p>This book moreover provides lots of challenging exercises for you to try.
Don&#8217;t rush past these!
Lean is about <em>doing</em> mathematics interactively, not just reading about it.
Working through the exercises is central to the experience.
You don&#8217;t have to do all of them; when you feel comfortable that you have mastered
the relevant skills, feel free to move on.
You can always compare your solutions to the ones in the <code class="docutils literal notranslate"><span class="pre">solutions</span></code>
folder associated with each section.</p>
</section>
<section id="overview">
<h2><span class="section-number">1.2. </span>Overview<a class="headerlink" href="#overview" title="Link to this heading">&#61633;</a></h2>
<p>Put simply, Lean is a tool for building complex expressions in a formal language
known as <em>dependent type theory</em>.</p>
<p id="index-0">Every expression has a <em>type</em>, and you can use the <cite>#check</cite> command to
print it.
Some expressions have types like <cite>&#8469;</cite> or <cite>&#8469; &#8594; &#8469;</cite>.
These are mathematical objects.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span>

<span class="kd">def</span><span class="w"> </span><span class="n">f</span><span class="w"> </span><span class="o">(</span><span class="n">x</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">x</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">3</span>

<span class="k">#check</span><span class="w"> </span><span class="n">f</span>
</pre></div>
</div>
<p>Some expressions have type <cite>Prop</cite>.
These are mathematical statements.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="k">#check</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">4</span>

<span class="kd">def</span><span class="w"> </span><span class="n">FermatLastTheorem</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">&#8469;</span><span class="o">,</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&gt;</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">&#8743;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="mi">0</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">x</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">y</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8800;</span><span class="w"> </span><span class="n">z</span><span class="w"> </span><span class="bp">^</span><span class="w"> </span><span class="n">n</span>

<span class="k">#check</span><span class="w"> </span><span class="n">FermatLastTheorem</span>
</pre></div>
</div>
<p>Some expressions have a type, <cite>P</cite>, where <cite>P</cite> itself has type <cite>Prop</cite>.
Such an expression is a proof of the proposition <cite>P</cite>.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">theorem</span><span class="w"> </span><span class="n">easy</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="mi">2</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="mi">4</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="n">rfl</span>

<span class="k">#check</span><span class="w"> </span><span class="n">easy</span>

<span class="kd">theorem</span><span class="w"> </span><span class="n">hard</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">FermatLastTheorem</span><span class="w"> </span><span class="o">:=</span>
<span class="w">  </span><span class="gr">sorry</span>

<span class="k">#check</span><span class="w"> </span><span class="n">hard</span>
</pre></div>
</div>
<p>If you manage to construct an expression of type <code class="docutils literal notranslate"><span class="pre">FermatLastTheorem</span></code> and
Lean accepts it as a term of that type,
you have done something very impressive.
(Using <code class="docutils literal notranslate"><span class="pre">sorry</span></code> is cheating, and Lean knows it.)
So now you know the game.
All that is left to learn are the rules.</p>
<p>This book is complementary to a companion tutorial,
<a class="reference external" href="https://leanprover.github.io/theorem_proving_in_lean4/">Theorem Proving in Lean</a>,
which provides a more thorough introduction to the underlying logical framework
and core syntax of Lean.
<em>Theorem Proving in Lean</em> is for people who prefer to read a user manual cover to cover before
using a new dishwasher.
If you are the kind of person who prefers to hit the <em>start</em> button and
figure out how to activate the potscrubber feature later,
it makes more sense to start here and refer back to
<em>Theorem Proving in Lean</em> as necessary.</p>
<p>Another thing that distinguishes <em>Mathematics in Lean</em> from
<em>Theorem Proving in Lean</em> is that here we place a much greater
emphasis on the use of <em>tactics</em>.
Given that we are trying to build complex expressions,
Lean offers two ways of going about it:
we can write down the expressions themselves
(that is, suitable text descriptions thereof),
or we can provide Lean with <em>instructions</em> as to how to construct them.
For example, the following expression represents a proof of the fact that
if <code class="docutils literal notranslate"><span class="pre">n</span></code> is even then so is <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">*</span> <span class="pre">n</span></code>:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="k">fun</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="o">(</span><span class="n">hk</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">k</span><span class="o">)&#10217;</span><span class="w"> </span><span class="bp">&#8614;</span>
<span class="w">  </span><span class="k">have</span><span class="w"> </span><span class="n">hmn</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hk</span><span class="o">,</span><span class="w"> </span><span class="n">mul_add</span><span class="o">]</span>
<span class="w">  </span><span class="k">show</span><span class="w"> </span><span class="bp">&#8707;</span><span class="w"> </span><span class="n">l</span><span class="o">,</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">=</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="bp">+</span><span class="w"> </span><span class="n">l</span><span class="w"> </span><span class="k">from</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">_</span><span class="o">,</span><span class="w"> </span><span class="n">hmn</span><span class="o">&#10217;</span>
</pre></div>
</div>
<p>The <em>proof term</em> can be compressed to a single line:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span>
<span class="k">fun</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">hk</span><span class="o">&#10217;</span><span class="w"> </span><span class="bp">&#8614;</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="kd">by</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hk</span><span class="o">,</span><span class="w"> </span><span class="n">mul_add</span><span class="o">]&#10217;</span>
</pre></div>
</div>
<p>The following is, instead, a <em>tactic-style</em> proof of the same theorem, where lines
starting with <code class="docutils literal notranslate"><span class="pre">--</span></code> are comments, hence ignored by Lean:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="c1">-- Say `m` and `n` are natural numbers, and assume `n = 2 * k`.</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">hk</span><span class="o">&#10217;</span>
<span class="w">  </span><span class="c1">-- We need to prove `m * n` is twice a natural number. Let&#39;s show it&#39;s twice `m * k`.</span>
<span class="w">  </span><span class="n">use</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span>
<span class="w">  </span><span class="c1">-- Substitute for `n`,</span>
<span class="w">  </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hk</span><span class="o">]</span>
<span class="w">  </span><span class="c1">-- and now it&#39;s obvious.</span>
<span class="w">  </span><span class="n">ring</span>
</pre></div>
</div>
<p>As you enter each line of such a proof in VS Code,
Lean displays the <em>proof state</em> in a separate window,
telling you what facts you have already established and what
tasks remain to prove your theorem.
You can replay the proof by stepping through the lines,
since Lean will continue to show you the state of the proof
at the point where the cursor is.
In this example, you will then see that
the first line of the proof introduces <code class="docutils literal notranslate"><span class="pre">m</span></code> and <code class="docutils literal notranslate"><span class="pre">n</span></code>
(we could have renamed them at that point, if we wanted to),
and also decomposes the hypothesis <code class="docutils literal notranslate"><span class="pre">Even</span> <span class="pre">n</span></code> to
a <code class="docutils literal notranslate"><span class="pre">k</span></code> and the assumption that <code class="docutils literal notranslate"><span class="pre">n</span> <span class="pre">=</span> <span class="pre">2</span> <span class="pre">*</span> <span class="pre">k</span></code>.
The second line, <code class="docutils literal notranslate"><span class="pre">use</span> <span class="pre">m</span> <span class="pre">*</span> <span class="pre">k</span></code>,
declares that we are going to show that <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">*</span> <span class="pre">n</span></code> is even by
showing <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">*</span> <span class="pre">n</span> <span class="pre">=</span> <span class="pre">2</span> <span class="pre">*</span> <span class="pre">(m</span> <span class="pre">*</span> <span class="pre">k)</span></code>.
The next line uses the <code class="docutils literal notranslate"><span class="pre">rw</span></code> tactic
to replace <code class="docutils literal notranslate"><span class="pre">n</span></code> by <code class="docutils literal notranslate"><span class="pre">2</span> <span class="pre">*</span> <span class="pre">k</span></code> in the goal (<code class="docutils literal notranslate"><span class="pre">rw</span></code> stands for &#8220;rewrite&#8221;),
and the <code class="docutils literal notranslate"><span class="pre">ring</span></code> tactic solves the resulting goal <code class="docutils literal notranslate"><span class="pre">m</span> <span class="pre">*</span> <span class="pre">(2</span> <span class="pre">*</span> <span class="pre">k)</span> <span class="pre">=</span> <span class="pre">2</span> <span class="pre">*</span> <span class="pre">(m</span> <span class="pre">*</span> <span class="pre">k)</span></code>.</p>
<p>The ability to build a proof in small steps with incremental feedback
is extremely powerful. For that reason,
tactic proofs are often easier and quicker to write than
proof terms.
There isn&#8217;t a sharp distinction between the two:
tactic proofs can be inserted in proof terms,
as we did with the phrase <code class="docutils literal notranslate"><span class="pre">by</span> <span class="pre">rw</span> <span class="pre">[hk,</span> <span class="pre">mul_add]</span></code> in the example above.
We will also see that, conversely,
it is often useful to insert a short proof term in the middle of a tactic proof.
That said, in this book, our emphasis will be on the use of tactics.</p>
<p>In our example, the tactic proof can also be reduced to a one-liner:</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">rintro</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">&#10216;</span><span class="n">k</span><span class="o">,</span><span class="w"> </span><span class="n">hk</span><span class="o">&#10217;</span><span class="bp">;</span><span class="w"> </span><span class="n">use</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">k</span><span class="bp">;</span><span class="w"> </span><span class="n">rw</span><span class="w"> </span><span class="o">[</span><span class="n">hk</span><span class="o">]</span><span class="bp">;</span><span class="w"> </span><span class="n">ring</span>
</pre></div>
</div>
<p>Here we have used tactics to carry out small proof steps.
But they can also provide substantial automation,
and justify longer calculations and bigger inferential steps.
For example, we can invoke Lean&#8217;s simplifier with
specific rules for simplifying statements about parity to
prove our theorem automatically.</p>
<div class="highlight-lean notranslate"><div class="highlight"><pre><span></span><span class="kd">example</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="bp">&#8704;</span><span class="w"> </span><span class="n">m</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="o">:</span><span class="w"> </span><span class="n">Nat</span><span class="o">,</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="n">n</span><span class="w"> </span><span class="bp">&#8594;</span><span class="w"> </span><span class="n">Even</span><span class="w"> </span><span class="o">(</span><span class="n">m</span><span class="w"> </span><span class="bp">*</span><span class="w"> </span><span class="n">n</span><span class="o">)</span><span class="w"> </span><span class="o">:=</span><span class="w"> </span><span class="kd">by</span>
<span class="w">  </span><span class="n">intros</span><span class="bp">;</span><span class="w"> </span><span class="n">simp</span><span class="w"> </span><span class="o">[</span><span class="bp">*</span><span class="o">,</span><span class="w"> </span><span class="n">parity_simps</span><span class="o">]</span>
</pre></div>
</div>
<p>Another big difference between the two introductions is that
<em>Theorem Proving in Lean</em> depends only on core Lean and its built-in
tactics, whereas <em>Mathematics in Lean</em> is built on top of Lean&#8217;s
powerful and ever-growing library, <em>Mathlib</em>.
As a result, we can show you how to use some of the mathematical
objects and theorems in the library,
and some of the very useful tactics.
This book is not meant to be used as an complete overview of the library;
the <a class="reference external" href="https://leanprover-community.github.io/">community</a>
web pages contain extensive documentation.
Rather, our goal is to introduce you to the style of thinking that
underlies that formalization, and point out basic entry points
so that you are comfortable browsing the library and
finding things on your own.</p>
<p>Interactive theorem proving can be frustrating,
and the learning curve is steep.
But the Lean community is very welcoming to newcomers,
and people are available on the
<a class="reference external" href="https://leanprover.zulipchat.com/">Lean Zulip chat group</a> round the clock
to answer questions.
We hope to see you there, and have no doubt that
soon enough you, too, will be able to answer such questions
and contribute to the development of <em>Mathlib</em>.</p>
<p>So here is your mission, should you choose to accept it:
dive in, try the exercises, come to Zulip with questions, and have fun.
But be forewarned:
interactive theorem proving will challenge you to think about
mathematics and mathematical reasoning in fundamentally new ways.
Your life may never be the same.</p>
<p><em>Acknowledgments.</em> We are grateful to Gabriel Ebner for setting up the
infrastructure for running this tutorial in VS Code,
and to Kim Morrison and Mario Carneiro for help porting it from Lean 4.
We are also grateful for help and corrections from
Takeshi Abe,
Julian Berman, Alex Best, Thomas Browning,
Bulwi Cha, Hanson Char, Bryan Gin-ge Chen, Steven Clontz, Mauricio Collaris, Johan Commelin,
Mark Czubin,
Alexandru Duca,
Pierpaolo Frasa,
Denis Gorbachev, Winston de Greef, Mathieu Guay-Paquet,
Marc Huisinga,
Benjamin Jones,
Julian K&#252;lshammer,
Victor Liu, Jimmy Lu,
Martin C. Martin, Giovanni Mascellani, John McDowell, Joseph McKinsey, Bhavik Mehta, Isaiah Mindich,
Kabelo Moiloa, Hunter Monroe, Pietro Monticone,
Oliver Nash, Emanuelle Natale, Filippo A. E. Nuccio,
Pim Otte,
Bartosz Piotrowski,
Nicolas Rolland, Keith Rush,
Yannick Seurin, Guilherme Silva, Bernardo Subercaseaux,
Pedro S&#225;nchez Terraf, Matthew Toohey, Alistair Tucker,
Floris van Doorn,
Eric Wieser,
and others.
Our work has been partially supported by the Hoskinson Center for
Formal Mathematics.</p>
</section>
</section>


           </div>
          </div>
          <footer><div class="rst-footer-buttons" role="navigation" aria-label="Footer">
        <a href="index.html" class="btn btn-neutral float-left" title="Mathematics in Lean" accesskey="p" rel="prev"><span class="fa fa-arrow-circle-left" aria-hidden="true"></span> Previous</a>
        <a href="C02_Basics.html" class="btn btn-neutral float-right" title="2. Basics" accesskey="n" rel="next">Next <span class="fa fa-arrow-circle-right" aria-hidden="true"></span></a>
    </div>

  <hr/>

  <div role="contentinfo">
    <p>&#169; Copyright 2020-2025, Jeremy Avigad, Patrick Massot. Text licensed under CC BY 4.0.</p>
  </div>

  Built with <a href="https://www.sphinx-doc.org/">Sphinx</a> using a
    <a href="https://github.com/readthedocs/sphinx_rtd_theme">theme</a>
    provided by <a href="https://readthedocs.org">Read the Docs</a>.
   

</footer>
        </div>
      </div>
    </section>
  </div>
  <script>
      jQuery(function () {
          SphinxRtdTheme.Navigation.enable(true);
      });
  </script> 

</body>
</html>