{"payload":{"pageCount":2,"repositories":[{"type":"Public","name":"formalising-mathematics-2024","owner":"ImperialCollegeLondon","isFork":false,"description":"Formalising Mathematics; a course for undergraduate mathematicians. Ran between January and March 2024.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":2,"issueCount":0,"starsCount":63,"forksCount":17,"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,0,0,0,9,0,0,0,2,3,10,25,14,19,6,6,0,0,0,0,0,0,0,3,0,0,0,0,0,0,0],"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-05-11T22:41:32.602Z"}},{"type":"Public","name":"formalising-mathematics-2022","owner":"ImperialCollegeLondon","isFork":false,"description":"Lean 3 material for Kevin Buzzard's Jan-Mar 2022 course on formalising mathematics. Lean 4 version available here: <a href=\"https://github.com/ImperialCollegeLondon/formalising-mathematics-2024\">https://github.com/ImperialCollegeLondon/formalising-mathematics-2024</a>","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":118,"forksCount":25,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-09T11:25:34.999Z"}},{"type":"Public","name":"natural_number_game","owner":"ImperialCollegeLondon","isFork":false,"description":"Building the natural numbers in Lean 3. The original natural number game, now frozen. See README for Lean 4 information.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":9,"issueCount":32,"starsCount":289,"forksCount":72,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-09T11:20:04.917Z"}},{"type":"Public","name":"formalising-mathematics","owner":"ImperialCollegeLondon","isFork":false,"description":"Lean 3 material for Kevin Buzzard's 2021 TCC courrse on formalising mathematics. Lean 4 version available here: <a href=\"https://github.com/ImperialCollegeLondon/formalising-mathematics-2024\">https://github.com/ImperialCollegeLondon/formalising-mathematics-2024</a>","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":0,"starsCount":294,"forksCount":22,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-09T11:16:32.044Z"}},{"type":"Public","name":"M40001_lean","owner":"ImperialCollegeLondon","isFork":false,"description":"Lean 3 material related to Imperial College's \"Introduction to University Mathematics\" course","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":0,"starsCount":155,"forksCount":14,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-03-09T10:15:47.400Z"}},{"type":"Public","name":"formalising-mathematics-2023","owner":"ImperialCollegeLondon","isFork":false,"description":"repository for material for Jan-Mar 2023 course on formalising mathematics","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":48,"forksCount":16,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2024-02-12T17:39:26.465Z"}},{"type":"Public","name":"M1F-explained","owner":"ImperialCollegeLondon","isFork":false,"description":"A computer formalisation of parts of Martin Liebeck's book \"a concise introduction to pure mathematics\"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":1,"starsCount":10,"forksCount":5,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-08-24T12:43:51.987Z"}},{"type":"Public","name":"m1fexplained_lean3","owner":"ImperialCollegeLondon","isFork":false,"description":"A Lean formalisation of parts of Martin Liebeck's \"A concise introduction to pure mathematics\"","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":13,"forksCount":6,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-07-07T18:07:09.592Z"}},{"type":"Public","name":"group-theory-experiments","owner":"ImperialCollegeLondon","isFork":false,"description":"Lean 4 experiments in undergraduate group theory","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":5,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-07-07T15:14:50.489Z"}},{"type":"Public","name":"real-number-game","owner":"ImperialCollegeLondon","isFork":false,"description":"A gamification of the theorems in MATH40002 Analysis 1","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":2,"issueCount":2,"starsCount":75,"forksCount":7,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2023-02-05T01:10:45.585Z"}},{"type":"Public","name":"tcc-lean-alg-geom-2022","owner":"ImperialCollegeLondon","isFork":false,"description":"Experiments in algebraic geometry as part of the EPSRC Taught Course Centre course on formalising number theory and geometry","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":7,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-12-05T15:42:36.510Z"}},{"type":"Public","name":"diophantine","owner":"ImperialCollegeLondon","isFork":false,"description":"Solving Diophantine equations in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":8,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-11-24T20:15:23.783Z"}},{"type":"Public","name":"complex-number-game","owner":"ImperialCollegeLondon","isFork":false,"description":"The Complex Number Game. Make the complex numbers in Lean.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":2,"starsCount":32,"forksCount":4,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-11-12T00:24:39.049Z"}},{"type":"Public","name":"lean-maths-examples","owner":"ImperialCollegeLondon","isFork":false,"description":"Some theorems presented to first and second year mathematics undergraduates, First and second year undergraduate level mathematics ","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":12,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2022-01-16T18:05:48.588Z"}},{"type":"Public","name":"group-action-exercises","owner":"ImperialCollegeLondon","isFork":false,"description":"Exercises for the basic theory of group actions in Lean 3","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":1,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-07-03T23:17:28.556Z"}},{"type":"Public","name":"Example-Lean-Projects","owner":"ImperialCollegeLondon","isFork":false,"description":"Some examples of Lean projects, for undergraduate mathematicians.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":1,"issueCount":0,"starsCount":22,"forksCount":2,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-06-07T19:05:39.268Z"}},{"type":"Public","name":"group-theory-game","owner":"ImperialCollegeLondon","isFork":false,"description":"Building group theory from scratch in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":57,"forksCount":3,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2021-01-24T20:59:18.092Z"}},{"type":"Public","name":"M40002","owner":"ImperialCollegeLondon","isFork":false,"description":"Completely unofficial Lean repository for the undergraduate analysis M40002/M40010 course","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-12-10T18:27:09.012Z"}},{"type":"Public","name":"condensed-sets","owner":"ImperialCollegeLondon","isFork":false,"description":"Condensed mathematics in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":1,"starsCount":5,"forksCount":2,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-10-01T10:52:58.421Z"}},{"type":"Public","name":"P11-Galois-Theory","owner":"ImperialCollegeLondon","isFork":false,"description":"Lean notes for Imperial course P11 : Galois Theory","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":2,"starsCount":4,"forksCount":0,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-09-14T10:51:46.403Z"}},{"type":"Public","name":"british-natural-number-game","owner":"ImperialCollegeLondon","isFork":false,"description":"The British Natural Number Game. We develop the theory of `num`","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-08-08T11:39:03.152Z"}},{"type":"Public","name":"uniform-structures","owner":"ImperialCollegeLondon","isFork":false,"description":"Various definitions of a uniform space in Lean","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":"2020-06-18T15:50:22.269Z"}},{"type":"Public","name":"dots_and_boxes","owner":"ImperialCollegeLondon","isFork":false,"description":"Ellen's dots and boxes project","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":5,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-06-06T10:17:58.890Z"}},{"type":"Public","name":"xena-UROP-2018","owner":"ImperialCollegeLondon","isFork":false,"description":"A place to put our 2018 Xena project UROP thoughts and programs.","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":10,"starsCount":23,"forksCount":5,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-05-27T11:03:01.988Z"}},{"type":"Public","name":"M4P33","owner":"ImperialCollegeLondon","isFork":false,"description":"M4 algebraic geometry course in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":2,"starsCount":57,"forksCount":5,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-03-04T17:51:46.443Z"}},{"type":"Public","name":"local-fields","owner":"ImperialCollegeLondon","isFork":false,"description":"Formalisation of parts of the theory of local fields in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":3,"forksCount":1,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2020-02-13T21:34:49.002Z"}},{"type":"Public","name":"M1F_example_sheets","owner":"ImperialCollegeLondon","isFork":false,"description":"M1F 2018-19 example sheets in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":5,"forksCount":2,"license":"GNU General Public License v3.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2019-11-20T13:10:22.280Z"}},{"type":"Public","name":"M1P1-lean","owner":"ImperialCollegeLondon","isFork":false,"description":"Material from M1P1, formalised in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":14,"forksCount":2,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2019-11-02T20:39:27.576Z"}},{"type":"Public","name":"lean-groups","owner":"ImperialCollegeLondon","isFork":false,"description":"Some advanced undergrad group theory in Lean","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":4,"forksCount":0,"license":null,"participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2019-08-30T20:34:51.441Z"}},{"type":"Public","name":"M1F-exam-may-2018","owner":"ImperialCollegeLondon","isFork":false,"description":"Questions and solutions to may 2018 M1F exam","topicNames":[],"topicsNotShown":0,"allTopics":[],"primaryLanguage":{"name":"Lean","color":"#ccc"},"pullRequestCount":0,"issueCount":0,"starsCount":2,"forksCount":0,"license":"Apache License 2.0","participation":null,"lastUpdated":{"hasBeenPushedTo":true,"timestamp":"2019-05-06T20:49:55.493Z"}}],"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":"Repositories"}