Stream: Machine learning and automation

Topic: Free access to OpenAI API


view this post on Zulip 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:

view this post on Zulip Huỳnh Trần Khanh (Jun 15 2023 at 03:22):

https://openai.com/blog/function-calling-and-other-api-updates

view this post on Zulip 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: Jun 17 2024 at 22:01 UTC