文件名称：lean-gptf:精益互动神经定理证明
文件大小：26KB
文件格式：ZIP
更新时间：2024-05-28 04:14:14
Lean
精益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
【文件预览】：
lean-gptf-master
----src()
--------tactic()
--------basic()
--------example.lean(2KB)
----leanpkg.toml(242B)
----LICENSE(11KB)
----README.md(3KB)
----.gitignore(37B)