Question about released checkpoint split strategy

[mikeljl]

Hi, thanks for the great work on LeanDojo!

Could you clarify what data split was used to train the released checkpoint(tactic generator and premise retriever) on huggingface? Was it trained on the random split, the novel premises split, or all data?

Thanks a lot!