In Lean 4: sorry (I’m not sorry.) #4

Hello everyone,

In this article, I will talk about the “sorry” command, which I first encountered in Lean 4. It took me a while to understand what it actually does.

First of all, just like I did in my previous post, I will explain it through a proof. In fact, I will use the exact same example.

Let’s say you have a main proof, but you also need to prove certain things within it — for instance, a + b = b + a. At that moment, you might not remember the “add_comm” command, or perhaps you are more focused on the main proof and don’t want to deal with the inner proofs right then. For situations just like this, We have ‘sorry’, which was created for situations like this.

Whereas normally, it should be like this:

import Mathlib.Tactic example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := by rw [add_comm x y]

If we use “sorry”, the code will work like this:

import Mathlib.Tactic example {M : Type*} [AddCommMonoid M] (x y : M) : x + y = y + x := by sorry

Important note: You must indent “sorry”. Meaning, considering the start of the line above it, you need to press the spacebar twice. If you write it aligned with the previous line, it will throw an error.

Stay coding!