feat: #formalize, backed by a choice of LLMs

[semorrison]

This replaces

• feat: interface for ChatGPT #3785, which has essentially been moved to an independent repository and generalised to interface with a choice of OpenAI's GPT, a gpt4all model (running locally via their python binding), or a model compatible with llama.cpp (e.g. the 4-bit quantised versions of Meta's LLaMa models).
• feat: #formalize, backed by GPT #3786, which has been modified slightly but still adds code here in Mathlib.Tactic.Formalize.

Typical output:

#formalize "There are infinitely many primes numbers ending with a 7."

produces:

• GPT4

-- /-- There are infinitely many prime numbers ending with a 7. -/
-- theorem infinitely_many_primes_ending_with_7 : ∀ N : Nat, ∃ p, N < p ∧ p.Prime ∧ p % 10 = 7 :=
--   sorry

• ggml-gpt4all-j-v1.3-groovy.bin:

-- There are infinitely many prime numbers that end with a 7.

• 7B/ggml-model-q4_0.bin:

-- ∀ p : nat, 7 < 7p + 1 := sorry
-– \end{code}

There are other sample outputs in test/formalize.lean

If you don't currently have a LLM that the leanprover-community/llm project can recognise, when you run #formalize you get an error message, which currently reads:

Could not find a usable chat bot!

You can try one of the following:
* Obtain an OpenAI API access key at https://platform.openai.com/account/api-keys,
  and store it in the environment variable OPENAI_API_KEY.
  This will enable you to use ChatGPT.
* Download the GPT4All-J model `https://gpt4all.io/models/ggml-gpt4all-j-v1.3-groovy.bin`,
  and put it in either `$HOME/.models/` or `$LLM_MODELS`.
  Also install the gpt4all python bindings via `pip3 install pygpt4all`.
* Clone the `llama.cpp` repository from https://github.com/ggerganov/llama.cpp.
  Set the environment variable `LLAMA_CPP_HOME` to this repository.
  Follow the instructions in the README to produce `7B/ggml-model-q4_0.bin`
  starting from the Meta LLaMa weights.
  You can store this file at one of
  * `$LLAMA_CPP_HOME/models/7B/ggml-model-q4_0.bin`
  * `$HOME/.models/7B/ggml-model-q4_0.bin`
  * `$LLM_MODELS/7B/ggml-model-q4_0.bin`

Currently there are not user-configurable hooks to pick which LLM to use: it checks the conditions described in those bullet points, and takes the first one it finds. (i.e. if you want to use the LLaMa 7B/ggml-model-q4_0.bin, you have to remove your OpenAI API key!). However a tactic in a downstream project (e.g. mathlib) can specify which interface and model it wants to use, or just call findChatBot for the behaviour described in that message.

---

[jcommelin]

Would it make sense to make the #formalize command part of the llm package, so that other projects can use it without depending on mathlib?