The Lean developers put out a paper about v4's reference counting last year which shows that in basic benchmarks, Lean 4 is in the same ballpark as Haskell, Swi

The Lean developers put out a paper about v4's reference counting last year which shows that in basic benchmarks, Lean 4 is in the same ballpark as Haskell, Swift, and ML. https://arxiv.org/abs/1908.05647 https://arxiv.org/abs/1908.05647