The AMS Linter

The AMSLinter is a linter to aid with formatting contributions to the Formal Conjectures repository by ensuring that results in a file have the appropriate subject tags.

def AMSLinter : Lean.Linter

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

Equations

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