issues
search
lean-dojo
/
ReProver
Retrieval-Augmented Theorem Provers for Lean
https://leandojo.org
MIT License
196
stars
40
forks
source link
issues
Newest
Newest
Most commented
Recently updated
Oldest
Least commented
Least recently updated
"ValueError: Tensors must be contiguous" when training ReProver (CUDA 12.4)
#66
realharryhero
opened
1 day ago
0
Checkpoints
#64
Adarsh321123
opened
1 week ago
1
Update Checkpoints Format
#63
yangky11
closed
1 week ago
0
Minor fix to remove CI node warning
#61
Peiyang-Song
closed
2 weeks ago
0
feat: decoder-only models
#60
ZIYU-DEEP
closed
1 week ago
1
Unknown package "Mathlib"
#58
hongjin-su
closed
1 month ago
2
Evaluating ReProver without training local checkpoints / Model checkpoints access
#54
Yingjia-Wan
opened
1 month ago
10
Jointly sort theorems and positions in `evaluate.py`
#49
matt-seb-ho
closed
3 months ago
1
Handling of in-file negatives in ReProver
#46
luan-xiaokun
closed
4 months ago
1
Cannot locate premise
#44
zoryzhang
closed
4 months ago
3
Runtime Init Error
#43
ethanlabelle
closed
3 months ago
5
Enabling vllm-based prover
#40
albertqjiang
closed
3 months ago
1
Merge pull request #38 from lean-dojo/main
#39
yangky11
closed
7 months ago
0
sync with dev
#38
yangky11
closed
7 months ago
0
remove tree from SearchResult for efficiency
#37
yangky11
closed
7 months ago
0
update readme
#36
yangky11
closed
7 months ago
0
Don't evaluate during validation
#35
yangky11
closed
7 months ago
0
Retriever embeddings depend on padding
#34
darabos
closed
6 months ago
4
url, hashcode in scripts/download_data.py
#33
irene622
closed
8 months ago
1
The evaluation result on the dataset Minif2f and ProofNet, indexed-corpus-path option
#31
irene622
closed
8 months ago
3
what is the Request GET /repos/facebookresearch/miniF2F failed with 403: rate limit exceeded
#30
irene622
closed
9 months ago
1
Error when running python scripts/trace_repos.py
#29
j991222
closed
9 months ago
2
/bin/sh: 1: lake: not found
#28
mnluzimu
closed
10 months ago
5
Update
#27
yangky11
closed
10 months ago
0
[QUESTION, BUG] all theorem are discarded when using miniF2F
#26
irene622
closed
9 months ago
8
When evaluation done, add case which all theorem is discarded. Modify num_gpus in ray.init
#24
irene622
closed
10 months ago
4
How to apply the dataset, miniF2F to ReProver?
#23
irene622
closed
10 months ago
1
Parser tactic state using LeanDojo parser
#21
antonkov
closed
1 year ago
0
Consider publishing datasets on HuggingFace
#19
SamPruden
closed
1 year ago
3
Publish datasets on HuggingFace
#18
SamPruden
closed
1 year ago
1
Format state_before/state_after datapoints as partial updates
#17
antonkov
closed
1 year ago
8
DeepSpeed checkpoints for the retreiver?
#15
bollu
closed
1 year ago
2
Deduplicate (url, commits) pairs before checking LeanGitRepo in cache to speed up trace_repos.py
#14
antonkov
closed
1 year ago
4
add tac_dix
#13
yangky11
closed
1 year ago
0
Generator conditioned on retriever
#12
yangky11
closed
1 year ago
0
Fix the problem with loading checkpoints
#11
yangky11
closed
1 year ago
0
Prover
#10
yangky11
closed
1 year ago
0
Prover
#9
yangky11
closed
1 year ago
0
treat ProofGivenUp as error in proof search
#8
yangky11
closed
1 year ago
0
fix
#7
yangky11
closed
1 year ago
0
minor fix
#6
yangky11
closed
1 year ago
0
Prover
#5
yangky11
closed
1 year ago
0
add context
#4
yangky11
closed
1 year ago
0
save validation outputs
#3
yangky11
closed
1 year ago
0
Prover
#2
yangky11
closed
1 year ago
0
Prover
#1
yangky11
closed
1 year ago
0