{"payload":{"pageCount":2,"repositories":[{"type":"Public","name":"mathlib4","owner":"leanprover-community","isFork":false,"description":"The math library of Lean 4","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":990,"issueCount":219,"starsCount":1184,"forksCount":257,"license":"Apache License 2.0","participation":[128,86,141,116,129,103,86,127,130,140,83,66,93,90,118,161,138,139,114,102,125,120,117,151,43,189,128,107,124,170,249,172,177,134,114,125,130,88,160,131,153,111,131,127,151,179,166,189,139,165,151,161],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-11T18:41:07.205Z"}},{"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":39,"forksCount":15,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-11T07:38:22.543Z"}},{"type":"Public","name":"aesop","owner":"leanprover-community","isFork":false,"description":"White-box automation for Lean 4","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":18,"starsCount":155,"forksCount":25,"license":"Apache License 2.0","participation":[3,0,3,0,6,6,9,4,2,0,3,12,5,2,7,3,2,3,8,0,2,0,0,2,0,2,1,18,16,9,14,20,5,3,0,0,1,2,0,1,0,0,3,3,4,13,11,14,13,12,12,6],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-10T13:02:12.093Z"}},{"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":[19,33,2,1,0,0,0,0,5,2,5,11,2,2,14,0,4,5,18,53,73,7,4,4,0,7,2,4,2,4,3,3,1,4,1,4,0,1,1,3,2,1,10,1,0,1,2,1,2,3,14,5],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-10T09:44:05.991Z"}},{"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":76,"issueCount":27,"starsCount":220,"forksCount":89,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-11T15:54:57.672Z"}},{"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":1,"starsCount":35,"forksCount":10,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-08T20:52:12.339Z"}},{"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":1,"issueCount":1,"starsCount":56,"forksCount":2,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-09T19:34:03.198Z"}},{"type":"Public","name":"lean-auto","owner":"leanprover-community","isFork":false,"description":"Experiments in automation for Lean","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":6,"starsCount":60,"forksCount":10,"license":"Apache License 2.0","participation":[28,18,27,19,14,34,38,30,16,12,16,29,19,36,19,22,24,21,2,1,0,6,3,0,0,5,4,1,2,3,1,14,0,0,3,2,0,0,4,4,9,1,5,0,28,0,0,0,0,3,1,0],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-10T06:16:48.477Z"}},{"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":0,"starsCount":6,"forksCount":3,"license":"Apache License 2.0","participation":[0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,0,5,7,0,6,0,0,0,2,3,0,0,1,0,2,3,1,1,0,0,0,8,8,0,1,2,2,3,0,6,8],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-09T22:45:14.593Z"}},{"type":"Public","name":"duper","owner":"leanprover-community","isFork":false,"description":"","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":45,"forksCount":8,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-08T07:38:16.764Z"}},{"type":"Public","name":"NNG4","owner":"leanprover-community","isFork":false,"description":"Natural Number Game","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":12,"starsCount":87,"forksCount":31,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-04T15:17:02.240Z"}},{"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-07-01T08:25:40.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-07-01T08:24:48.968Z"}},{"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":1,"issueCount":8,"starsCount":54,"forksCount":14,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-01T05:13:16.976Z"}},{"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":3,"issueCount":11,"starsCount":70,"forksCount":10,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-01T02:30:32.232Z"}},{"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":12,"starsCount":94,"forksCount":22,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-01T01:25:03.053Z"}},{"type":"Public","name":"mathlib","owner":"leanprover-community","isFork":false,"description":"Lean 3's obsolete mathematical components library: please use mathlib4","allTopics":["theorem-proving","lean","formal-methods","formal-mathematics","proof-automation","formal-proofs"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":283,"issueCount":92,"starsCount":1664,"forksCount":297,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-06-28T02:36:34.050Z"}},{"type":"Public","name":"byte-slice","owner":"leanprover-community","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-06-05T00:52:43.566Z"}},{"type":"Public","name":"lean4-metaprogramming-book","owner":"leanprover-community","isFork":false,"description":"","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":8,"issueCount":17,"starsCount":203,"forksCount":46,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-07-04T18:00:17.878Z"}},{"type":"Public","name":"tutorials4","owner":"leanprover-community","isFork":false,"description":"Lean 4 tutorial files","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":0,"starsCount":23,"forksCount":3,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-03T16:46:45.468Z"}},{"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":0,"issueCount":3,"starsCount":63,"forksCount":4,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-02-20T14:26:06.317Z"}},{"type":"Public","name":"lean-liquid","owner":"leanprover-community","isFork":false,"description":"💧 Liquid Tensor Experiment","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":2,"issueCount":6,"starsCount":162,"forksCount":12,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-23T02:00:42.028Z"}},{"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":22,"forksCount":0,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-05T02:59:55.779Z"}},{"type":"Public","name":"merge-queue-test","owner":"leanprover-community","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-11-05T21:18:33.278Z"}},{"type":"Public","name":"lftcm2020","owner":"leanprover-community","isFork":false,"description":"Lean for the Curious Mathematician 2020","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":63,"forksCount":78,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-24T14:46:50.505Z"}},{"type":"Public archive","name":"lean4-samples","owner":"leanprover-community","isFork":false,"description":"Code samples for Lean 4","allTopics":["lean4"],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":3,"starsCount":67,"forksCount":22,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-19T07:01:06.877Z"}},{"type":"Public archive","name":"tutorials","owner":"leanprover-community","isFork":false,"description":"Some Lean tutorials","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":0,"starsCount":181,"forksCount":61,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-10T21:19:53.443Z"}},{"type":"Public","name":"mathlib4_with_LeanInfer","owner":"leanprover-community","isFork":false,"description":"","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-09-17T06:18:00.852Z"}},{"type":"Public","name":"mathzoo","owner":"leanprover-community","isFork":false,"description":"Lean mathzoo","allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":22,"forksCount":4,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-03-23T22:09:20.367Z"}},{"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":32,"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"}