using gptf on olympiad problems

Stream: lean-gptf

[David Renshaw]

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

[David Renshaw]

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

[David Renshaw]

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]

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

[David Renshaw]

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

[David Renshaw]

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]

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]

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]

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]

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

[Kevin Buzzard]

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

[Jason Rute]

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

[Jesse Michael Han]

gptf is often faster than library_search :robot: