DistilGPT2 English language model fine-tuned on mathematical proofs extracted from arXiv.org LaTeX sources from 1992 to 2020.
Proofs have been cleaned up a bit. In particular, they use
CITE
for any citationREF
for any referenceMATH
for any LaTeX mathematical formulaCASE:
for any\\item
or labeled subcase.
For text generation, I recommend prompts such as:
Let MATH be given.
By the inductive hypothesis,
If MATH is a nonempty