public/lean-for-javascript-developers/1.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/10.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/11.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/12.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/13.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/14.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/15.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/16.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/17.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/18.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/19.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/2.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/20.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/24.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/25.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/26.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/27.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/3.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/4.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/5.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/6.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/7.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/8.png

This is a binary file and will not be displayed.

public/lean-for-javascript-developers/9.png

This is a binary file and will not be displayed.

+889

public/lean-for-javascript-developers/index.md

··· 1 1 + --- 2 2 + title: Lean for JavaScript Developers 3 3 + date: '2025-09-02' 4 4 + spoiler: Programming with proofs. 5 5 + --- 6 6 + 7 7 + This is my opinionated syntax primer for the [Lean](https://lean-lang.org/) programming language. It is far from complete and may contain inaccuracies (I'm still learning Lean myself) but this is how I wish I was introduced to it, and what I wish was clarified. 8 8 + 9 9 + --- 10 10 + 11 11 + ### Why Lean? 12 12 + 13 13 + This post assumes you're already eager to learn a bit of Lean. For motivation, I humbly submit to you two takes: [one from me](https://bsky.app/profile/danabra.mov/post/3lxjfxdlow22m) and [one from its creator](https://www.amazon.science/blog/how-the-lean-language-brings-math-to-coding-and-coding-to-math). 14 14 + 15 15 + --- 16 16 + 17 17 + ### Declaring Definitions 18 18 + 19 19 + Let's start by writing a few *definitions*. These can appear at the top level of the file: 20 20 + 21 21 + ```lean 22 22 + def name := "Alice" 23 23 + def age := 42 24 24 + ``` 25 25 + 26 26 + *([Try it in the online playground.](https://live.lean-lang.org/#codez=CYUwZgBAdghgtiCAuAvBARAQQDYEsDGI6AUKJDAOaKoQAsATMUA))* 27 27 + 28 28 + Note you have to write `:=` (assignment) rather than `=`. This is because Lean uses `=` for comparisons. This might remind you of Go or Pascal (if you're old enough). 29 29 + 30 30 + Although you haven't written any types explicitly, each definition is typed. To find out their types, you can hover over `name` and `age` in the online playground or [inside VS Code](https://lean-lang.org/install/). You should see `name : String` and `42 : Nat`, respectively. (Going forward, when I say "hover", I'll assume either of those environments.) 31 31 + 32 32 + Here, `String` is obviously a string, while `Nat` stands for a "natural number". In Lean, natural numbers include `0`, `1`, `2`, and so on, going up arbitrarily large. 33 33 + 34 34 + You could specify types explicitly by writing ` : SomeType` before the `:=`: 35 35 + 36 36 + ```lean 37 37 + def name : String := "Alice" 38 38 + def age : Nat := 42 39 39 + ``` 40 40 + 41 41 + If you don't, Lean will try to infer the type from what you wrote on the right side. 42 42 + 43 43 + --- 44 44 + 45 45 + ### Specifying Types 46 46 + 47 47 + You've just seen that Lean infers `"Alice"` to be a `String` and `42` to be a `Nat`. A `Nat` could be `0`, `1`, `2`, and so on. What if you try a negative number like `-140`? 48 48 + 49 49 + ```lean 50 50 + def temperature := -140 51 51 + ``` 52 52 + 53 53 + If you hover on `temperature`, you'll see that it's an `Int`. An `Int`, which stands *for integer*, is a built-in type allowing any whole number, negative or positive. 54 54 + 55 55 + You could ask for a specific type like `Int` explicitly in the definition: 56 56 + 57 57 + ```lean 58 58 + def roomTemperature : Int := 25 59 59 + ``` 60 60 + 61 61 + If you just wrote `def roomTemperature := 25`, Lean would give you a `Nat`, but adding `: Int` explicitly nudged type inference to try to produce an `Int`. 62 62 + 63 63 + Another way to ask for a specific type is to wrap the expression itself: 64 64 + 65 65 + ```lean 66 66 + def roomTemperature := (25 : Int) 67 67 + ``` 68 68 + 69 69 + In both cases, you're saying you really want to get an `Int`. If Lean couldn't figure out how to produce an `Int` from the expression, it would give you a type error. 70 70 + 71 71 + --- 72 72 + 73 73 + Let's calculate Alice's birth year based on her age: 74 74 + 75 75 + ```lean {3} 76 76 + def name := "Alice" 77 77 + def age := 42 78 78 + def birthYear := 2025 - age 79 79 + ``` 80 80 + 81 81 + We need to get `birthYear` somewhere on the screen. If you're following along in the [online playground](https://live.lean-lang.org/), you might realize that your code isn't actually running. 82 82 + 83 83 + This is because there are two ways to use Lean. 84 84 + 85 85 + One way to use Lean is to run your code. Another way to use Lean is to prove some facts *about* your code. You can also do both--write code and proofs about it. We're going to start by learning to run some code, and then we'll look at writing proofs. 86 86 + 87 87 + --- 88 88 + 89 89 + ### Running Code 90 90 + 91 91 + If you just want to see the result of some expression, add an `#eval` command: 92 92 + 93 93 + ```lean {5} 94 94 + def name := "Alice" 95 95 + def age := 42 96 96 + def birthYear := 2025 - age 97 97 + 98 98 + #eval birthYear 99 99 + ``` 100 100 + 101 101 + Hovering over this `#eval` in your editor will now say `1983`. Another place where it'll show up is the *InfoView* on the right side of the online playground: 102 102 + 103 103 +  104 104 + 105 105 + Note `1983` in the bottom right corner. If you [set up VS Code with the Lean extension](https://lean-lang.org/install/) locally, you can get the same InfoView displayed like this: 106 106 + 107 107 +  108 108 + 109 109 + Lean InfoView is incredibly useful and I suggest to keep it open at all times. 110 110 + 111 111 + The `#eval` command is handy for doing inline calculations and to verify your code is working as intended. But maybe you actually want to run a program that outputs something. You can turn a Lean file into a real program by defining `main`: 112 112 + 113 113 + ```lean {4} 114 114 + def name := "Alice" 115 115 + def age := 42 116 116 + def birthYear := 2025 - age 117 117 + def main := IO.println birthYear 118 118 + ``` 119 119 + 120 120 + I intentionally did not say "a `main` function" because `main` is not a function. (You can hover over it to learn the type of the `main` but we won't focus on that today.) 121 121 + 122 122 + Let's run our program: 123 123 + 124 124 + ```sh 125 125 + lean --run Scratch.lean 126 126 + ``` 127 127 + 128 128 + Now `1983` appears in the terminal. Alternatively, you could also do this: 129 129 + 130 130 + ```sh 131 131 + lean Scratch.lean -c Scratch.c 132 132 + ``` 133 133 + 134 134 + The C code generated by Lean compiler will include an instruction to print `1983`: 135 135 + 136 136 + ```c 137 137 + LEAN_EXPORT lean_object* _lean_main(lean_object* x_1) { 138 138 + lean_object* x_2; lean_object* x_3; 139 139 + x_2 = lean_unsigned_to_nat(1983u); 140 140 + x_3 = l_IO_println___at___main_spec__0(x_2, x_1); 141 141 + return x_3; 142 142 + } 143 143 + ``` 144 144 + 145 145 + Now you see that Lean can be used to write programs. 146 146 + 147 147 + --- 148 148 + 149 149 + ### Writing Proofs 150 150 + 151 151 + Now let's *prove* that `age + birthYear` together add up to `2025`. 152 152 + 153 153 + Define a little `theorem` alongside with your program: 154 154 + 155 155 + ```lean {5-6} 156 156 + def name := "Alice" 157 157 + def age := 42 158 158 + def birthYear := 2025 - age 159 159 + 160 160 + theorem my_theorem : age + birthYear = 2025 := by 161 161 + sorry 162 162 + ``` 163 163 + 164 164 + A `theorem` is like a `def`, but [aimed](https://proofassistants.stackexchange.com/a/1576) specifically at declaring proofs. 165 165 + 166 166 + [The declared type of a theorem is a statement that it's supposed to prove.](/beyond-booleans/#propositions-as-types) Your job is now to construct a proof of that type, and the Lean "tactic mode" (activated with `by`) provides you with an interactive and concise way to construct such proofs. 167 167 + 168 168 + Initially, the InfoView tells you that your goal is `age + birthYear = 2025`: 169 169 + 170 170 +  171 171 + 172 172 + However, that's not something you can be sure in directly. What's `age`? Try to `unfold age` to replace `age` in the goal with whatever its definition says: 173 173 + 174 174 +  175 175 + 176 176 + Note how this made the goal in your InfoView change to `42 + birthYear = 2025`. Okay, but what's a `birthYear`? Let's `unfold birthYear` as well: 177 177 + 178 178 +  179 179 + 180 180 + You're getting closer; the goal is now `42 + (2025 - age) = 2025`. Unfolding `birthYear` brought back `age`, what's `age` again? Let's `unfold age`: 181 181 + 182 182 +  183 183 + 184 184 + At this point the goal is `42 + (2025 - 42) = 2025`, which is a simple arithmetic expression. The built-in `decide` tactic can solve those with gusto: 185 185 + 186 186 +  187 187 + 188 188 + And you're done! You've now proven that `age + birthYear = 2025` without actually having *run* any code. This is being verified *during typechecking.* 189 189 + 190 190 + You can verify that editing `age` to another number will not invalidate your proof. However, if you edit `birthYear` to `2023 - age`, the proof no longer typechecks: 191 191 + 192 192 +  193 193 + 194 194 + Of course, this was all a bit verbose. Instead of doing `unfold` for each definition manually, you can tell the `simp` simplifier to do them recursively for you: 195 195 + 196 196 + ![simp [age, birthView] solves the same theorem](./13.png) 197 197 + 198 198 + This also proves the goal. 199 199 + 200 200 + This example is contrived but I wanted to show you how it feels to step through the code step by step and transform it "outside in". It almost makes you feel like *you're* the computer, logically transforming the code towards the goal. It won't always be so tedious, especially if you have some useful theorems prepared. 201 201 + 202 202 + We'll come back to proving things, but for now let's learn some more Lean basics. 203 203 + 204 204 + --- 205 205 + 206 206 + ### Opening Namespaces 207 207 + 208 208 + Have another look at this `main` definition: 209 209 + 210 210 + ```lean {4} 211 211 + def name := "Alice" 212 212 + def age := 42 213 213 + def birthYear := 2025 - age 214 214 + def main := IO.println birthYear 215 215 + ``` 216 216 + 217 217 + Here, `IO.println birthYear` is a function call. `IO` is a namespace, and `println` is a function defined in that namespace. You pass `birthYear` to it. 218 218 + 219 219 + You could avoid the need to write `IO.` before it by *opening* the `IO` namespace: 220 220 + 221 221 + ```lean {1,6} 222 222 + open IO 223 223 + 224 224 + def name := "Alice" 225 225 + def age := 42 226 226 + def birthYear := 2025 - age 227 227 + def main := println birthYear 228 228 + ``` 229 229 + 230 230 + This doesn't have to be done at the top of the file: 231 231 + 232 232 + ```lean {5} 233 233 + def name := "Alice" 234 234 + def age := 42 235 235 + def birthYear := 2025 - age 236 236 + 237 237 + open IO 238 238 + def main := println birthYear 239 239 + ``` 240 240 + 241 241 + It can be a bit confusing that now you have to write `IO.println` anywhere above that `open IO` but you can write `println` directly anywhere below it. As an alternative, you can scope opening `IO` to a specific definition by adding `in`: 242 242 + 243 243 + ```lean {5} 244 244 + def name := "Alice" 245 245 + def age := 42 246 246 + def birthYear := 2025 - age 247 247 + 248 248 + open IO in 249 249 + def main := println birthYear 250 250 + ``` 251 251 + 252 252 + This would make the shorter syntax available inside `main` but not outside it. 253 253 + 254 254 + We're not using `IO` much so I'll keep referring to `println` as `IO.println` below. 255 255 + 256 256 + --- 257 257 + 258 258 + ### Passing Arguments 259 259 + 260 260 + Now notice how you're passing `birthYear` to the `println` function: 261 261 + 262 262 + ```lean {4} 263 263 + def name := "Alice" 264 264 + def age := 42 265 265 + def birthYear := 2025 - age 266 266 + def main := IO.println birthYear 267 267 + ``` 268 268 + 269 269 + Unlike languages like JavaScript, Lean doesn't use parentheses or commas for function calls. Instead of `f(a, b, c)`, you would write `f a b c` in Lean. 270 270 + 271 271 + I need to emphasize this. No commas and no parens are used for function calls! 272 272 + 273 273 + However, you would sometimes use parentheses *around* individual arguments. Suppose you replace `birthYear` with `2025 - age` directly in the function call: 274 274 + 275 275 + ```lean {3} 276 276 + def name := "Alice" 277 277 + def age := 42 278 278 + def main := IO.println 2025 - age 279 279 + ``` 280 280 + 281 281 + This will lead to an error: 282 282 + 283 283 +  284 284 + 285 285 + Lean thinks you're trying to do `(IO.println 2025) - age`, so it looks for a way to subtract `age` (which is a `Nat`) from whatever `IO.println 2025` returns (which happens to be something called `IO Unit`). Lean can't find a subtraction operation (`HSub`) between an `IO Unit` and a `Nat`, so it gives up in frustration. 286 286 + 287 287 + To fix this, add parentheses around `2025 - age`: 288 288 + 289 289 + ```lean {3} 290 290 + def name := "Alice" 291 291 + def age := 42 292 292 + def main := IO.println (2025 - age) 293 293 + ``` 294 294 + 295 295 + Now instead of `IO.println` "eating" the `2025` argument, it knows that the first argument is the entire `(2025 - age)` expression. You might find it helpful to use `(` and `)` liberally and try removing them to get a feel for when they're necessary. 296 296 + 297 297 + Note `(` and `)` here have nothing to do with the `IO.println` function call. Their only purpose is to "group" `2025 - age` together, like you group things in math. 298 298 + 299 299 + **In other words, instead of writing `something(f(x, y), a, g(z))` as you might in JavaSript, you would write `something (f x y) a (g z)` in Lean.** 300 300 + 301 301 + Read this closely several times and make sure it burns deep in your subconscious. 302 302 + 303 303 + --- 304 304 + 305 305 + ### Nesting Expressions 306 306 + 307 307 + You can't nest Lean definitions. However, if some of your definitions get complex, you can simplify them by declaring some `let` bindings inside of the `def`. 308 308 + 309 309 + For example, you could pull `(2025 - age)` from the last example into a `let`: 310 310 + 311 311 + ```lean {5-6} 312 312 + def name := "Alice" 313 313 + def age := 42 314 314 + 315 315 + def main := 316 316 + let birthYear := 2025 - age 317 317 + IO.println birthYear 318 318 + ``` 319 319 + 320 320 + Again, note the use of `:=` for assignment. It's `:=`, not `=`! 321 321 + 322 322 + You might think that being multiline makes `main` a function, but it doesn't. Adding a `let` binding is just a way to make definitions easier to read. You could use `let` inside of any definition, including the `name` and `age` definitions: 323 323 + 324 324 + ```lean {2-3,6-8} 325 325 + def name := 326 326 + let namesInPassport := ["Alice", "Babbage", "McDuck"] 327 327 + namesInPassport[0] 328 328 + 329 329 + def age := 330 330 + let twenty := 20 331 331 + let one := 1 332 332 + twenty + twenty + one + one 333 333 + 334 334 + def main := 335 335 + let birthYear := 2025 - age 336 336 + IO.println birthYear 337 337 + ``` 338 338 + 339 339 + There is no need for a `return` statement here. The last line of a definition becomes its value. This is why the definitions above are equivalent to: 340 340 + 341 341 + ```lean 342 342 + def name := ["Alice", "Babbage", "McDuck"][0] 343 343 + def age := 20 + 20 + 1 + 1 344 344 + def main := IO.println (2025 - age) 345 345 + ``` 346 346 + 347 347 + In the end, the right side of any definition unfolds into a single expression, but `let` lets you break down that expression into more readable (and reusable) pieces. 348 348 + 349 349 + --- 350 350 + 351 351 + ### Declaring Functions 352 352 + 353 353 + Currently `birthYear` hardcodes `2025` into the calculation: 354 354 + 355 355 + ```lean {3} 356 356 + def name := "Alice" 357 357 + def age := 42 358 358 + def birthYear := 2025 - age 359 359 + def main := IO.println birthYear 360 360 + ``` 361 361 + 362 362 + You can turn `birthYear` into a *function* definition by declaring a `currentYear` argument immediately after writing `def birthYear` followed by a space: 363 363 + 364 364 + ```lean {3} 365 365 + def name := "Alice" 366 366 + def age := 42 367 367 + def birthYear currentYear := currentYear - age 368 368 + ``` 369 369 + 370 370 + This makes `birthYear` a function. You can call it by writing `birthYear 2025`: 371 371 + 372 372 + ```lean {4} 373 373 + def name := "Alice" 374 374 + def age := 42 375 375 + def birthYear currentYear := currentYear - age 376 376 + def main := IO.println (birthYear 2025) 377 377 + ``` 378 378 + 379 379 + Again, the parens around `birthYear 2025` ensure that `IO.println` doesn't try to "eat" the `birthYear` function itself. We want it to "eat" `birthYear 2025`. 380 380 + 381 381 + If you hover over `birthYear` now, you'll see that its type is no longer a `Nat`: 382 382 + 383 383 +  384 384 + 385 385 + This is how Lean pretty-prints function types. You see the function name `birthYear`, followed by its arguments (we only have one), `:` and the return type. 386 386 + 387 387 + You could write it that way explicitly, too, to clarify your intended types: 388 388 + 389 389 + ```lean 390 390 + def birthYear (currentYear : Nat) : Nat := currentYear - age 391 391 + ``` 392 392 + 393 393 + Note, again, that `(` `)` parentheses in Lean have nothing to do with function calls. You only use the parentheses to treat `(currentYear : Nat)` as a single thing. 394 394 + 395 395 + --- 396 396 + 397 397 + ### Many Ways to Declare a Function 398 398 + 399 399 + You've seen two ways to define the same function, with implicit and explicit types: 400 400 + 401 401 + ```lean 402 402 + /-- Types are implicit here, Lean infers them -/ 403 403 + def birthYear currentYear := currentYear - age 404 404 + 405 405 + /-- Types are explicit here -/ 406 406 + def birthYear (currentYear : Nat) : Nat := currentYear - age 407 407 + ``` 408 408 + 409 409 + There are even more valid ways to write the same thing with different verbosity. Here is a (non-exhaustive) list of ways to define the same `birthYear` function: 410 410 + 411 411 + ```lean 412 412 + /-- Concise definition -/ 413 413 + def birthYear currentYear := currentYear - age 414 414 + def birthYear (currentYear: Nat) := currentYear - age 415 415 + def birthYear (currentYear: Nat) : Nat := currentYear - age 416 416 + 417 417 + /-- Definition set to an anonymous function -/ 418 418 + def birthYear := fun currentYear => currentYear - age 419 419 + def birthYear := fun (currentYear: Nat) => currentYear - age 420 420 + 421 421 + /-- Definition (with explicit type) set to an anonymous function -/ 422 422 + def birthYear : Nat → Nat := fun currentYear => currentYear - age 423 423 + ``` 424 424 + 425 425 + This might remind you of `function f() {}` vs `const f = () => ...` in JS. I find the concise syntax most pleasant to read and recommend using it unless you specifically need an anonymous function (e.g. to pass it to another function). 426 426 + 427 427 + Here, `Nat → Nat` is the actual type of `birthYear`, no matter which syntax is used. It takes a `Nat` and it returns a `Nat`, so it's `Nat → Nat`. The fancy `→` arrow is typed by writing `\to` followed by a space in the [playground](https://live.lean-lang.org/) or with [Lean VSCode](https://lean-lang.org/install/). 428 428 + 429 429 + Specifying argument types but inferring the return is often a nice middle ground: 430 430 + 431 431 + ```lean 432 432 + def birthYear (currentYear: Nat) := currentYear - age 433 433 + ``` 434 434 + 435 435 + Just like with `function` declarations vs arrow functions in JavaScript, the level of verbosity and typing that you want to do in each case is mostly up to you. 436 436 + 437 437 + (Sidenote: You might also see syntax like `fun x ↦ x * 2` rather than `fun x => x * 2`. Here, `↦` is typed as `\maps`, and mathematicians prefer it aesthetically to `=>`. Lean doesn't distinguish them so you'll see `=>` in codebases like Lean itself while `↦` shows up in "mathy" codebases like Mathlib. They do exactly the same.) 438 438 + 439 439 + --- 440 440 + 441 441 + ### Adding Arguments 442 442 + 443 443 + Now that you know a dozen ways to write functions, let's get back to this one: 444 444 + 445 445 + ```lean {3} 446 446 + def name := "Alice" 447 447 + def age := 42 448 448 + def birthYear currentYear := currentYear - age 449 449 + def main := IO.println (birthYear 2025) 450 450 + ``` 451 451 + 452 452 + Suppose you want to make `age` an argument to the `birthYear` function. To add an argument, just write it next in the `def birthYear` definition argument list: 453 453 + 454 454 + ```lean {2-3} 455 455 + def name := "Alice" 456 456 + def birthYear currentYear age := currentYear - age 457 457 + def main := IO.println (birthYear 2025 42) 458 458 + ``` 459 459 + 460 460 + Actually, this doesn't work, and the error is sucky. 461 461 + 462 462 +  463 463 + 464 464 + The problem is the issue I described earlier--at this point, Lean has no idea what the types of `currentYear` and `age` might be. Previously, it relied on `age` being an earlier declaration (and inferred it to be a `Nat`) but now Lean is truly stumped. 465 465 + 466 466 + The strange error message ("typeclass instance is stuck") alludes to the fact that it's trying to find an implementation of subtraction between two types (searching for that implementation is done via "typeclass search") but it doesn't even know what those types are (that's why you see weird `?m.24` and `?m.12` placeholders). 467 467 + 468 468 + The fix to this is to bite the bullet and to actually specify the types: 469 469 + 470 470 + ```lean {3} 471 471 + def name := "Alice" 472 472 + 473 473 + def birthYear (currentYear : Nat) (age : Nat) := 474 474 + currentYear - age 475 475 + 476 476 + def main := IO.println (birthYear 2025 42) 477 477 + ``` 478 478 + 479 479 + Now there is no ambiguity. Note that the parentheses here don't mean anything special--it's only a way to separate parameters from each other. Just like when calling functions, we're not using commas so we need parens for grouping. 480 480 + 481 481 + When you have multiple parameters of the same type in a row, like `currentYear` and `age` above, you may put them together together under one type declaration: 482 482 + 483 483 + ```lean {3} 484 484 + def name := "Alice" 485 485 + 486 486 + def birthYear (currentYear age : Nat) := 487 487 + currentYear - age 488 488 + 489 489 + def main := IO.println (birthYear 2025 42) 490 490 + ``` 491 491 + 492 492 + This doesn't change semantics but is shorter to write. This is particularly useful in mathematics where you might have 3 or 4 parameters that are all `Nat` or such. 493 493 + 494 494 + Now that you're specifying all parameter types explicitly, it makes sense to think about them harder and to give them slightly different types. While `age` should remain a `Nat`, `currentYear` makes more sense as an `Int` so that the calculation still works for people born in the BC era or who are over two thousand years old. 495 495 + 496 496 + ```lean {3} 497 497 + def name := "Alice" 498 498 + 499 499 + def birthYear (currentYear : Int) (age : Nat) := 500 500 + currentYear - age 501 501 + 502 502 + def main := IO.println (birthYear 2025 42) 503 503 + ``` 504 504 + 505 505 + The non-pretty-formatted type of `birthYear` is `Int → Nat → Int` because it takes an `Int` and also a `Nat`, and returns an `Int`. As in some other functional languages, you can partially apply it--for example, `birthYear 2025` will give you a `Nat → Int` function that you can later call with the remaining `age` argument. 506 506 + 507 507 + By now, you might have guessed that there are other increasingly deranged equivalent ways to define the same function that takes an `Int` and a `Nat`: 508 508 + 509 509 + ```lean 510 510 + def birthYear (currentYear : Int) (age : Nat) := currentYear - age 511 511 + def birthYear (currentYear : Int) := fun (age : Nat) => currentYear - age 512 512 + def birthYear := fun (currentYear : Int) (age : Nat) => currentYear - age 513 513 + def birthYear := fun (currentYear : Int) => fun (age : Nat) => currentYear - age 514 514 + def birthYear: Int → Nat → Int := fun currentYear age => currentYear - age 515 515 + def birthYear: Int → Nat → Int := fun currentYear => fun age => currentYear - age 516 516 + ``` 517 517 + 518 518 + **Read them closely keeping in mind that they are all exactly equivalent in Lean.** It's confusing to mix syntax within a single definition so we'll stick with this: 519 519 + 520 520 + ```lean 521 521 + def birthYear (currentYear : Int) (age : Nat) := 522 522 + currentYear - age 523 523 + ``` 524 524 + 525 525 + It's time to revisit proofs. 526 526 + 527 527 + --- 528 528 + 529 529 + ### Proving For All 530 530 + 531 531 + A few sections earlier, you've proven `birthYear + age = 2005` for this code: 532 532 + 533 533 + ```lean 534 534 + def name := "Alice" 535 535 + def age := 42 536 536 + def birthYear := 2025 - age 537 537 + 538 538 + theorem my_theorem : age + birthYear = 2025 := by 539 539 + simp [age, birthYear] 540 540 + ``` 541 541 + 542 542 + However, now `birthYear` is a function which takes two arguments: 543 543 + 544 544 + ```lean {3} 545 545 + def name := "Alice" 546 546 + 547 547 + def birthYear (currentYear : Int) (age : Nat) := 548 548 + currentYear - age 549 549 + ``` 550 550 + 551 551 + You could copypaste this theorem for concrete values of `age` and `currentYear`: 552 552 + 553 553 + ```lean {6-13} 554 554 + def name := "Alice" 555 555 + 556 556 + def birthYear (currentYear : Int) (age : Nat) := 557 557 + currentYear - age 558 558 + 559 559 + theorem my_theorem : 42 + birthYear 2025 42 = 2025 := by 560 560 + simp [birthYear] 561 561 + 562 562 + theorem my_theorem' : 25 + birthYear 2025 25 = 2025 := by 563 563 + simp [birthYear] 564 564 + 565 565 + theorem my_theorem'' : 77 + birthYear 1980 77 = 1980 := by 566 566 + simp [birthYear] 567 567 + ``` 568 568 + 569 569 + These proofs typecheck, but there's a feeling that it's not any better than writing tests. What we're hoping to capture is a *universal pattern*, not a bunch of cases. 570 570 + 571 571 + The fact is, no matter what `cy` (I'll shorten "current year" to that) and `a` (short for "age") are, `birthYear cy a` is supposed to be equal to `cy`. Let's capture that: 572 572 + 573 573 + ```lean {6-7} 574 574 + def name := "Alice" 575 575 + 576 576 + def birthYear (currentYear : Int) (age : Nat) := 577 577 + currentYear - age 578 578 + 579 579 + theorem my_theorem : a + birthYear cy a = cy := by 580 580 + sorry 581 581 + ``` 582 582 + 583 583 + Although you haven't declared `a` and `cy`, this is actually valid syntax! The VS Code Lean extension will implicitly insert `{a cy}` arguments after `my_theorem`: 584 584 + 585 585 +  586 586 + 587 587 + These "implicit" arguments surrounded by `{` `}` curly braces can sometimes be very useful to avoid boilerplate, but in this case they're more confusing than helpful. Let's declare `cy` and `a` explicitly as normal arguments to `my_theorem`: 588 588 + 589 589 + ```lean {6} 590 590 + def name := "Alice" 591 591 + 592 592 + def birthYear (currentYear : Int) (age : Nat) := 593 593 + currentYear - age 594 594 + 595 595 + theorem my_theorem (cy : Int) (a : Nat) : a + birthYear cy a = cy := by 596 596 + sorry 597 597 + ``` 598 598 + 599 599 + Note how declaring `my_theorem` with `cy` and `a` is similar to declaring function arguments--except that you can't actually "call" this theorem. You're just stating that, for any `cy` and `a`, you can produce a proof of `a + birthYear cy a = cy`. 600 600 + 601 601 + Let's see if you actually can! 602 602 + 603 603 + You start out with the goal of `↑a + birthYear cy a = cy`: 604 604 + 605 605 +  606 606 + 607 607 + The `⊢` symbol before it tells you that this is the goal, i.e. what you want to prove. Things above it, like `cy : Int` and `a : Nat`, are the things you *already have.* 608 608 + 609 609 + You might be wondering: what *are* those `cy : Int` and `a : Nat`. What *are* their values? But the question doesn't make sense. You're writing a proof, so in a sense, you are working with *all possible values at the same time.* You only have their types. 610 610 + 611 611 + Have another look at the goal: `↑a + birthYear cy a = cy`. 612 612 + 613 613 + What's that up arrow? 614 614 + 615 615 + Hover over it in the InfoView: 616 616 + 617 617 +  618 618 + 619 619 + The signature is a bit confusing (what's that `@`? what's that `instNatCastInt`?) but you can see that it takes your `a` (which is a `Nat`) and returns an `Int`. So this is how Lean displays the fact that your `a` is being converted to an `Int` so that it can be added with the result of `birthYear cy a` call (which is already an `Int`). 620 620 + 621 621 + Okay, cool, the goal is to prove `↑a + birthYear cy a = cy`. How do we do that? 622 622 + 623 623 + Well, first, let's `unfold birthYear` to replace it with the implementation: 624 624 + 625 625 +  626 626 + 627 627 + Now the goal becomes `↑a + (cy - ↑a) = cy`. 628 628 + 629 629 + You can't use the `decide` tactic from earlier because it only deals with known concrete numbers--it's like a calculator. However, Lean also includes an `omega` tactic that can check equations that include unknown numbers like `a` and `cy`. 630 630 + 631 631 + With `omega`, you can complete this proof! 632 632 + 633 633 +  634 634 + 635 635 + Let's have another look at the full code: 636 636 + 637 637 + ```lean 638 638 + def name := "Alice" 639 639 + 640 640 + def birthYear (currentYear : Int) (age : Nat) := 641 641 + currentYear - age 642 642 + 643 643 + theorem my_theorem (cy: Int) (a : Nat) : a + birthYear cy a = cy := by 644 644 + unfold birthYear 645 645 + omega 646 646 + ``` 647 647 + 648 648 + You have a function called `birthYear` and a theorem called `my_theorem` about its behavior. By convention, you might want to call it `birthYear_spec`, or something more specific like `age_add_birthYear_eq_current_year`. 649 649 + 650 650 + In a way it's like a test, but it's a test for *all possible inputs of that function* that runs during typechecking. I think this is incredibly cool. You can verify that incorrectly changing the formula of `birthYear` will cause the proof to no longer typecheck: 651 651 + 652 652 +  653 653 + 654 654 + --- 655 655 + 656 656 + ### Universal Quantifier 657 657 + 658 658 + You've previously declared `cy` and `a` as arguments for `my_theorem`: 659 659 + 660 660 + ```lean 661 661 + theorem my_theorem (cy: Int) (a : Nat) : a + birthYear cy a = cy := by 662 662 + unfold birthYear 663 663 + omega 664 664 + ``` 665 665 + 666 666 + In this case, it's fine to omit their types because they can be exactly inferred by Lean from the `birthYear` call itself, which you already explicitly annotated: 667 667 + 668 668 + ```lean {1} 669 669 + theorem my_theorem cy a : a + birthYear cy a = cy := by 670 670 + unfold birthYear 671 671 + omega 672 672 + ``` 673 673 + 674 674 + This theorem says "for all `cy` and `a`, `a + birthYear cy a` is equal to `cy`”. Mathematicians have their own way of writing statements like this, using the *universal quantifier* ∀ (which stands for "for all"): *∀ cy a, a + birthYear(cy, a) = cy*. 675 675 + 676 676 + You can restate the above in a mathematician's style with the `∀` quantifier: 677 677 + 678 678 + ```lean {1} 679 679 + theorem my_theorem : ∀ cy a, a + birthYear cy a = cy := by 680 680 + sorry 681 681 + ``` 682 682 + 683 683 + To type `∀`, write `\all` and press space. 684 684 + 685 685 + Now instead of `cy a :`, we have `: ∀ cy a`. The universal quantifier lets the arguments get introduced "later"--pretty much like currying in programming. However, the difference is mostly stylistic. The theorem signature is the same. 686 686 + 687 687 + When you use `∀`, you're starting out with a universal statement ("for all `cy` and `a`") so `cy` and `a` aren't in your tactic state yet. Use `intro cy a` to bring them in: 688 688 + 689 689 +  690 690 + 691 691 + Again, you don't have their *concrete* values because a proof is supposed to work for all possible values. You don't know anything about them except their types. 692 692 + 693 693 + From that point, your goal is `↑a + birthYear cy a = cy`, which you can solve: 694 694 + 695 695 + ```lean {3-4} 696 696 + theorem my_theorem : ∀ cy a, a + birthYear cy a = cy := by 697 697 + intro cy a 698 698 + unfold birthYear 699 699 + omega 700 700 + ``` 701 701 + 702 702 + Notice how `∀ cy a` has essentially moved the declarations of `cy` and `a` "inside" the proof itself. Under the hood, the `intro` tactic generates a nested function with `cy` and `a` arguments, so in the end this `theorem` has the same shape as before adding `∀`. It may feel disorienting that Lean lets you write the same thing in many styles, but this lets the Lean core stay small and evolve faster, while tactics and conventions may evolve independently and vary between projects. 703 703 + 704 704 + Using `∀` may not seem particularly appealing in this example, but it is great for nested propositions where anonymous functions would add too much clutter. It can also be convenient to extract a theorem's claim into its own definition: 705 705 + 706 706 + ```lean {1,3,4} 707 707 + def TheLawOfAging : Prop := ∀ cy a, a + birthYear cy a = cy 708 708 + 709 709 + theorem my_theorem : TheLawOfAging := by 710 710 + unfold TheLawOfAging 711 711 + unfold birthYear 712 712 + omega 713 713 + ``` 714 714 + 715 715 + To learn what a `Prop` is, check out [my previous article](/beyond-booleans/). 716 716 + 717 717 + --- 718 718 + 719 719 + ### Implicit Arguments 720 720 + 721 721 + Now let us come back to this example, and specifically to this line: 722 722 + 723 723 + ```lean {8} 724 724 + def name := "Alice" 725 725 + 726 726 + def birthYear (currentYear : Int) (age : Nat) := 727 727 + currentYear - age 728 728 + 729 729 + def main := 730 730 + let year := birthYear 2025 42 731 731 + IO.println year 732 732 + ``` 733 733 + 734 734 + Hover over `IO.println`, and you might freak out: 735 735 + 736 736 + ![IO.println.\{u_1\} \{a : Type u_1\} [ToString α] (s: α) : IO Unit](./25.png) 737 737 + 738 738 + What the hell is this signature?! Learning to read these signatures will immensely improve your ability to understand Lean APIs and debug errors so I'm going to break it down even though we haven't discussed most of the relevant topics. 739 739 + 740 740 + The key insight is that the parts in `{` `}` and `[` `]` are not something you pass to the function directly. That's why you're able to just write `IO.println year`. However, these *are* actual arguments--they're just filled in by Lean itself. 741 741 + 742 742 + Command+Click into `println` to see that it declares `{α}` and `[ToString α]`: 743 743 + 744 744 + ```lean 745 745 + def println {α} [ToString α] (s : α) : IO Unit := 746 746 + print ((toString s).push '\n') 747 747 + ``` 748 748 + 749 749 + So if you Lean fills them in for you, where *are* they coming from? 750 750 + 751 751 + The parts in `{` `}` are called *ordinary implicit parameters*, and they are filled in by type inference based on the parameters that have already been passed in. If Lean can't unambiguously fill them in, it will complain and would not typecheck. Here, the `α` argument is implicit, but it's determined by what *you* passed as an explicit `(s : α)` argument. You're printing an `Int`, you passed `(s: Int)`, so `α` is `Int`. This is similar to generics, but in Lean generics are just arguments (often implicit). 752 752 + 753 753 + 754 754 + The parts in `[` `]`, like `[ToString α]`, are called *instance implicit parameters* and are filled in automatically depending on the code you've imported so far. Lean has a mechanism that lets libraries declare implementations of certain intefaces--for example, "how to subtract `Int` and `Int`" or "how to convert `Nat` to `Int`" or "how to turn an `Int` to a `String`”. The `println` function wants a `ToString` implementation that knows how to turn whatever *you* passed (an `Int`) to a string. Lean has a `ToString Int` implementation in core, so that's what `println` gets. 755 755 + 756 756 + Finally, the very first `.{}` thing is a "universe" in which this function's type lives. This is rarely something you need to deal with, and is also filled in automatically. 757 757 + 758 758 + If you're curious what Lean is filling in (or need to debug some gnarly case that wouldn't typecheck), you can prefix your function call with `@` to force all arguments to be passed explicitly. Start by passing `_` placeholders: 759 759 + 760 760 + ```lean {8} 761 761 + def name := "Alice" 762 762 + 763 763 + def birthYear (currentYear : Int) (age : Nat) := 764 764 + currentYear - age 765 765 + 766 766 + def main := 767 767 + let year := birthYear 2025 42 768 768 + @IO.println _ _ year 769 769 + ``` 770 770 + 771 771 + Now you can hover over each `_` placeholder to see what Lean has inferred for it. 772 772 + 773 773 + For example, the `{α}` implicit parameter was inferred to be `Int`: 774 774 + 775 775 +  776 776 + 777 777 + And the `[ToString]` instance implicit parameter received `instToStringInt`: 778 778 + 779 779 +  780 780 + 781 781 + If you want to further debug what's going on, you can fill them in in the code: 782 782 + 783 783 + ```lean {8} 784 784 + def name := "Alice" 785 785 + 786 786 + def birthYear (currentYear : Int) (age : Nat) := 787 787 + currentYear - age 788 788 + 789 789 + def main := 790 790 + let year := birthYear 2025 42 791 791 + @IO.println Int instToStringInt year 792 792 + ``` 793 793 + 794 794 + That's what you would have to type if Lean couldn't fill them in automatically. 795 795 + 796 796 + Now it's easy to Command+Click them and see if they match what you expected. For example, Command+Clicking `instToStringInt` from here will teleport you to the place in the Lean source that actually implements `ToString Int`: 797 797 + 798 798 + ```lean 799 799 + instance : ToString Int where 800 800 + toString 801 801 + | Int.ofNat m => toString m 802 802 + | Int.negSucc m => "-" ++ toString (succ m) 803 803 + ``` 804 804 + 805 805 + Seems legit! When you're done spelunking, you can remove the `@` and the `_`s: 806 806 + 807 807 + ```lean {8} 808 808 + def name := "Alice" 809 809 + 810 810 + def birthYear (currentYear : Int) (age : Nat) := 811 811 + currentYear - age 812 812 + 813 813 + def main := 814 814 + let year := birthYear 2025 42 815 815 + IO.println year 816 816 + ``` 817 817 + 818 818 + Implicit and instance arguments save a tremenduous amount of boilerplate when operating on complex structures like mathematical objects and proofs. But even here, they let Lean provide a simple, extensible, and strongly-typed `println` API. 819 819 + 820 820 + --- 821 821 + 822 822 + ### Command+Click Anything 823 823 + 824 824 + There's a *lot* more I would've liked to cover but I'm running out of steam--and this article is already long. The good news is, there's a lot you can learn by peeking under the hood on your own because Lean is extremely Command+Click-able. 825 825 + 826 826 + You can Command+Click into data types like `Nat` and `String`, and even pieces of syntax like `∀`. Much of Lean is implemented in Lean itself, and most of the time what I found ended up both simpler and more interesting than what I expected. 827 827 + 828 828 + ```lean 829 829 + /-- 830 830 + The natural numbers, starting at zero. 831 831 + This type is special-cased by both the kernel and the compiler, and overridden with an efficient 832 832 + implementation. Both use a fast arbitrary-precision arithmetic library (usually 833 833 + [GMP](https://gmplib.org/)); at runtime, `Nat` values that are sufficiently small are unboxed. 834 834 + -/ 835 835 + inductive Nat where 836 836 + /-- Zero, the smallest natural number. -/ 837 837 + | zero : Nat 838 838 + /-- The successor of a natural number `n`. -/ 839 839 + | succ (n : Nat) : Nat 840 840 + ``` 841 841 + 842 842 + Who would've thought that numbers just a recursively generated enum? 843 843 + 844 844 + Turns out, a language built with recursively defined types like this can express and prove facts like that the [area of a circle is π * r ^ 2](https://github.com/leanprover-community/mathlib4/blob/aac79004bad67a82c18ab7d39c609529f4159d6f/Archive/Wiedijk100Theorems/AreaOfACircle.lean#L81-L130), or that [it takes 23 people to exceed a 50% chance of same birthday](https://github.com/leanprover-community/mathlib4/blob/aac79004bad67a82c18ab7d39c609529f4159d6f/Archive/Wiedijk100Theorems/BirthdayProblem.lean#L65-L81), or that [you can't cube a cube](https://github.com/leanprover-community/mathlib4/blob/aac79004bad67a82c18ab7d39c609529f4159d6f/Archive/Wiedijk100Theorems/CubingACube.lean#L533-L546). But you can also write normal programs with it that compile to C. [Async/await](https://lean-lang.org/fro/roadmap/1900-1-1-the-lean-fro-year-3-roadmap/) is in the works. 845 845 + 846 846 + Maybe you could create something in the middle--programs interleaved with proofs? You can see this pattern in the Lean core itself: here's a [`List.append` (`++`) function](https://github.com/leanprover/lean4/blob/c83237baf78d6930d40e556a5cacdca149c4b198/src/Init/Data/List/Basic.lean#L614-L616), and here are proofs that [`(as ++ bs).length = as.length + bs.length`](https://github.com/leanprover/lean4/blob/c83237baf78d6930d40e556a5cacdca149c4b198/src/Init/Data/List/Basic.lean#L661-L664) and [`(as ++ bs) ++ cs = as ++ (bs ++ cs)`](https://github.com/leanprover/lean4/blob/c83237baf78d6930d40e556a5cacdca149c4b198/src/Init/Data/List/Basic.lean#L666-L669) written alongside it. In other words, using the Lean data structures in code means also lets you reuse known facts about those structures to prove claims about your own code. 847 847 + 848 848 + --- 849 849 + 850 850 + ### Programming With Proofs 851 851 + 852 852 + Lean is built on old ideas and a lot of prior art, but there are both novel and pragmatic twists. Sometimes I can't tell if I'm writing Go or Haskell, Rocq or C#, OCaml or Python. In its giddily unrestrained ambition it reminds me of [Nemerle](https://en.wikipedia.org/wiki/Nemerle), but it also feels solid and grounded. It's being used in both industry and academia, including by [DeepMind](https://deepmind.google/discover/blog/ai-solves-imo-problems-at-silver-medal-level/) and [Amazon](https://aws.amazon.com/blogs/opensource/lean-into-verified-software-development/). It's been a while since I felt excited about a programming language (mind you--a *pure* functional programming language). 853 853 + 854 854 + Anyway, here's a little program that counts up and down alongside some proofs. 855 855 + 856 856 + ```lean 857 857 + def append (xs ys : List a) : List a := Id.run do 858 858 + let mut out := ys 859 859 + for x in xs.reverse do 860 860 + out := x :: out 861 861 + return out 862 862 + 863 863 + theorem append_abcd : append ["a", "b"] ["c", "d"] = ["a", "b", "c", "d"] := by 864 864 + simp [append] 865 865 + 866 866 + theorem append_length (xs ys : List a) : (append xs ys).length = xs.length + ys.length := by 867 867 + simp [append] 868 868 + 869 869 + 870 870 + def count_up_and_down n := 871 871 + let up := List.range (n) 872 872 + let down := (List.range (n + 1)).reverse 873 873 + append up down 874 874 + 875 875 + theorem count_up_and_down_length n : (count_up_and_down n).length = n * 2 + 1 := by 876 876 + simp only [count_up_and_down, append_length, List.length_range, List.length_reverse] 877 877 + omega 878 878 + 879 879 + 880 880 + def main := do 881 881 + IO.println "Enter a number: " 882 882 + let stdin ← IO.getStdin 883 883 + let input ← stdin.getLine 884 884 + let n := input.trim.toNat! 885 885 + let sequence := count_up_and_down n 886 886 + IO.println sequence 887 887 + ``` 888 888 + 889 889 + I've never written code alongside proofs like this before. Have you?