On: Llemma: An Open Language Model for Mathematics

[Vetch]

Ah you're right. That makes sense. The autocomplete, informal proofs, translation or autoformalization, reference, search, feedback interactive assistant use-cases do seem promising though.