Lean GPT-f beta

Stream: lean-gptf

[Jesse Michael Han]

The lean-gptf beta is now online! Sign up for an API key here and check out the lean-gptf repository here.

Currently the repository uses a custom fork of Lean 3.23; however, we are planning a new community Lean release soon with all the features needed by the gptf tactic.

[Bryan Gin-ge Chen]

I managed to get this working in VS Code :tada:

I'm passing the API key to vscode-lean by launching VS Code from the command line with OPENAI_API_KEY=key code . (Actually, I made an alias for this in my profile.)

One slightly annoying thing is that the curl output causes the Lean: Server Errors panel to pop up (see screenshot): Screen-Shot-2021-01-18-at-1.29.35-PM.png

Maybe there's some option you can use that makes curl more silent?

[Jesse Michael Han]

@Bryan Gin-ge Chen thanks for flagging, pushed a fix so that curl is invoked with the --silent flag --- does this solve the issue?

[Bryan Gin-ge Chen]

Yes, it does. Thanks!

[Rob Lewis]

Jesse Michael Han said:

Currently the repository uses a custom fork of Lean 3.23; however, we are planning a new community Lean release soon with all the features needed by the gptf tactic.

This means we need to compile mathlib locally to use it as a dependency in your lean-gptf repo, right?

[Patrick Massot]

I think the same as Rob: I'll definitely play with this toy, but I'll wait for the Lean release (and mathlib Lean version bump).

[Rob Lewis]

If you push a mathlib branch that changes leanpkg.toml to use your forked Lean, and then change the leanpkg.toml in lean-gptf to point to that mathlib commit, it should let us use leanproject like normal here

[Rob Lewis]

Note that I only suggest this because this is a cool toy and I trust Jesse! I'd prefer this not to become a standard way to interact with the CI :)

[Rob Lewis]

Patrick Massot said:

I think the same as Rob: I'll definitely play with this toy, but I'll wait for the Lean release (and mathlib Lean version bump).

(This isn't what I think btw, I'm compiling locally now)

[Jesse Michael Han]

Rob Lewis said:

Jesse Michael Han said:

Currently the repository uses a custom fork of Lean 3.23; however, we are planning a new community Lean release soon with all the features needed by the gptf tactic.

This means we need to compile mathlib locally to use it as a dependency in your lean-gptf repo, right?

correct, though this should hopefully only be necessary for a few more days :pray:

[Rob Lewis]

Bryan Gin-ge Chen said:

I managed to get this working in VS Code :tada:

I'm passing the API key to vscode-lean by launching VS Code from the command line with OPENAI_API_KEY=key code . (Actually, I made an alias for this in my profile.)

@Bryan Gin-ge Chen could you elaborate? What did you do before launching VS Code? Just setting the env variable and then launching from that shell doesn't seem to be enough.

[Jesse Michael Han]

^you can also set the private meta def OPENAI_API_KEY := some $KEY (in tactic.gptf.gptf) instead of none to hack around this

[Rob Lewis]

Thanks, that's easier for now

[Bryan Gin-ge Chen]

@Rob Lewis Hmm, strange, all I did was launch VS Code from the command line with the OPENAPI_API_KEY=my_key code .. The VAR=value should be setting the environment variable for the command that follows, in this case code ..

[Rob Lewis]

Hmm, alright, thanks. I'll keep fiddling

[Jesse Michael Han]

Patrick Massot said:

I think the same as Rob: I'll definitely play with this toy, but I'll wait for the Lean release (and mathlib Lean version bump).

@Patrick Massot new Lean release + mathlib version have been bumped, build time should be instantaneous now with leanproject get-mathlib-cache :pray:

[Patrick Massot]

Great! I'll definitely play with it

[Stanislas Polu]

Sorry for the small latency in getting the latest invites out. Everyone who requested access should have received an invite by now. Please do not hesitate to reach out if it's not the case.

[Johan Commelin]

Now that mathlib uses lean-3.26.0 should this be easier to setup?

[Patrick Massot]

Is there documentation about how to add this as a dependency to an existing project depending on mathlib? Say we want to play with it while working on the liquid tensor experiment, what should we do?

[Jesse Michael Han]

Patrick Massot said:

Is there documentation about how to add this as a dependency to an existing project depending on mathlib? Say we want to play with it while working on the liquid tensor experiment, what should we do?

now that it uses the same base Lean as mathlib, it's as easy as

leanpkg add jesse-michael-han/lean-gptf

leanpkg configure

leanproject get-mathlib-cache

leanpkg build

then remember to import tactic.gptf :)

[Jesse Michael Han]

i just checked and it was able to rederive a proof in for_mathlib/linear_algebra in lean-liquid:

lemma reindex_linear_equiv_sum_empty_symm :
  (reindex_linear_equiv (sum_empty _) (sum_empty _)).symm M = from_blocks M 0 0 0 :=
begin
  ext; simp, rcases i; rcases j; simp!,
    { cases j; simp },
    { rcases i with ⟨i⟩ },
    { cases i }

  -- ext (i|i) (j|j),
  -- { simp only [sum_empty_apply_inl, reindex_linear_equiv_symm_apply, from_blocks_apply₁₁] },
  -- { cases j },
  -- { cases i }
end

[Jesse Michael Han]

^updated the lean-gptf README as well, thanks for flagging

[Patrick Massot]

Thanks @Jesse Michael Han!

[Johan Commelin]

@Jesse Michael Han this is great! thanks a lot

[Stanislas Polu]

Batch of invites sent today. Sorry for the delay in responding some of the requests submitted at https://forms.gle/WaS7dbGjkP31uhS59

[Kalle Kytölä]

Hi! First of all, I might have plenty of misunderstandings about what lean-gptf is and what its current status is, but from the comments / presentations I've seen about it, it looks extremely interesting! If possible, I'd like to try it.

I tried the instructions posted above and in the repo. In step 1, leanpkg add jesse-michael-han/lean-gptf, however, I get the error

lean-gptf: trying to update _target/deps/lean-gptf to revision lean-3.30.0
cannot find revision lean-3.30.0 in repository _target/deps/lean-gptf

Is it obvious what I'm doing wrong? Thanks in advance!

[Stanislas Polu]

cc @Jesse Michael Han

[Huỳnh Trần Khanh]

This error is pretty frustrating. In the meantime you can just clone the lean-gptf repo and edit the example.lean file when you want GPT-f suggestions.

[Huỳnh Trần Khanh]

That's what I do.

[Ayush Agrawal]

Hi guys! I recently got the key. After pasting the key. I tried to start tinkering with the example.lean file. There are no errors coming but the tactic states are taking forever to appear (see the ss). It been quite a long since I have put the cursor over the refl tactic. Is this normal or am I missing something? image.png

[Jason Rute]

Have you tried restarting the lean server? (The easiest way is just to restart vs code.)

[Ayush Agrawal]

Yes @Jason Rute I restarted vscode. I'll do this again and notify if I this problem persists.

[Ayush Agrawal]

After waiting for some time. These errors popped up. Can you please shed some light on these? image.png

[Floris van Doorn]

That is a common error message if the server is unhappy.

• Make sure you have the mathlib olean files: leanproject get-mathlib-cache
• Restarting VSCode again

[Floris van Doorn]

Also make sure you have not edited any file that is imported by the file you have open (try e.g. git status)

[Ayush Agrawal]

Regarding the key should I paste my key like OPEN_AI_KEY : "<KEY>" or OPEN_AI_KEY : "KEY". Also, for private meta def OPENAI_API_KEY : option string := some $KEY or some "KEY"(Is it important to past the key here also?). Please clarify if there is some mistake in pasting here :sweat_smile: . Thanks!

[Ayush Agrawal]

Now it seems working but it is throwing the error can't find the OpenAI key. Maybe there is a issue with the way I pasted the key. image.png @Floris van Doorn @Stanislas Polu any leads on this?

[Jason Rute]

By the way, for general Lean knowledge, Floris is a good person to ask. For gptf specific stuff, like this key question, Stan is better. But, let me look up how I have it set up on my machine…

[Ayush Agrawal]

Maybe these errors might also help process exited with status 35.. image.png

[Jason Rute]

I personally opted to go the environment variable route. If you are familiar with Environment variables, then I put it in my bash_profile file as follows:

# open ai key
export OPENAI_API_KEY="Ab3De6Gh9JkAb3De6Gh9JkAb3De6Gh9JkAb3De6Gh9Jk"

(where Ab3De6Gh9JkAb3De6Gh9JkAb3De6Gh9JkAb3De6Gh9Jk is in place of my real key). You can check it is correct as follows from the command line:

$ echo $OPENAI_API_KEY
Ab3De6Gh9JkAb3De6Gh9JkAb3De6Gh9JkAb3De6Gh9Jk

If you are not comfortable with env variables, you can edit this line in the gpt.lean file to look like below:

private meta def OPENAI_API_KEY : option string := some "Ab3De6Gh9JkAb3De6Gh9JkAb3De6Gh9JkAb3De6Gh9Jk"

But please heed the warnings and don't commit this changed file to a public repo.

I personally have not done this second way, but I assume it works.

[Ayush Agrawal]

@Jason Rute I tried the second method and getting the error process exited with status 35. Are u familiar with this error? image.png

[Jason Rute]

I think that is being returned by the curl command (which gptf uses under the hood). I don’t really have time to debug what is happening right now, but here is some documentation on that error: https://bobcares.com/blog/php-curl-ssl-connect-error-35/

[Jason Rute]

Sorry. I wish I could be of more help.

[Ayush Agrawal]

Thanks @Jason Rute . Np! I'll notify if this issue gets fixed.. Thanks for the help!

[Jason Rute]

That website lists a firewall as being one source of that error. Are you on a system with a firewall (say at a company) that bans SSL connections.

[Ayush Agrawal]

Oh yes I am working on my company's work system.

[Ayush Agrawal]

Hi @Jason Rute I am now able to use the gpt-f tactic - I installed Lean over some other remote server so probably the previous errors were due to the firewall on my current sys that was banning the SSL connections.

[Arthur Paulino]

Hey I've seen some content about GPT-f from Jan/Feb/Mar and I think it's pretty impressive. Is there a place where the team keeps track of improvements and new findings? It got me super curious :smiley_cat:

[Stanislas Polu]

Hi Arthur! Released work include the GPT-f paper and the PACT paper:
https://arxiv.org/abs/2009.03393
https://arxiv.org/abs/2102.06203
Happy to answer any question you might have and hopefully we can share more soon!

[Stanislas Polu]

Hi Everyone. We're tearing down the model that is backing the gptf tactic but will work on getting a new model online soon. We'll also work on providing a better experience potentially looking to interface with the VSCode extension more directly. If you have any idea you'd like us to explore, please let us know, the goal is really to provide the community with useful assistance from the models we train. Please let me know if you have questions :+1:

[Stanislas Polu]

Note: that model is trained on a very old mathlib snapshot and rotted in many ways. I doubt it has today any usefulness to anybody with access to it. But let me know if that's the case and we'll find a way to support you.

[Ayush Agrawal]

Hi @Stanislas Polu I wanted to use the gpt-f and see some outputs from that. I had the key but I am currently not able to use it as it says search engine not found. Have you teared down the model? Or if there is some other way to access it let me know. Thanks!

[Daniel Selsam]

Ayush Agrawal said:

Hi Stanislas Polu I wanted to use the gpt-f and see some outputs from that. I had the key but I am currently not able to use it as it says search engine not found. Have you teared down the model? Or if there is some other way to access it let me know. Thanks!

See https://leanprover.zulipchat.com/#narrow/stream/274007-lean-gptf/topic/Lean.20GPT-f.20beta/near/273140603

[Ayush Agrawal]

Hi @Daniel Selsam. I saw the above post. I was just wondering whether there is some backup available or we cannot have the access to the prior gpt-f at all..

[Stanislas Polu]

Hi @Ayush Agrawal! Unfortunately the model is offline right now. We'll work on setting a more recent one up shortly :+1:

[Adam Topaz]

Stanislas Polu said:

Hi Ayush Agrawal! Unfortunately the model is offline right now. We'll work on setting a more recent one up shortly :+1:

I'm just wondering whether there are any updates on this front?