---
license: mit
---

Tactic generation model in CT2 format, generated by [this Python script](https://github.com/lean-dojo/LeanCopilot/blob/main/scripts/convert_t5encoder_to_ct2.py).