The Problem Status Linter

The problemStatusLinter is a linter to aid with formatting contributions to the Formal Conjectures repository by ensuring that results in a file have the appropriate tags in order to distinguish between open/already solved problems and background results/sanity checks.

def problemStatusLinter : Lean.Linter

The problem category linter checks that every theorem/lemma/example has been given a problem category attribute.

Equations

• One or more equations did not get rendered due to their size.