lean-gptf:精益互动神经定理证明

精益gptf 该存储库使您可以使用GPT-f根据目标状态来建议策略。 当前模型在mathlib （commit 33483a3de6d91066e0fb9efd6aa4c0275d7ac44c ）中的80％战术证明上进行了33483a3de6d91066e0fb9efd6aa4c0275d7ac44c 。 设置 # download pre-built binaries and build the project leanpkg configure && leanpkg build 精益编译完成后，尝试在src/example.lean注释掉证明，并在begin ... end块内调用gptf 。 确保您的API密钥已设置（请参见下文）。 例如， example {α} (a : α) : a = a := begin gptf, end 应该会成功，并显示以下消息： Suc