{"payload":{"pageCount":3,"repositories":[{"type":"Public","name":"batteries","owner":"leanprover-community","isFork":false,"description":"The \"batteries included\" extended library for the Lean programming language and theorem prover","allTopics":["lean","lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":66,"issueCount":28,"starsCount":236,"forksCount":99,"license":"Apache License 2.0","participation":[0,3,11,16,12,20,6,24,14,6,12,28,13,8,13,14,12,12,19,30,24,4,5,3,6,12,6,1,6,11,9,8,9,5,4,3,10,10,4,4,6,3,5,2,5,4,13,4,5,12,0,4],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-25T01:30:35.788Z"}},{"type":"Public","name":"mathlib4","owner":"leanprover-community","isFork":false,"description":"The math library of Lean 4","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1097,"issueCount":224,"starsCount":1394,"forksCount":310,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-25T01:26:31.076Z"}},{"type":"Public","name":"aesop","owner":"leanprover-community","isFork":false,"description":"White-box automation for Lean 4","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":19,"starsCount":189,"forksCount":26,"license":"Apache License 2.0","participation":[12,5,2,5,5,2,3,8,0,2,0,0,2,0,2,0,18,17,9,9,16,14,2,1,1,1,2,1,1,0,0,3,3,0,17,9,14,14,13,11,7,1,0,4,6,3,2,5,12,6,7,4],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-24T20:28:15.048Z"}},{"type":"Public","name":"leanprover-community.github.io","owner":"leanprover-community","isFork":false,"description":"Hosts the website for mathlib and other Lean community infrastructure.","allTopics":[],"primaryLanguage":{"name":"CSS","color":"#563d7c"},"pullRequestCount":10,"issueCount":21,"starsCount":51,"forksCount":119,"license":"MIT License","participation":[3,2,10,16,1,8,4,0,10,7,1,4,0,6,32,2,4,0,4,1,3,1,5,1,0,1,0,0,2,4,9,1,3,2,1,4,1,2,3,1,2,0,23,3,2,0,1,5,2,3,1,3],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-24T13:01:29.488Z"}},{"type":"Public","name":"mathlib_stats","owner":"leanprover-community","isFork":false,"description":"Display gitstats output on the mathlib website","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":5,"license":null,"participation":[7,7,7,13,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,7,11,7,7,7,7,7,7,7,6,7,7,5,7,7,7,7,7,7,7,7,7,7,7,7,7],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-24T02:27:19.618Z"}},{"type":"Public","name":"lean-auto","owner":"leanprover-community","isFork":false,"description":"Experiments in automation for Lean","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":8,"starsCount":66,"forksCount":10,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-23T18:38:48.477Z"}},{"type":"Public","name":"lean4web","owner":"leanprover-community","isFork":false,"description":"The Lean 4 web editor","allTopics":["lean4"],"primaryLanguage":{"name":"TypeScript","color":"#3178c6"},"pullRequestCount":0,"issueCount":6,"starsCount":64,"forksCount":17,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-23T18:31:04.013Z"}},{"type":"Public","name":"con-nf","owner":"leanprover-community","isFork":false,"description":"A formal consistency proof of Quine's set theory New Foundations","allTopics":["set-theory","lean4","new-foundations"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":1,"starsCount":57,"forksCount":4,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-23T14:55:32.230Z"}},{"type":"Public","name":"quote4","owner":"leanprover-community","isFork":false,"description":"Intuitive, type-safe expression quotations for Lean 4.","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":5,"issueCount":13,"starsCount":73,"forksCount":11,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-23T12:09:39.907Z"}},{"type":"Public","name":"LeanSearchClient","owner":"leanprover-community","isFork":false,"description":"Syntax for searching with natural language from Lean, using <a href=\"https://leansearch.net/\" rel=\"nofollow\">https://leansearch.net/</a> (may extend to other services)","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":1,"starsCount":6,"forksCount":3,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-19T10:50:02.816Z"}},{"type":"Public","name":"blog","owner":"leanprover-community","isFork":false,"description":"Source for the community blog","allTopics":[],"primaryLanguage":{"name":"Python","color":"#3572A5"},"pullRequestCount":7,"issueCount":5,"starsCount":6,"forksCount":19,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-18T00:13:44.532Z"}},{"type":"Public","name":"flt-regular","owner":"leanprover-community","isFork":false,"description":"Fermat's Last Theorem for regular primes","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":50,"forksCount":3,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-17T07:57:14.991Z"}},{"type":"Public","name":"mathematics_in_lean","owner":"leanprover-community","isFork":false,"description":"The user home repository for the Mathematics in Lean tutorial.","allTopics":[],"primaryLanguage":{"name":"HTML","color":"#e34c26"},"pullRequestCount":0,"issueCount":0,"starsCount":241,"forksCount":179,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-08T21:11:05.335Z"}},{"type":"Public","name":"lean4game","owner":"leanprover-community","isFork":false,"description":"Server to host lean games.","allTopics":["react","lean4"],"primaryLanguage":{"name":"TypeScript","color":"#3178c6"},"pullRequestCount":3,"issueCount":69,"starsCount":174,"forksCount":29,"license":"GNU General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-07T18:15:16.692Z"}},{"type":"Public","name":"import-graph","owner":"leanprover-community","isFork":false,"description":"Tool to analyse the import structure of lean projects.","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":1,"starsCount":7,"forksCount":4,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-06T15:24:16.586Z"}},{"type":"Public","name":"sphere-eversion","owner":"leanprover-community","isFork":false,"description":"Formalization of the existence of sphere eversions","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":35,"forksCount":10,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-06T08:57:22.339Z"}},{"type":"Public","name":"mathlib4_docs","owner":"leanprover-community","isFork":false,"description":"","allTopics":["lean4"],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":7,"forksCount":2,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-06T08:50:50.584Z"}},{"type":"Public","name":"logic_and_proof","owner":"leanprover-community","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"TeX","color":"#3D6117"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":1,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-04T18:21:29.772Z"}},{"type":"Public","name":"repl","owner":"leanprover-community","isFork":false,"description":"A simple REPL for Lean 4, returning information about errors and sorries.","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":2,"issueCount":9,"starsCount":68,"forksCount":15,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-03T06:49:51.977Z"}},{"type":"Public","name":"ProofWidgets4","owner":"leanprover-community","isFork":false,"description":"Helper toolkit for creating your own Lean 4 UserWidgets","allTopics":["lean","lean4","visualization"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":3,"issueCount":13,"starsCount":103,"forksCount":24,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-09-03T04:35:46.425Z"}},{"type":"Public","name":"duper","owner":"leanprover-community","isFork":false,"description":"","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":46,"forksCount":8,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-30T04:56:47.604Z"}},{"type":"Public","name":"lean4-metaprogramming-book","owner":"leanprover-community","isFork":false,"description":"","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":4,"issueCount":17,"starsCount":211,"forksCount":51,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-29T11:41:23.020Z"}},{"type":"Public","name":"NNG4","owner":"leanprover-community","isFork":false,"description":"Natural Number Game","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":13,"starsCount":102,"forksCount":32,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-28T21:51:30.240Z"}},{"type":"Public","name":"iris-lean","owner":"leanprover-community","isFork":false,"description":"Lean 4 port of Iris, a higher-order concurrent separation logic framework","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":3,"starsCount":63,"forksCount":5,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-20T06:45:50.919Z"}},{"type":"Public","name":"lean4-mode","owner":"leanprover-community","isFork":false,"description":"Emacs major mode for Lean 4","allTopics":["emacs","lean4"],"primaryLanguage":{"name":"Emacs Lisp","color":"#c065db"},"pullRequestCount":6,"issueCount":22,"starsCount":64,"forksCount":27,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-19T18:17:16.437Z"}},{"type":"Public","name":"mathport","owner":"leanprover-community","isFork":false,"description":"Mathport is a tool for porting Lean3 projects to Lean4","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":4,"issueCount":33,"starsCount":41,"forksCount":15,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-13T19:32:07.543Z"}},{"type":"Public","name":"mathlib3port","owner":"leanprover-community","isFork":false,"description":"Synport output from mathport for mathlib3","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":11,"forksCount":5,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-13T06:53:57.635Z"}},{"type":"Public","name":"lean3port","owner":"leanprover-community","isFork":false,"description":"Stub for downloading mathport artifacts for Lean 3","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":4,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-08-13T06:53:04.968Z"}},{"type":"Public","name":"llm","owner":"leanprover-community","isFork":false,"description":"Interfacing with Large Language Models (remote and local) from Lean.","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":23,"forksCount":1,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-15T18:40:02.259Z"}},{"type":"Public","name":"lean-perfectoid-spaces","owner":"leanprover-community","isFork":false,"description":"Perfectoid spaces in the Lean formal theorem prover.","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":3,"issueCount":6,"starsCount":115,"forksCount":13,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-09T11:17:21.271Z"}}],"repositoryCount":68,"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":"leanprover-community repositories"}