Huỳnh Trần Khanh (Jun 15 2023 at 03:11): Huỳnh Trần Khanh (Jun 15 2023 at 03:11):if you're doing formal verification, you may be eligible for free API access. fill out this form https://docs.google.com/forms/d/e/1FAIpQLSfVc2MJOggqxUCFF12Td80YVbQE5EAy97mgCXSHPAkm_dIvWQ/viewform and wait 2 weeks. hopefully you can make something interesting. you can use "function calling" on gpt 3.5 and on June 27, you'll be able to use "function calling" on gpt 4. someone can invent a natural language interface for Coq now :eyes:
Huỳnh Trần Khanh (Jun 15 2023 at 03:22):https://openai.com/blog/function-calling-and-other-api-updates
Huỳnh Trần Khanh (Jun 15 2023 at 10:37):I'm sorry. after searching in the Lean Zulip I found out that the form isn't monitored anymore. still many Lean users are having free access to the API and they're building cool stuff with it. I got access on Feb 5, 2021. I was excited about the function calling feature, that's why I made this post. but I didn't check whether the form was still monitored or not when posting
I guess you could tell me what kind of stuff I could try to build with this new capability to make Coq more user friendly? and if I manage to make a quick PoC I'll share it with you
Last updated: Oct 13 2024 at 01:02 UTC