GitHub / openai/lean-gym issues and pull requests
#34 - Unable to install lean-gym due to outdated mathlib revision
Issue -
State: open - Opened by ctseng777 6 months ago
#33 - Add devcontainer configuration to enable codespace
Pull Request -
State: closed - Opened by ctseng777 6 months ago
#32 - Having trouble init_search miniF2F proofs
Issue -
State: closed - Opened by Some-random about 2 years ago
- 2 comments
#31 - Segmentation fault error
Issue -
State: open - Opened by ayush1801 over 2 years ago
#30 - (Willing to PR) Support multi sub-goals, like what is done in `HyperTree Proof Search for Neural Theorem Proving`
Issue -
State: open - Opened by fzyzcjy over 2 years ago
- 1 comment
#29 - Make scripts fail fast
Pull Request -
State: open - Opened by fzyzcjy over 2 years ago
#28 - fail to setup
Issue -
State: open - Opened by yxliu0903 almost 3 years ago
#27 - How to search a customed theorem with lean-gym?
Issue -
State: open - Opened by liebenxj almost 3 years ago
#26 - How to integrate lean-gym with python?
Issue -
State: open - Opened by venom12138 almost 3 years ago
- 1 comment
#25 - Accessing the Global Environment
Issue -
State: closed - Opened by yangky11 almost 3 years ago
#24 - Decreasing Performance
Issue -
State: open - Opened by todbeibrot about 3 years ago
- 3 comments
#23 - Question about PACT tactic dataset
Issue -
State: closed - Opened by wiio12 about 3 years ago
- 8 comments
#22 - Return error when parse failed without exiting.
Pull Request -
State: closed - Opened by wiio12 over 3 years ago
- 3 comments
#21 - Do not trace with run_tac but do trace otherwise + fix
Pull Request -
State: closed - Opened by spolu over 3 years ago
- 1 comment
#20 - Various fixes and bump mathlib/minif2f
Pull Request -
State: closed - Opened by spolu over 3 years ago
#19 - Remove gptf dependency
Pull Request -
State: closed - Opened by spolu over 3 years ago
- 2 comments
#18 - Shrink
Pull Request -
State: closed - Opened by dselsam over 3 years ago
- 4 comments
#17 - Monad
Pull Request -
State: closed - Opened by Scikud over 3 years ago
- 12 comments
#16 - wip, added tactic to narrow state, tactic to register new lemma
Pull Request -
State: closed - Opened by Scikud almost 4 years ago
#15 - chore(bump mathlib)
Pull Request -
State: closed - Opened by spolu almost 4 years ago
#14 - strengthen `validate_proof`
Pull Request -
State: closed - Opened by jesse-michael-han almost 4 years ago
- 2 comments
#13 - Bump miniF2F to v1
Pull Request -
State: closed - Opened by spolu almost 4 years ago
- 1 comment
#12 - bump miniF2F
Pull Request -
State: closed - Opened by DyeKuu almost 4 years ago
#11 - bump miniF2F
Pull Request -
State: closed - Opened by DyeKuu almost 4 years ago
- 1 comment
#10 - bump mathlib
Pull Request -
State: closed - Opened by spolu about 4 years ago
- 1 comment
#9 - [repl] tentatively fix dangling metavariable issue
Pull Request -
State: closed - Opened by jesse-michael-han about 4 years ago
- 1 comment
#8 - In case of error, capture if there is no goals and succeed instead
Pull Request -
State: closed - Opened by spolu about 4 years ago
- 1 comment
#7 - Proof checks should happen after every tactic
Issue -
State: open - Opened by jasonrute about 4 years ago
- 7 comments
#6 - Check against the use of `undefined`
Pull Request -
State: closed - Opened by spolu about 4 years ago
- 5 comments
#5 - Add checks against `sorry` and proof term type mismath
Pull Request -
State: closed - Opened by spolu about 4 years ago
#4 - [repl] loop forever using `iterate_until`
Pull Request -
State: closed - Opened by jesse-michael-han about 4 years ago
- 1 comment
#3 - Support for `init_search` and `clear_search`
Pull Request -
State: closed - Opened by spolu about 4 years ago
#2 - [util/tactic] use `expr.reduce_let` in `tactic_hash`
Pull Request -
State: closed - Opened by jesse-michael-han about 4 years ago
- 1 comment
#1 - [repl] cleanup using state_t instead of explicit state-passing
Pull Request -
State: closed - Opened by jesse-michael-han about 4 years ago
- 1 comment