lean-gptf

lean-gptf copied to clipboard

Is there any version for Lean 4?

1

Is there any version for Lean 4?

EricZhongYJ

Getting Invalid Organization error

3

[gptf_proof_search_step] run_best_beam_candidate UNEXPECTED MESSAGE: --- ["ERROR { \"error\":{ \"code\":\"invalid_organization\", \n \"message\":\"No such organization: org-kuQ09yewcuHU5GN5YYEUp2hh.\", \n \"param\":null, \n \"type\":\"invalid_request_error\"}}"]

saisurbehera

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

venom12138

OpenAI key

1

Hi! I applied for an OpenAI key for exploring the gpt-f tactic by filling the form mentioned in the repo last week. @jesse-michael-han Is there any further step necessary for...

ayush1801