Kaiyu Yang
Kaiyu Yang
You could just PR from your own fork.
Which theorem is failing? Can you paste the SMT query displayed in the infoview panel? Most failures are due to the instability of SMT solvers across different platforms or even...
If it's `proposition_1`, it's probably not an SMT issue (only the last few proofs are challenging for SMT). I don't see immediately what the issue is. `¬b = a` shouldn't...
It would be more helpful if the screenshot include complete information. Currently I cannot see which tactic is failing and the exact error message.
I'm not able to reproduce this issue. @loganrjmurphy any idea?
Any update on this?
I updated LeanCopilot to support recent versions of Lean. Could you please re-try and see if the error still persists?
Thanks for noticing that. I'll try to re-run the experiments to see if the encoding makes a difference when I get a chance, though it's currently not our priority.
Hi, I'm not able to reproduce the problem. I tried running `python prover/evaluate.py --data-path data/leandojo_benchmark_4/random/ --gen_ckpt_path kaiyuy/leandojo-lean4-tacgen-byt5-small --split test --num-workers 40 --num-gpus 8` and got the GPU utilization below. It...
How many these messages did you see?