Improve keyword-based prompting

[0art0]

• [ ] Collect an extensive list of mathematical keywords
• [ ] Handle synonymous keywords (Isomorphism, isomorphism, isomorphisms and isomorphic are all considered the same)
• [ ] Extract keywords from mathlib docstrings and backtranslated statements and group mathlib statements by keywords
• [ ] Organise and store the mathlib keyword data for efficient search
• [ ] Allow for a custom database of statements and keywords in addition to mathlib
• [ ] Design heuristics for selecting statements with a given set of keywords
• [ ] Allow for this to be used as a standalone tool

[siddhartha-gadgil]

@0art0 Perhaps lemmatization (https://en.wikipedia.org/wiki/Lemmatisation) may be useful, using something like Wordnet (I don't know if there are modern versions of this based on LLMs).

[0art0]

• [x] Compute the embeddings of all mathematical keywords from Wiktionary and store them.
• [x] Following https://towardsdatascience.com/keyword-extraction-with-bert-724efca412ea (as suggested by @siddhartha-gadgil), attempt keyword extraction by computing similarity between the input sentence and potential keywords.
• [ ] If the results are reasonable, experiment again with a larger keyword set comprising all mathematics-related Wikipedia titles (using this script)
• [ ] Retain only those keywords that occur in the database of sentences for input-dependent prompting (prompts.json)
• [ ] Compute and store the keyword data for all sentences in the database, using the restricted set of keywords.
• [ ] Create a pipeline for keyword-based prompting.

[0art0]

As identifier-based prompting may be useful in other contexts, the infrastructure for keyword-based prompting should ideally be abstract enough to handle prompting of this general nature.

[siddhartha-gadgil]

Models are changing and this part has lower priority. Reopen if focussed on this.