Skip to content

Issues: leanprover-community/lean4game

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

86 Open 159 Closed
86 Open 159 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

NewHiddenTactics give “Missing Tactic Documentation” warning fixed on dev Will be part of the next update
#300 opened Feb 25, 2025 by TentativeConvert
Can we distinguish apply? from apply enhancement New feature or request priority-medium should be addressed within the next months
#299 opened Feb 25, 2025 by TentativeConvert
1
Running games locally using devcontainer gives "permission denied" error bug Something isn't working priority-high address ASAP
#296 opened Feb 23, 2025 by platypus999
2
Allow multiple hidden hints enhancement New feature or request priority-low nice to have
#294 opened Feb 21, 2025 by TentativeConvert
Move Definitions into same Tabs as Theorems enhancement New feature or request fixed on dev Will be part of the next update
#293 opened Feb 21, 2025 by TentativeConvert
3
Cannot create edge with nonexistant world, but game builds successfully fixed on dev Will be part of the next update
#292 opened Feb 14, 2025 by JadAbouHawili
3
Deployment with Docker Compose
#289 opened Feb 9, 2025 by aziis98
1
Incompatible with LeanCopilot bug Something isn't working priority-low nice to have
#286 opened Jan 26, 2025 by joneugster
complement superscript shows squares on Android
#278 opened Jan 7, 2025 by bsdz
Point and click interface ideal for volunteers Feature request which should make for a good isolated project. Currently out-of-scope/unclaimed
#277 opened Jan 5, 2025 by miguelmarco
1
Level completed with warnings? bug Something isn't working
#276 opened Dec 27, 2024 by Timmmm
2
Extra help for 0 * m = m bug Something isn't working
#275 opened Dec 26, 2024 by Timmmm
2
There is no responsive answer from the game after executing command bug Something isn't working
#273 opened Nov 9, 2024 by yourcomrade
2
Suggestion: Dependencies throw an error if there is a missing world.
#272 opened Oct 27, 2024 by Louw123
Don't show locked items in inventory.
#265 opened Oct 10, 2024 by miguelmarco
4
have a hypothesis that has multiple premises
#264 opened Oct 5, 2024 by Qinggao1729
1
Building issue
#263 opened Oct 5, 2024 by kant2002
3
fix filtering of "unsolved goal" error bug Something isn't working
#257 opened Aug 18, 2024 by joneugster
Failed to Configure mathlib Dependency for GlimpseOfLean in lean4game bug Something isn't working priority-high address ASAP
#256 opened Aug 17, 2024 by RexWzh
1
Delete tmp games client Functionality of the client side code enhancement New feature or request priority-medium should be addressed within the next months
#255 opened Aug 13, 2024 by joneugster
1
Struggling to run games locally manually
#254 opened Jul 28, 2024 by ndcroos
4
Does this game have hints for new beginner ?
#252 opened Jul 19, 2024 by geraltgod
4
Website Translation from German to English fails on Robo wontfix This will not be worked on
#247 opened Jul 3, 2024 by AMindToThink
2
feat: inventory of cheat sheets/summaries in addition to tactics, definitions and theorems enhancement New feature or request wontfix This will not be worked on
#246 opened Jul 1, 2024 by TentativeConvert
1
feat: navigation buttons "previous lemma", "next lemma" in inventory enhancement New feature or request
#245 opened Jul 1, 2024 by TentativeConvert
ProTip! Type g p on any issue or pull request to go back to the pull request listing page.