Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

LeanCopilot + MathLib #126

Open
math-ai-meetup opened this issue Oct 6, 2024 · 0 comments
Open

LeanCopilot + MathLib #126

math-ai-meetup opened this issue Oct 6, 2024 · 0 comments

Comments

@math-ai-meetup
Copy link

Hello team and thank you for the wonderful project!

I am trying to get LeanCopilot running alongside MathLib. I suspect the issue is with version compatibility.

For example, if I start with this project and then follow this guide to add MathLib to an existing project, everything fails.

I noticed that installing MathLib automatically updates lean-toolchain from leanprover/lean4:v4.11.0 to leanprover/lean4:v4.13.0-rc3 and the latter is not supported by LeanCopilot.

Is there an easy fix for this?

Again, awesome project and apologies for annoying questions!

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant