本仓库包含了一款基于 Lean 4 与 Julia 混合开发的智能定理证明辅助系统。前端深度集成于 Lean 4 编辑器,能实时调用大模型生成证明战术并在后台进行沙箱静默验证;后端依托 Julia 构建了轻量级通信网关与 Web 可视化启动器,支持一键无缝切换 DeepSeek、Ollama 等云端或本地模型,实现了形式化验证与底层 AI 算力的高效解耦。
-
Notifications
You must be signed in to change notification settings - Fork 0
GaoMath/Julia-Lean
Folders and files
| Name | Name | Last commit message | Last commit date | |
|---|---|---|---|---|
Latest commit | ||||
Repository files navigation
About
一款基于 Lean 4 与 Julia 混合开发的智能定理证明辅助系统。前端深度集成于 Lean 4 编辑器,能实时调用大模型生成证明战术并在后台进行沙箱静默验证;后端依托 Julia 构建了轻量级通信网关与 Web 可视化启动器,支持一键无缝切换 DeepSeek、Ollama 等云端或本地模型,实现了形式化验证与底层 AI 算力的高效解耦。
Resources
License
Stars
Watchers
Forks
Releases
No releases published