The Math Is Haunted — overreacted
Lean is a programming language, but it is mostly used by mathematicians. That is quite unusual! This is because Lean is designed to formalize mathematics.
Lean lets mathematicians treat mathematics as code—break it into structures, theorems and proofs, import each other’s theorems, and put them on GitHub.
The big idea is that eventually much of the humanity’s mathematical knowledge might be available as code—statically checked, verifiable, and composable.
To a mathematician’s eye, this syntax looks like stating a theorem. We have the theorem keyword, the name or our theorem, a colon : before its statement, the statement that we’d like to prove, and := by followed by the proof (sorry means that we haven’t completed the actual proof yet but we’re planning to fill it in later).
But if you’re a programmer, you might notice a hint of something else. That theorem looks suspiciously like a function. But then what is 2 = 2? It looks like a return type of that function. But how can 2 = 2 be a type? Isn’t 2 = 2 just a boolean? And if 2 = 2 really is a type, what are the values of that 2 = 2 type? These are very interesting questions, but we’ll have to forget about them for now.
