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