search

lean-dojo / LeanCopilot

LLMs as Copilots for Theorem Proving in Lean
https://leandojo.org
MIT License
999 stars 92 forks source link

Bump to latest version of Lean and fix errors introduced by breaking changes #129

Open Peiyang-Song opened 2 weeks ago

Peiyang-Song commented 2 weeks ago

Already fixed Issue #125. Need to fix the error reported by CI (and also Issue #127 which looks related). After that Lean Copilot should be able to to work with latest versions of Lean, thus fixing Issue #126. In the mean time, Lean Copilot v1.6.0 still works and should be treated as the latest stable release of Lean Copilot for now, which works the best with Lean v4.11.0.