{"payload":{"pageCount":1,"repositories":[{"type":"Public","name":"abstract-algebra-template","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-20T08:06:52.254Z"}},{"type":"Public","name":"G12_Myerson-s-Lemma","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-17T14:05:21.729Z"}},{"type":"Public","name":"group3-algebraic_integers_of_Q_adjoin_sqrt_-3_is_PID","owner":"bicmr-ai4math","isFork":false,"description":"BICMR-ai4math 寒假研讨班第3组:algebraic_integers_of_Q_adjoin_sqrt_-3_is_PID","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-04-11T08:13:57.411Z"}},{"type":"Public","name":"Group5_Nine_Point_Circle","owner":"bicmr-ai4math","isFork":false,"description":"寒假讨论班第五组----九点圆","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-31T11:43:43.163Z"}},{"type":"Public","name":"Group_1_JZM_problem","owner":"bicmr-ai4math","isFork":false,"description":"BICMR第一小组五点共圆问题形式化","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-28T03:59:42.019Z"}},{"type":"Public","name":"Group_pq_notSimple-by-lean4","owner":"bicmr-ai4math","isFork":false,"description":"pq阶群非单（p、q为互异素数）","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-26T07:27:46.277Z"}},{"type":"Public","name":"Group13-CLT","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-26T07:07:31.010Z"}},{"type":"Public","name":"Group6-Formalization-on-Lie-algebra-rep","owner":"bicmr-ai4math","isFork":false,"description":"A formalization project for finite dimensional Lie algebra representation","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-26T07:06:33.251Z"}},{"type":"Public","name":"Group4_BFGS_update","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-26T06:27:01.484Z"}},{"type":"Public","name":"Group10-2.13-2.15","owner":"bicmr-ai4math","isFork":false,"description":"problem 2.13/2.15","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-26T06:11:44.334Z"}},{"type":"Public","name":"Group7-3D","owner":"bicmr-ai4math","isFork":false,"description":"BICMR-ai4math 寒假研讨班第七组：一二三维 Lie 代数分类 (三维)","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-25T16:41:33.540Z"}},{"type":"Public","name":"Group7-1D-2D","owner":"bicmr-ai4math","isFork":false,"description":"BICMR-ai4math 寒假研讨班第七组：一二三维 Lie 代数分类 (一维、二维)","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-25T16:40:25.358Z"}},{"type":"Public","name":"group-9-Number-Theory-P1","owner":"bicmr-ai4math","isFork":false,"description":"group-9-Number-Theory-P1","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-25T03:54:04.098Z"}},{"type":"Public","name":"group-0-p-0","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-22T07:33:11.719Z"}},{"type":"Public","name":"bicmr-ai4math.github.io","owner":"bicmr-ai4math","isFork":false,"description":"<a href=\"https://bicmr-ai4math.github.io\" rel=\"nofollow\">https://bicmr-ai4math.github.io</a>","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"TypeScript","color":"#3178c6"},"pullRequestCount":0,"issueCount":0,"starsCount":5,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-01-11T08:55:40.215Z"}},{"type":"Public","name":"lean-simple-mirror","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Shell","color":"#89e051"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-10-14T07:06:11.464Z"}},{"type":"Public","name":"mirror-clone","owner":"bicmr-ai4math","isFork":true,"description":"All-in-one mirror utility for SJTUG mirror","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Rust","color":"#dea584"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":9,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-09-29T10:03:08.362Z"}},{"type":"Public","name":"elan","owner":"bicmr-ai4math","isFork":true,"description":"A Lean version manager","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Rust","color":"#dea584"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":34,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-09-29T09:37:27.332Z"}},{"type":"Public","name":"Operad","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-09-23T14:46:52.700Z"}},{"type":"Public","name":"spectral-sequence","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-20T17:03:22.663Z"}},{"type":"Public","name":"sol-2-9","owner":"bicmr-ai4math","isFork":false,"description":"The repository contains Lean code that implements problem 2-9","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":0,"starsCount":0,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-04T02:58:54.372Z"}},{"type":"Public","name":"sol-2-11","owner":"bicmr-ai4math","isFork":false,"description":"Four lemmas","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-02T16:06:56.846Z"}},{"type":"Public","name":"sol-2-10","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-02T14:53:48.160Z"}},{"type":"Public","name":"sol-2-14","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-02T14:19:14.867Z"}},{"type":"Public","name":"sol-2-16","owner":"bicmr-ai4math","isFork":false,"description":"For positive integers $a, s, t$, prove that $a^{\\mathrm{gcd}(s,t)}-1=\\mathrm{gcd}(a^s-1,a^t-1)$. As a bonus, it can be proven that for any positive integer $n&gt;1$, $n \\nmid 2^n-1$.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-02T12:36:52.376Z"}},{"type":"Public","name":"sol-2-6","owner":"bicmr-ai4math","isFork":false,"description":"for two subgroups H1, H2 of a group G such that H1 ∪ H2 is a subgroup, prove that H1, H2 have mutual inclusion relations","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-02T02:04:52.989Z"}},{"type":"Public","name":"course-invite","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":null,"pullRequestCount":0,"issueCount":0,"starsCount":0,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-01T07:42:54.087Z"}},{"type":"Public","name":"sol-2-19","owner":"bicmr-ai4math","isFork":false,"description":"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":1,"forksCount":3,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-07-31T16:01:10.066Z"}}],"repositoryCount":28,"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"}