I'm not part of the community, so I assume Martin's comment is on the lack of fraternity that Leonardo shows to other theorem provers' creators.
But I'm extremely impressed on Lean's strategy to verify software correctness. Even if it's well know that multiple implementations help to find bugs, I'm surprised the Lean team invested time and effort to set up a system to cross check the different implementations result accross multiple proofs.
@rogersm @gallais @MartinEscardo It's two things: he describes the idea of a small independent proof-checking kernel as if it was his original idea, when it's a principle that has been around in the proof assistant community for a long time (named the *de Bruijn criterion*. Earliest published reference I can find is Barendregt and Wiedijk 2005 http://doi.org/10.1098/rsta.2005.1650 but I distinctly remember people talking about it when I was doing my PhD 2000-2004).
He also describes it as an advantage that Lean has over Rocq, when Rocq has a kernel and this was considered an important part of its design from the very start of Coq v1.
Roger Sen
Robin Adams