Rudimentary Proof search step using "first tactic" prompts

[siddhartha-gadgil]

Overview

• Key observation: Even though internal tactic states are not exposed to Codex, the first tactic in each theorem or lemma is part of the source. This should be a reasonably large number.
• So we can build a model as with translation by encoding the current tactic state as a theorem statement, with the local context giving the arguments and the goal giving the statement.
• We can then find nearby statements from a database as examples in the prompt, and ask for the next tactic. Building such a database may be reasonably easy.

Implementation

Some of these steps have been tried out in Fiddle.lean and some others are like previous code.

• Extract theorems and first tactics (where the proof is in tactic mode) in context from given Lean files.
  • [x] we need a parser that matches defs. theorems and lemmas proved/defined in tactic mode and extracts components, including the first tactic
  • [x] to deduce the context we also need parsers for sections and variables, and should deduce the context when a theorem is parsed.
  • [x] in the case of structured application of induction and cases, we get a very long tactic; this should be replaced by just induction n or equivalent (warning: there can be multiple variables).
• [x] given a local context in tactic mode, have a tactic generating a theorem statement.
• [x] list lean files in a given folder and extract the data from these.
• [x] implement storing and pickling embeddings and querying for sentence similarity.
• [x] have an appropriate first effective tactic based on a list of strings.

[siddhartha-gadgil]

We may want to use something other than sentence similarity for these, perhaps keyword matching based on identifiers.

[siddhartha-gadgil]

To trace bug, in mathlib4/Mathlib/Data/Finset/Basic.lean have "index out of bounds"

[siddhartha-gadgil]

To avoid the above bug, while parsing we must:

• [x] skip comment sections of all forms
• [x] if the first character of the unparsed tail is a letter, drop all letters begging with that.

[siddhartha-gadgil]

This is implemented in 68cb6613c2c621ffc5 with a switch to a smaller but correct database in 1769432f69151d08