The thing I love most about mechanized proofs is that my questions about the reasoning always have tangible answers, even if the answer is “we axiomatized this thing”.

The availability of the intermediate proof state as a part of the published object makes those answers that much easier to find. This is a really great project!