Zulip Chat Archive

Stream: lean-gptf

Topic: using gptf on olympiad problems


view this post on Zulip David Renshaw (Apr 06 2021 at 02:09):

lean-gptf just helped me finish this proof: https://github.com/dwrensha/mathematical-puzzles-in-lean/blob/85f3a4c903dc33a50b1ea03499f55e4646850daf/src/bulgaria1998_q3.lean

view this post on Zulip David Renshaw (Apr 06 2021 at 02:10):

I'm starting to think of it as an "autocomplete" feature.

view this post on Zulip David Renshaw (Apr 06 2021 at 02:13):

Two places where I specifically remember it helping:

      have h2 : (0:) < 2 ^ i := pow_pos (by norm_num) i,

and

calc (i : ) in finset.range n, (1:) / 2^i
          = (i : ) in finset.range n, (1 / 2)^i : by {congr; simp [div_eq_mul_inv]}

view this post on Zulip Jason Rute (Apr 06 2021 at 04:19):

When you say “autocomplete”, do you mean you used the prefix feature, or that it completes the proof?

view this post on Zulip David Renshaw (Apr 06 2021 at 12:01):

"the prefix feature" is not something that I know about

view this post on Zulip David Renshaw (Apr 06 2021 at 12:03):

I mean that it feels like a bit like writing natural language in Google Docs, where sometimes Google will suggest three or four words to finish your sentence.

view this post on Zulip David Renshaw (Apr 06 2021 at 12:04):

In both the lean-gptf and the Google Docs case, I am often impressed with the context-dependence and accuracy of the predictions.

view this post on Zulip David Renshaw (Apr 06 2021 at 12:07):

But also in both cases, I don't expect the AI to help if I don't already basically have the high level idea of what I'm trying to say already laid out.

view this post on Zulip David Renshaw (Apr 06 2021 at 12:13):

I find myself reaching for gptf when I think "I know there are probably some lemmas or tactics in mathlib that will easily close this goal, but I'm too lazy to wade through the mathlib docs to find them (and library_search isn't helping)".

view this post on Zulip David Renshaw (Apr 06 2021 at 12:16):

(It occurs to me that maybe I ought to try the simpler suggest tactic more.)

view this post on Zulip Kevin Buzzard (Apr 06 2021 at 12:23):

hint is also helpful in these situations (I think suggest suggests lemmas and hint suggests tactics)

view this post on Zulip Jason Rute (Apr 06 2021 at 12:51):

As for the prefix feature gptf {pfx:= “rw”} , say, forces it to give you a tactic command starting with “rw”.

view this post on Zulip Jesse Michael Han (Apr 06 2021 at 12:57):

gptf is often faster than library_search :robot:


Last updated: May 18 2021 at 09:14 UTC