Is it any good at autoformalisation? I think it's likely to take focused fine-tuning to get something small enough that is still good at that.