Stream: lean-gptf

Topic: using gptf on olympiad problems

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

David Renshaw (Apr 06 2021 at 02:10):

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

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]}


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?

David Renshaw (Apr 06 2021 at 12:01):

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

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.

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.

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.

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)".

David Renshaw (Apr 06 2021 at 12:16):

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

Kevin Buzzard (Apr 06 2021 at 12:23):

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

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”.

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