kaiyuy
/

ct2-leandojo-lean4-retriever-byt5-small

Inference Endpoints

Model card Files Files and versions Community

Edit model card

Tactic generation model in CT2 format, generated by this Python script.

Downloads last month: 5

Inference API

Unable to determine this model’s pipeline type. Check the docs .

Collection including kaiyuy/ct2-leandojo-lean4-retriever-byt5-small

LeanDojo

Machine learning for theorem proving in Lean: https://leandojo.org/ • 10 items • Updated Jul 23 • 1