Discussions

• 1 You must be logged in to vote

  🙏

  Request for retrievers trained on both random and novel_premises splits

  JobPetrovcic asked Sep 10, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Request to verify evaluation setup for fair performance comparison between ReProver and a custom model on the same test subset

  byrong7 asked Jun 17, 2025 in Q&A · Unanswered

  

  

  0
• 1 You must be logged in to vote

  🙏

  Noob question.The command was not found or executable: lake

  1854039 asked Dec 14, 2024 in Q&A · Unanswered

  

  

  3
• 1 You must be logged in to vote

  🙏

  How to reproduce the results from paper

  monkeytim19 asked May 10, 2024 in Q&A · Answered

  

  

  

  

  6
• 1 You must be logged in to vote

  💬

  Does LeanDojo support for whole proof evaluation instead of a single tactic?

  zengyuzhi started Jul 18, 2024 in General

  

  

  2
• 1 You must be logged in to vote

  🙏

  How to train different model (InternLM-Math) on ReProver dataset other than google/byt5-small?

  realharryhero asked Aug 1, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Downloaded models from huggingface but getting Deepspeed checkpoint loading error

  AndreSlavescu asked May 1, 2024 in Q&A · Closed · Answered

  

  

  

  

  3
• 1 You must be logged in to vote

  🙏

  Converting Hugging Face Safetensor to Checkpoint

  Bojun-Feng asked May 13, 2024 in Q&A · Unanswered

  

  

  

  

  8
• 1 You must be logged in to vote

  🙏

  I want to use the .ckpt files in huggingface, but I face OSerror.

  zengyuzhi asked Jun 17, 2024 in Q&A · Closed · Answered

  

  

  3
• 2 You must be logged in to vote

  🙏

  How to reproduce ReProver training offline?

  laetitia-teo asked Feb 6, 2024 in Q&A · Closed · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  pytorch-lighning_version Error

  jganten asked Jun 21, 2024 in Q&A · Closed · Answered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Errors on loading the checkpoint for indexing the corpus

  Jun-Kai-Zhang asked Jul 1, 2024 in Q&A · Closed · Answered

  

  

  

  

  4
• 1 You must be logged in to vote

  🙏

  Running premise selection using pretrained model/embeddings

  jrr6 asked Jul 12, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  403: rate limit exceeded errors

  joshuaongg21 asked Jun 22, 2024 in Q&A · Answered

  

  

  3
• 2 You must be logged in to vote

  💬

  ReProver fine-tuning

  darabos started Mar 4, 2024 in General

  

  

  1
• 1 You must be logged in to vote

  🙏

  Lean 3 Checkpoints

  sean-lamont asked May 13, 2024 in Q&A · Closed · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Failing to get mathlib4

  AndreSlavescu asked Mar 28, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Handling of in-file negatives in ReProver

  luan-xiaokun asked Mar 20, 2024 in Q&A · Answered

  

  

  2
• 2 You must be logged in to vote

  💬

  How To Locate Premise Definitions

  yangky11 started Mar 16, 2024 in General

  

  

  0
• 2 You must be logged in to vote

  💬

  Is the intention to grow this repo into a useful tool?

  SamPruden started Jul 14, 2023 in General

  

  

  8
• 1 You must be logged in to vote

  🙏

  List of ReProver proofs on benchmarks?

  darabos asked Oct 26, 2023 in Q&A · Answered

  

  

  2
• 1 You must be logged in to vote

  🙏

  Which is the most powerful automation tactic available in Lean, LeanDojo or ReProver

  brando90 asked Sep 18, 2023 in Q&A · Unanswered

  

  

  3
• 1 You must be logged in to vote

  💬

  question about reproducing results from paper

  maverick-harmonic started Jul 27, 2023 in General · Closed

  

  

  6
• 1 You must be logged in to vote

  🙏

  How to get all premises in a random Lean repo?

  Some-random asked Jul 18, 2023 in Q&A · Answered

  

  

  5