Discussions

• 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 · Unanswered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Failing to get mathlib4

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

  

  

  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

  💬

  ReProver fine-tuning

  darabos started Mar 4, 2024 in General

  

  

  0
• 2 You must be logged in to vote

  🙏

  How to reproduce ReProver training offline?

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

  

  

  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