Lean's Law of Formalisation Design

Stream: general

[Fabrizio Montesi]

The discussion in #computer science > Overloading Lean's notation and a recent exchange with Phil himself makes me think there's a scientific law about formalisations akin to Wadler's law for language design. ;-)
I propose:

---

Lean's Law of Formalisation Design

In any Lean formalisation design, the total time spent discussing a feature is proportional to two raised to the power of its position.

0. Theorems
1. Types
2. Namespaces
3. Notation

---

Maybe people have observed this already?

[Alok Singh]

Omfg lmfao

[Edward van de Meent]

something something proportional to a constant :lol:

[Ruben Van de Velde]

I think the total time spent is O(lifetime of the universe) for all of those