how to use claude 3.5 sonnet as out of the box as possible?

lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean

https://leandojo.org

MIT License

999 stars 92 forks source link

how to use claude 3.5 sonnet as out of the box as possible? #124

Open alok opened 2 months ago

alok commented 2 months ago

(this issue is partly a testing ground for an ai tool)

@ellipsis-dev please add to the README how to use claude 3.5 sonnet with leancopilot on a mac (over cloud).

Peiyang-Song commented 2 weeks ago

Thank you @alok , is the test done yet? Also curious what is the outcome :)

By the way, if there is really a demand to use any new external model with LeanCopilot by its API, the easiest approach should be to follow a similar pipeline as PR #97 to use Lean Copilot's external model support feature.

alok commented 2 weeks ago

Apparently a repo owner has to invoke the bot, though i'd be happy to pay the $20 to try it for a month for the repo. The annoying thing about #97 is needing to run the python server, which is not quite out of the box.