{"payload":{"pageCount":1,"repositories":[{"type":"Public","name":"LeanCopilot","owner":"lean-dojo","isFork":false,"description":"LLMs as Copilots for Theorem Proving in Lean","allTopics":["machine-learning","theorem-proving","lean","formal-mathematics","lean4","llm-inference"],"primaryLanguage":{"name":"C++","color":"#f34b7d"},"pullRequestCount":0,"issueCount":4,"starsCount":834,"forksCount":70,"license":"MIT License","participation":[0,0,0,0,0,0,0,0,0,0,0,30,13,131,20,9,0,9,33,10,0,47,33,15,40,75,66,3,2,0,1,20,5,5,1,0,1,0,8,2,0,3,10,0,0,1,1,0,6,3,16,0],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-29T06:18:34.504Z"}},{"type":"Public","name":"LeanDojo","owner":"lean-dojo","isFork":false,"description":"Tool for data extraction and interacting with Lean programmatically.","allTopics":["machine-learning","theorem-proving","lean","lean4"],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":1,"issueCount":2,"starsCount":462,"forksCount":66,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-28T03:12:04.843Z"}},{"type":"Public","name":"LeanDojoWebsite","owner":"lean-dojo","isFork":false,"description":"Code for LeanDojo's website","allTopics":["machine-learning","theorem-proving","lean"],"primaryLanguage":{"name":"JavaScript","color":"#f1e05a"},"pullRequestCount":0,"issueCount":0,"starsCount":7,"forksCount":1,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-26T08:15:47.417Z"}},{"type":"Public","name":"ReProver","owner":"lean-dojo","isFork":false,"description":"Retrieval-Augmented Theorem Provers for Lean","allTopics":["machine-learning","theorem-proving","lean"],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":1,"starsCount":179,"forksCount":34,"license":"MIT License","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-10T20:50:59.210Z"}},{"type":"Public","name":"LeanDojoChatGPT","owner":"lean-dojo","isFork":false,"description":"ChatGPT plugin for theorem proving in Lean","allTopics":["machine-learning","lean","theorem","large-language-models","chatgpt","chatgpt-plugin"],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":100,"forksCount":13,"license":"MIT License","participation":[0,1,3,0,4,2,0,0,0,0,0,0,0,0,0,0,0,0,0,1,1,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0,0,0,0,0,1,0,0,0,0,0,0,0,0,0],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-04T01:18:26.000Z"}}],"repositoryCount":5,"userInfo":null,"searchable":true,"definitions":[],"typeFilters":[{"id":"all","text":"All"},{"id":"public","text":"Public"},{"id":"source","text":"Sources"},{"id":"fork","text":"Forks"},{"id":"archived","text":"Archived"},{"id":"template","text":"Templates"}],"compactMode":false},"title":"Repositories"}