Skip to content

Issues: lean-dojo/LeanDojo

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.

Sign up for GitHub

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

Clear current search query, filters, and sorts
4 Open 68 Closed
4 Open 68 Closed
Author
Filter by author
Loading
Label
Filter by label
Loading
Use alt + click/return to exclude labels
or ⇧ + click/return for logical OR
Projects
Filter by project
Loading
Milestones
Filter by milestone
Loading
Assignee
Filter by who’s assigned
Sort
Sort by
Newest Oldest Most commented Least commented Recently updated Least recently updated Best match
Most reactions
👍 👎 😄 🎉 😕 ❤️ 🚀 👀

Issues list

check_proof is not giving the desired feedback
#221 by shangetang was closed Feb 12, 2025
1
Questions about data
#220 by yuchen814 was closed Jan 21, 2025
2
Subsequent Tactics on a State Always Result in DojoTacticTimeoutError After an Initial Timeout
#218 by Edmund-Lai was closed Jan 10, 2025
2
problem in 'demo-lean.ipynb'
#217 by yuchen814 was closed Jan 16, 2025
2
Error tracing mathlib4 v4.15.0-rc1
#215 by oOo0oOo was closed Dec 11, 2024
1
hatch publish failed
#214 by yangky11 was closed Dec 24, 2024
1
Are self defined functions considered?
#213 by DDDOH was closed Nov 25, 2024
1
Unicode in data
#209 by timechess was closed Dec 24, 2024
1
I'd like to reopen #183
#208 by Adarsh321123 was closed Nov 14, 2024
1
trace_repo() gives a list index out of error message after storing stuff in cache
#203 by riya-avronna was closed Sep 18, 2024
1
lean_dojo.interaction.dojo.DojoCrashError: Unexpected EOF
#201 by njuyxw was closed Sep 18, 2024
3
Support asyncio for Dojo enhancement New feature or request
#200 by yangky11 was closed Aug 24, 2024
@yangky11
Fix mypy Typing Errors help wanted Extra attention is needed
#196 by yangky11 was closed Oct 28, 2024
2
Unable to find Lean4Repl.lean in the traced repo
#194 by LuoKaiGSW was closed Aug 11, 2024
Failed trace because of lean4 dependency
#193 by Adarsh321123 was closed Aug 21, 2024
3
LeanDojo should not be run as root
#191 by yyyhz was closed Aug 11, 2024
1
Error Loading lean_dojo due to Git Version Parsing Issue[Windows]
#186 by RexWzh was closed Jul 25, 2024
2
Alternative function to LeanGitRepo
#185 by LuoKaiGSW was closed Aug 2, 2024
2
Alternative function to LeanGitRepo
#184 by LuoKaiGSW was closed Jul 20, 2024
Buggy Benchmark Generation
#183 by Adarsh321123 was closed Aug 21, 2024
12
LeanDojo Benchmark 4 Version
#182 by Adarsh321123 was closed Jul 16, 2024
Errors tracing older repos
#177 by AG161 was closed Jul 30, 2024
6
Do we have a script to reproduce the numbers in the paper?
#172 by hongjin-su was closed Jun 24, 2024
1
"Missing $PATH/Main_dep.paths" during tracing of repo
#171 by realharryhero was closed Jun 21, 2024
1
build_lean4_repo.py exit with error
#170 by OctoberFox11 was closed Jun 26, 2024
3
ProTip! Follow long discussions with comments:>50.