search

jesse-michael-han / lean-gptf

Interactive neural theorem proving in Lean
Apache License 2.0
118 stars 6 forks source link

It seems that the model "formal-lean-pact" doesn't exist. #12

Open venom12138 opened 2 years ago

venom12138 commented 2 years ago

It seems that the model "formal-lean-pact" doesn't exist. Could you please tell me what 's the new model id?