>> Lean 3 was the least bloated theorem prover among Lean, Coq and Agda, and Lean 4 is the most bloated among this Big Three.
reply> Lean is far off the most bloated one. Isabelle most likely takes that spot.
Among these three is the operative phrase here.
I hate to be pedantic, but we are talking about theorem provers here :)
That is a fair point, thank you for the correction there
reply