Discussions

• 1 You must be logged in to vote

  🙏

  Traced repos in the remote cache

  zoryzhang asked Mar 17, 2024 in Q&A · Closed · Answered

  

  

  2
• 2 You must be logged in to vote

  🙏

  LeanDojo as REPL for online RL

  matt-seb-ho asked Apr 18, 2024 in Q&A · Unanswered

  

  

  

  

  9
• 1 You must be logged in to vote

  🙏

  Using LeanDojo in Google Colab

  ZIYU-DEEP asked Apr 10, 2024 in Q&A · Answered

  

  

  5
• 1 You must be logged in to vote

  🙏

  How to keep dojo alive even when a DojoCrashError is raised

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

  

  

  2
• 1 You must be logged in to vote

  🙏

  Which specific Lean version will leandojo use?

  wclsn asked Mar 26, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Getting States from a Theorem without Tracing

  princesspeace asked Mar 6, 2024 in Q&A · Unanswered

  

  

  3
• 4 You must be logged in to vote

  🙏

  In structured proof, how to focus on a specific goal in interaction mode

  subfish-zhou asked Mar 11, 2024 in Q&A · Answered

  

  

  6
• 1 You must be logged in to vote

  🙏

  trace depository error

  Moyvbai asked Dec 29, 2023 in Q&A · Answered

  

  

  3
• 1 You must be logged in to vote

  💬

  Finetuing CodeLLaMA on LeanDojo

  Some-random started Jul 4, 2023 in General

  

  

  

  

  15
• 1 You must be logged in to vote

  🙏

  Will LeanDojo Tolerate Theorems That Cannot Be Compiled?

  tangzhy asked Jan 26, 2024 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Questions about extracted benchmark dataset in Lean 3

  wiio12 asked Dec 19, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Failed to register worker 01000000ffffffffffffffffffffffffffffffffffffffffffffffff to Raylet. IOError: [RayletClient] Unable to register worker with raylet. No such file or directory

  parsifal-chx asked Nov 29, 2023 in Q&A · Answered

  

  

  11
• 1 You must be logged in to vote

  🙏

  subprocess.CalledProcessError: Command 'lake build Lean4Repl' returned non-zero exit status 1.

  parsifal-chx asked Nov 29, 2023 in Q&A · Answered

  

  

  

  

  16
• 1 You must be logged in to vote

  🙏

  Questions: What is purposes of file_path and full_name in LeanGitRepo, and what is the pp in TacticState?

  irene622 asked Dec 7, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  💬

  Why are the premises from the same file not listed as such?

  josojo started Nov 3, 2023 in General · Closed

  

  

  3
• 1 You must be logged in to vote

  🙏

  Interact with relp without project

  kaifronsdal asked Oct 19, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  💬

  Project structure

  josojo started Sep 23, 2023 in General

  

  

  7
• 1 You must be logged in to vote

  💬

  Execution errors

  josojo started Sep 1, 2023 in General

  

  

  13
• 1 You must be logged in to vote

  🙏

  Is it possible to build a google colab for Lean Dojo?

  brando90 asked Oct 2, 2023 in Q&A · Answered

  

  

  2
• 1 You must be logged in to vote

  🙏

  What is the best way to evaluate theorems and proofs generated by a LLM in LeanDojo?

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

  

  

  4
• 1 You must be logged in to vote

  🙏

  15 second Lean 3 startup time

  darabos asked Sep 21, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  Extracted data in hugging face?

  brando90 asked Sep 13, 2023 in Q&A · Answered

  

  

  1
• 1 You must be logged in to vote

  🙏

  使用LeanDojo 我需要自己训练 ReProver 吗？

  aifuqiang02 asked Jul 24, 2023 in Q&A · Answered

  

  

  1
• 2 You must be logged in to vote

  💬

  Getting Intermediate States from Combined Tactics

  AG161 started Jul 9, 2023 in General

  

  

  

  

  9