Why is LEAN called LEAN?

Stream: new members

[Ian Allen]

I can't find the the etymology for LEAN anywhere in any of the documentation. Where does the (assumedly) acronym come from?

[Kevin Buzzard]

It's not an acronym, it's a reference to the fact that the kernel is small.

[Johan Commelin]

It's also "Lean" instead of "LEAN", even though the logo might suggest otherwise.

[Ian Allen]

Thanks guys, I was clearly way off. And yeah, it was the logo that got me turned around; though I had the small kernel fact in mind, I was expecting some clever double entendre on top of an acronym.

I would suggest editing the following from the Lean introduction section 1.1 at https://leanprover.github.io/introduction_to_lean/,

"Lean has a small and carefully written kernel, which serves to check that an expression is well-formed and confirm that it has a given type. It is this kernel that gives Lean its special character, and its name. Dependent type theory serves as a foundational language, allowing us to describe all sorts of objects and prove things about them. The foundational language fixes the meaning of the objects we introduce, and the kernel ensures that the things we prove about them are correct."

with changes highlighted in bold.

[Yaël Dillies]

Kevin Buzzard said:

It's not an acronym, it's a reference to the fact that the kernel is small.

... and written by Leonardo de Moura?

[Ian Allen]

Maybe there should just be a short paragraph outright explaining the name in the introduction. That's standard, or did I miss it somewhere else in the documentation?

This is coming up, among other reasons, because I am introducing Lean to colleagues at work and they ask what the name means.

[Patrick Massot]

See https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Teaching.20lean.20to.20high.20school.20students/near/132137220

[Kevin Buzzard]

Huh, that thread (from 2018) also contains some kid called Buzzard going on about how his students really like a game where you make the natural numbers from scratch

[mars0i]

The quantifiers in the logo are cool regardless.