New model

Stream: lean-gptf

[Jesse Michael Han]

Hello everybody, we found a way to train a noticeably better (and smaller) model, now available as the default engine formal-large-lean-0119-mix-v1-c4 in the lean-gptf beta. It drove the dozen new PRs we merged yesterday and we're excited to have you guys try it out!

Also, now that mathlib has been bumped to 3.26.0, I have bumped lean-gptf to use 3.26.0 and thus it should be much easier to just add lean-gptfas a dependency to your own project and try using the gptf tactic there. Note, it has only been trained on 80% of a mathlib from 1 month ago, but it would be really interesting to see how well it can generalize to new domains/projects.

[Jesse Michael Han]

The new model is, strangely enough, very fond of using semicolons. It synthesized the following proof of list.kunion_kerase in a single shot:

example {α : Type u} {β : α → Type v} [_inst_1 : decidable_eq α] {a : α} {l₁ l₂ : list (sigma β)} :
  (list.kerase a l₁).kunion (list.kerase a l₂) = list.kerase a (l₁.kunion l₂) :=
begin
  induction l₁ with x xs generalizing l₂; cases l₂ with y ys; simp
end

[Jesse Michael Han]

(the proof of this theorem did not appear in training data)

[Stanislas Polu]

Deleted model formal-3b-lean-webmath-1230-v2-c4 which predated the current one formal-large-lean-0119-mix-v1-c4, in preparation for the release of a new model. If you get errors related to formal-3b-lean-webmath-1230-v2-c4 please update to master (and please don't hesitate to reach out!)