This is a set of automatically generated lemmas. Each file consists of 8000 lemmas. Overall there are currently ~180000 lemmas.
It always ends with a commentary which states if the tactic 'try_finish' from lean-gym (https://github.com/openai/lean-gym) solves it. Otherwise, the line ends with '--non-trivial'. If there is an additional 'n' at the start of the commentary, the negation of the lemma is solved by 'try_finish'.