  In interactive theorem proving, formalization quality is a key factor for
maintainability and re-usability of developments and can also impact
proof-checking performance. Commonly, anti-patterns that cause quality issues
are known to experienced users. However, in many theorem prover systems, there
are no automatic tools to check for their presence and make less experienced
users aware of them. We attempt to fill this gap in the Isabelle environment by
developing a linter as a publicly available add-on component. The linter offers
basic configurability, extensibility, Isabelle/jEdit integration, and a
standalone command-line tool. We uncovered 480 potential problems in
Isabelle/HOL, 14016 in other formalizations of the Isabelle distribution, and
an astonishing 59573 in the AFP. With a specific lint bundle for AFP
submissions, we found that submission guidelines were violated in 1595 cases.
We set out to alleviate problems in Isabelle/HOL and solved 168 of them so far;
we found that high-severity lints corresponded to actual problems most of the
time, individual users often made the same mistakes in many places, and that
solving those problems retrospectively amounts to a substantial amount of work.
In contrast, solving these problems interactively for new developments usually
incurs only little overhead, as we found in a quantitative user survey with 22
participants (less than a minute for more than 60% of participants). We also
found that a good explanation of problems is key to the users' ease of solving
these problems (correlation coefficient 0.48), and their satisfaction with the
end result (correlation coefficient 0.62).
