{"id":1777030,"full_name":"leanprover/lean4","default_branch":"master","total_commits":40851,"total_committers":290,"total_bot_commits":55,"total_bot_committers":2,"mean_commits":140.8655172413793,"dds":0.4188147168979951,"past_year_total_commits":3695,"past_year_total_committers":101,"past_year_total_bot_commits":21,"past_year_total_bot_committers":1,"past_year_mean_commits":36.584158415841586,"past_year_dds":0.8435723951285521,"last_synced_at":"2026-10-17T07:31:17.294Z","last_synced_commit":"25ba8c3d3bcb1dded7ff5a6f3b6044b0a7970198","created_at":"2024-09-20T16:59:36.474Z","updated_at":"2026-10-18T10:32:19.924Z","committers":[{"name":"Leonardo de Moura","email":"leonardo@microsoft.com","login":"leodemoura","count":23742},{"name":"Sebastian Ullrich","email":"sebasti@nullri.ch","login":"Kha","count":5006},{"name":"Kim Morrison","email":"scott.morrison@gmail.com","login":"kim-em","count":1533},{"name":"tydeu","email":"tydeu@hatpress.net","login":"tydeu","count":1128},{"name":"Gabriel Ebner","email":"gebner@gebner.org","login":"gebner","count":1013},{"name":"Soonho Kong","email":"soonhok@cs.cmu.edu","login":"soonhokong","count":826},{"name":"Joachim Breitner","email":"mail@joachim-breitner.de","login":"nomeata","count":638},{"name":"Henrik Böving","email":"hargonix@gmail.com","login":"hargoniX","count":512},{"name":"Lean stage0 autoupdater","email":"","login":null,"count":484},{"name":"Mario Carneiro","email":"di.gama@gmail.com","login":"digama0","count":439},{"name":"Jeremy Avigad","email":"avigad@cmu.edu","login":"avigad","count":419},{"name":"Kyle Miller","email":"kmill31415@gmail.com","login":"kmill","count":381},{"name":"Markus Himmel","email":"markus@lean-fro.org","login":"TwoFX","count":336},{"name":"Cameron Zwarich","email":"cameron@lean-fro.org","login":"zwarich","count":335},{"name":"Wojciech Nawrocki","email":"wjnawrocki@protonmail.com","login":"Vtec234","count":331},{"name":"Sebastian Graf","email":"sgraf1337@gmail.com","login":"sgraf812","count":285},{"name":"Floris van Doorn","email":"fpv@andrew.cmu.edu","login":null,"count":266},{"name":"Daniel Selsam","email":"daniel.selsam@gmail.com","login":null,"count":225},{"name":"Marc Huisinga","email":"mhuisi@protonmail.com","login":"mhuisi","count":199},{"name":"Paul Reichert","email":"6992158+datokrat","login":"datokrat","count":184},{"name":"Wojciech Różowski","email":"wojciech@lean-fro.org","login":"wkrozowski","count":153},{"name":"David Thrane Christiansen","email":"david@davidchristiansen.dk","login":"david-christiansen","count":151},{"name":"Jakob von Raumer","email":"javra@web.de","login":null,"count":145},{"name":"Daniel Selsam","email":"daniel.selsam@protonmail.com","login":"dselsam","count":142},{"name":"E.W.Ayers","email":"edward.ayers@outlook.com","login":"EdAyers","count":118},{"name":"Garmelon","email":"joscha@plugh.de","login":"Garmelon","count":104},{"name":"Siddharth","email":"siddu.druid@gmail.com","login":"bollu","count":100},{"name":"Eric Wieser","email":"efw@google.com","login":"eric-wieser","count":94},{"name":"Rob Lewis","email":"rob.y.lewis@gmail.com","login":"robertylewis","count":71},{"name":"Rob23oba","email":"152706811+Rob23oba","login":"Rob23oba","count":65},{"name":"Sofia Rodrigues","email":"sofia@algebraic.dev","login":"algebraic-dev","count":60},{"name":"jrr6","email":"7482866+jrr6","login":"jrr6","count":53},{"name":"Tobias Grosser","email":"tobias@grosser.es","login":"tobiasgrosser","count":50},{"name":"Rob Lewis","email":"rlewis1@andrew.cmu.edu","login":null,"count":48},{"name":"Luisa Cicolini","email":"48860705+luisacicolini","login":"luisacicolini","count":47},{"name":"larsk21","email":"57503246+larsk21","login":"larsk21","count":47},{"name":"Daniel Fabian","email":"daniel.fabian@integral-it.ch","login":"DanielFabian","count":46},{"name":"Johannes Hölzl","email":"johannes.hoelzl@gmx.de","login":"johoelzl","count":45},{"name":"Joe Hendrix","email":"joe@lean-fro.org","login":"joehendrix","count":45},{"name":"dependabot[bot]","email":"49699333+dependabot[bot]","login":"dependabot[bot]","count":39},{"name":"Nuno Lopes","email":"nlopes@microsoft.com","login":"nunoplopes","count":38},{"name":"Joe Hendrix","email":"jhendrix@galois.com","login":null,"count":32},{"name":"François G. Dorais","email":"fgdorais@gmail.com","login":"fgdorais","count":29},{"name":"Robert J. Simmons","email":"442315+robsimmons","login":"robsimmons","count":28},{"name":"JovanGerb","email":"56355248+JovanGerb","login":"JovanGerb","count":26},{"name":"Chris Lovett","email":"clovett@microsoft.com","login":"lovettchris","count":23},{"name":"Alex Keizer","email":"alex@keizer.dev","login":"alexkeizer","count":23},{"name":"Jannis Limperg","email":"jannis@limperg.de","login":"JLimperg","count":21},{"name":"Arthur Adjedj","email":"arthur.adjedj@gmail.com","login":"arthur-adjedj","count":21},{"name":"Lev Nachmanson","email":"levnach@microsoft.com","login":"levnach","count":20},{"name":"thorimur","email":"68410468+thorimur","login":"thorimur","count":20},{"name":"Haitao Zhang","email":"zhtprog@gmail.com","login":"htzh","count":20},{"name":"Marcus Rossel","email":"marcusrossel@icloud.com","login":"marcusrossel","count":18},{"name":"euprunin","email":"djupinlarning@gmail.com","login":"euprunin","count":18},{"name":"Jared Roesch","email":"roeschinc@gmail.com","login":"jroesch","count":16},{"name":"github-actions[bot]","email":"41898282+github-actions[bot]","login":"github-actions[bot]","count":16},{"name":"Parth Shastri","email":"31370288+cppio","login":"cppio","count":14},{"name":"Simon Hudon","email":"simon.hudon@gmail.com","login":"cipher1024","count":12},{"name":"Vlad Tsyrklevich","email":"vlad@tsyrklevich.net","login":"vlad902","count":12},{"name":"Jason Yuen","email":"jason_yuen2007@hotmail.com","login":"int-y1","count":11},{"name":"Ulrik Buchholtz","email":"ulrikbuchholtz@gmail.com","login":"UlrikBuchholtz","count":11},{"name":"Bulhwi Cha","email":"chabulhwi@semmalgil.com","login":"chabulhwi","count":11},{"name":"Adrien Champion","email":"AdrienChampion","login":"AdrienChampion","count":11},{"name":"Johan Commelin","email":"johan@commelin.net","login":"jcommelin","count":10},{"name":"Alok Singh","email":"alokbeniwal@gmail.com","login":"alok","count":9},{"name":"Favonia","email":"favonia@gmail.com","login":"favonia","count":9},{"name":"Bhavik Mehta","email":"bhavikmehta8@gmail.com","login":"b-mehta","count":8},{"name":"Jakob von Raumer","email":"jakob@von-raumer.de","login":"javra","count":8},{"name":"Michael Rothgang","email":"rothgang@math.uni-bonn.de","login":"grunweg","count":7},{"name":"ammkrn","email":"ammkrn@tuta.io","login":"ammkrn","count":7},{"name":"Julien Cretin","email":"git@ia0.eu","login":"ia0","count":7},{"name":"Violeta Hernández","email":"vi.hdz.p@gmail.com","login":"vihdzp","count":7},{"name":"Aaron Liu","email":"aaronliu2008@outlook.com","login":"plp127","count":7},{"name":"Alex J Best","email":"alex.j.best@gmail.com","login":"alexjbest","count":7},{"name":"Théo Zimmermann","email":"theo.zimmi@gmail.com","login":"Zimmi48","count":7},{"name":"Patrick Massot","email":"patrickmassot@free.fr","login":"PatrickMassot","count":7},{"name":"Jon Eugster","email":"eugster.jon@gmail.com","login":"joneugster","count":7},{"name":"Anne Baanen","email":"Vierkantor","login":"Vierkantor","count":7},{"name":"Austin Letson","email":"waustinletson@gmail.com","login":"austinletson","count":6},{"name":"David Renshaw","email":"dwrenshaw@gmail.com","login":"dwrensha","count":6},{"name":"Kitamado","email":"47292598+Seasawher","login":"Seasawher","count":6},{"name":"Mariana Alanis","email":"malanistamez@microsoft.com","login":"marianaalanis93","count":6},{"name":"Yuri de Wit","email":"ydewit@gmail.com","login":"ydewit","count":6},{"name":"Scott Morrison","email":"scott.morrison@anu.edu.au","login":null,"count":5},{"name":"Denis Gorbachev","email":"829578+DenisGorbachev","login":"DenisGorbachev","count":5},{"name":"FR","email":"zhao.yu-yang@foxmail.com","login":"FR-vdash-bot","count":5},{"name":"Tom Levy","email":"tomlevy93@gmail.com","login":"tom93","count":5},{"name":"Vladimir Gladshtein","email":"55004725+volodeyka","login":"volodeyka","count":5},{"name":"Corey Richardson","email":"corey@octayn.net","login":"emberian","count":5},{"name":"diakopter","email":"diakopter@gmail.com","login":"diakopter","count":5},{"name":"pcpthm","email":"pcpthm@gmail.com","login":"pcpthm","count":5},{"name":"Rishikesh Vaishnav","email":"rishhvaishnav@gmail.com","login":"rish987","count":4},{"name":"Matthew Robert Ballard","email":"100034030+mattrobball","login":"mattrobball","count":4},{"name":"Martin Dvořák","email":"martin.dvorak@matfyz.cz","login":"madvorak","count":4},{"name":"Leni Aniva","email":"107011294+lenianiva","login":"lenianiva","count":4},{"name":"Simon Cruanes","email":"simon.cruanes.2007@m4x.org","login":"c-cube","count":4},{"name":"Syohei YOSHIDA","email":"syohex@gmail.com","login":"syohex","count":4},{"name":"TomasPuverle","email":"TomasPuverle","login":"TomasPuverle","count":4},{"name":"seulbaek","email":"seulkeebaek@gmail.com","login":"skbaek","count":4},{"name":"L","email":"git@llllvvuu.dev","login":"llllvvuu","count":4},{"name":"Johannes Tantow","email":"44068763+jt0202","login":"jt0202","count":4},{"name":"Jeremy Tan Jie Rui","email":"reddeloostw@gmail.com","login":"Parcly-Taxel","count":4},{"name":"George Rennie","email":"georgerennie@gmail.com","login":"georgerennie","count":4},{"name":"Floris van Doorn","email":"fpvdoorn@gmail.com","login":"fpvandoorn","count":4},{"name":"zygi","email":"nonagon@fastmail.com","login":"zygi","count":4},{"name":"Wrenna Robson","email":"wrenna.robson@bristol.ac.uk","login":"linesthatinterlace","count":4},{"name":"Sean Leather","email":"sean.leather@gmail.com","login":"spl","count":3},{"name":"Markus Schmaus","email":"markus.schmaus.math@gmail.com","login":"markusschmaus","count":3},{"name":"damiano","email":"adomani@gmail.com","login":"adomani","count":3},{"name":"Hongyu Ouyang","email":"96765450+casavaca","login":"casavaca","count":3},{"name":"Marcelo Lynch","email":"marcelomlynch@gmail.com","login":"marcelolynch","count":3},{"name":"Alexander Bentkamp","email":"bentkamp@gmail.com","login":"abentkamp","count":3},{"name":"Christian Pehle","email":"christian.pehle@gmail.com","login":"cpehle","count":3},{"name":"Andrés Goens","email":"andres@goens.org","login":"goens","count":3},{"name":"Anders Christiansen Sørby","email":"anders@sorby.xyz","login":"Anderssorby","count":3},{"name":"Arthur Paulino","email":"arthurleonardo.ap@gmail.com","login":"arthurpaulino","count":3},{"name":"Copilot","email":"198982749+Copilot","login":"Copilot","count":3},{"name":"Elias Aebi","email":"eyelash","login":"eyelash","count":3},{"name":"Harun Khan","email":"58151072+mhk119","login":"mhk119","count":3},{"name":"Jacob Gross","email":"jag218@pitt.edu","login":"JacobGross","count":3},{"name":"James Sully","email":"sullyj3@gmail.com","login":"sullyj3","count":3},{"name":"Leonardo de Moura","email":"leonardodemoura@Leonardos-MacBook-Pro.local","login":null,"count":3},{"name":"Simon Hudon","email":"shudon@galois.com","login":null,"count":3},{"name":"Leni Aniva","email":"107011294+vleni","login":"vleni","count":2},{"name":"Andrii Kurdiumov","email":"kant2002@gmail.com","login":"kant2002","count":2},{"name":"Alissa Tung","email":"alissa-tung@outlook.com","login":"alissa-tung","count":2},{"name":"Alex Meiburg","email":"timeroot.alex@gmail.com","login":"Timeroot","count":2},{"name":"Pietro Monticone","email":"38562595+pitmonticone","login":"pitmonticone","count":2},{"name":"Nicolas Rouquette","email":"nicolas.f.rouquette@jpl.nasa.gov","login":"NicolasRouquette","count":2},{"name":"Max Wagner","email":"max@trollbu.de","login":"TehMillhouse","count":2},{"name":"Mauricio Collares","email":"mauricio@collares.org","login":"collares","count":2},{"name":"Lukas Gerlach","email":"12497479+monsterkrampe","login":"monsterkrampe","count":2},{"name":"Bolton Bailey","email":"bolton.bailey@gmail.com","login":"BoltonBailey","count":2},{"name":"Chris Henson","email":"46805207+chenson2018","login":"chenson2018","count":2},{"name":"Clement Courbet","email":"clement.courbet@gmail.com","login":"legrosbuffle","count":2},{"name":"Eric Paul","email":"eric.1334@icloud.com","login":"ericluap","count":2},{"name":"Francisco Giordano","email":"fg@frang.io","login":"frangio","count":2},{"name":"Geoffrey Irving","email":"irving@naml.us","login":"girving","count":2},{"name":"Hunter Monroe","email":"github.com@huntermonroe.com","login":"hmonroe","count":2},{"name":"Potato Hatsue","email":"berberman@yandex.com","login":"berberman","count":2},{"name":"Jens Petersen","email":"juhpetersen@gmail.com","login":"juhp","count":2},{"name":"Chris Hughes","email":"33847686+ChrisHughes24","login":"ChrisHughes24","count":2},{"name":"Buster Copley","email":"rcopley@gmail.com","login":"bustercopley","count":2},{"name":"Théophile Wallez","email":"theophile@wallez.net","login":"TWal","count":2},{"name":"bc²","email":"odanoburu","login":"odanoburu","count":2},{"name":"leiko","email":"wewamemokoto@gmail.com","login":"leiko1337","count":2},{"name":"pandaman","email":"kointosudesuyo@infoseek.jp","login":"pandaman64","count":2},{"name":"Shuhao Song","email":"znssong_meow@sina.com","login":"znssong","count":2},{"name":"Timo","email":"timorcb@gmail.com","login":"timotree3","count":2},{"name":"James Gallicchio","email":"JamesGallicchio","login":"JamesGallicchio","count":2},{"name":"John Tristan","email":"jean.baptiste.tristan@gmail.com","login":"jtristan","count":2},{"name":"Jonathan Coates","email":"git@squiddev.cc","login":"SquidDev","count":2},{"name":"Josh Levine","email":"github@junk.josh.com","login":"bigjosh","count":2},{"name":"Connor Baker","email":"connor.baker@tweag.io","login":null,"count":2},{"name":"Junyan Xu","email":"junyanxu.math@gmail.com","login":"alreadydone","count":2},{"name":"Keith Seim","email":"keith@firestitch.com","login":"kjsdesigns","count":2},{"name":"Xavier Noria","email":"fxn@hashref.com","login":"fxn","count":1},{"name":"WojciechKarpiel","email":"w.karpiel@o2.pl","login":"WojciechKarpiel","count":1},{"name":"Mohamed Al-Fahim","email":"31521089+MohamedAlFahim","login":"MohamedAlFahim","count":1},{"name":"Miyahara Kō","email":"52843868+Komyyy","login":"Komyyy","count":1},{"name":"Violetta Sim","email":"38787503+eyihluyc","login":"eyihluyc","count":1},{"name":"Vincent de Haan","email":"vincentdehaan@gmail.com","login":"vincentdehaan","count":1},{"name":"Varun Gandhi","email":"git@cutcul.us","login":"typesanitizer","count":1},{"name":"Tony Beta Lambda","email":"tonybetalambda@gmail.com","login":"tonyxty","count":1},{"name":"Tom Ball","email":"tballmsft","login":"tballmsft","count":1},{"name":"Xin Hao","email":"haoxinst@gmail.com","login":"haoxins","count":1},{"name":"Xubai Wang","email":"self@xubai.wang","login":"xubaiw","count":1},{"name":"Yang Song","email":"yangsong@alumni.princeton.edu","login":"yangsong97","count":1},{"name":"Yann Herklotz","email":"git@yannherklotz.com","login":"ymherklotz","count":1},{"name":"Yaël Dillies","email":"yael.dillies@gmail.com","login":"YaelDillies","count":1},{"name":"asdasd1dsadsa","email":"835263969@qq.com","login":"asdasd1dsadsa","count":1},{"name":"awson","email":"kyrab@mail.ru","login":"awson","count":1},{"name":"Reid Barton","email":"rwbarton@gmail.com","login":"rwbarton","count":1},{"name":"Reijo Jaakkola","email":"53764345+ReijoJaakkola","login":"ReijoJaakkola","count":1},{"name":"Richard Musiol","email":"mail@richard-musiol.de","login":"neelance","count":1},{"name":"Rob Dockins","email":"rdockins@galois.com","login":"robdockins","count":1},{"name":"gabriel-doriath-dohler","email":"gabriel.doriath.dohler@ens.fr","login":"gabriel-doriath-dohler","count":1},{"name":"hwatheod","email":"hwatheod@cs.stanford.edu","login":"hwatheod","count":1},{"name":"Sébastien Boisgérault","email":"Sebastien.Boisgerault@gmail.com","login":"boisgera","count":1},{"name":"Severen Redwood","email":"severen@shrike.me","login":"severen","count":1},{"name":"Sebastien Gouezel","email":"sebastien.gouezel@univ-rennes1.fr","login":"sgouezel","count":1},{"name":"Sebastian Reuße","email":"seb@wirrsal.net","login":"eigengrau","count":1},{"name":"Sebastian Miele","email":"iota@whxvd.name","login":"whxvd","count":1},{"name":"Sean McLaughlin","email":"seanmcl@gmail.com","login":"seanmcl","count":1},{"name":"SADIK KUZU","email":"sadikkuzu@hotmail.com","login":"sadikkuzu","count":1},{"name":"Robert Maxton","email":"robert.maxton42@gmail.com","login":"robertmaxton42","count":1},{"name":"TAKANO Mitsuhiro","email":"takano32@gmail.com","login":"takano32","count":1},{"name":"Tasiro","email":"tasiro-git@gmx.de","login":"Tasiro","count":1},{"name":"Thomas Köppe","email":"tkoeppe@google.com","login":"tkoeppe","count":1},{"name":"Kai Ruemmler","email":"kai.ruemmler@gmx.net","login":null,"count":1},{"name":"Joe Hendrix","email":"joe.hendrix@sri.com","login":null,"count":1},{"name":"Kaiyu Yang","email":"kaiyuy@caltech.edu","login":null,"count":1},{"name":"Bulhwi Cha","email":"chabulhwi@protonmail.ch","login":null,"count":1},{"name":"Armaël Guéneau","email":"armael.gueneau@ens-lyon.fr","login":null,"count":1},{"name":"Andrew Kent","email":"andrew@galois.com","login":null,"count":1},{"name":"Andrew Ashworth","email":"alashworth@gmail.com","login":null,"count":1},{"name":"matt rice","email":"ratmice@gmail.com","login":"ratmice","count":1},{"name":"maxwell3025","email":"44588341+maxwell3025","login":"maxwell3025","count":1},{"name":"mcdoll","email":"moritz.doll@googlemail.com","login":"mcdoll","count":1},{"name":"nnarek","email":"49597137+nnarek","login":"nnarek","count":1},{"name":"simon-dima","email":"126682907+simon-dima","login":"simon-dima","count":1},{"name":"tonneaus","email":"88409353+tonneaus","login":"tonneaus","count":1},{"name":"user202729","email":"25191436+user202729","login":"user202729","count":1},{"name":"vvs-","email":"vvs-","login":"vvs-","count":1},{"name":"zjhmale","email":"zjhmale@gmail.com","login":"swr1bm86","count":1},{"name":"William Blake","email":"35980963+langfield","login":"langfield","count":1},{"name":"ayhon","email":"43295942+ayhon","login":"ayhon","count":1},{"name":"brett koonce","email":"koonce@gmail.com","login":"brettkoonce","count":1},{"name":"crStiv","email":"cryptostiv7@gmail.com","login":"crStiv","count":1},{"name":"ecyrbe","email":"ecyrbe@gmail.com","login":"ecyrbe","count":1},{"name":"fiforeach","email":"249703130+fiforeach","login":"fiforeach","count":1},{"name":"えび (ebi_chan)","email":"spinylobster@outlook.com","login":"spinylobster","count":1},{"name":"Daniel Weber","email":"55664973+Command-Master","login":"Command-Master","count":1},{"name":"jcreedcmu","email":"jcreed@gmail.com","login":"jcreedcmu","count":1},{"name":"joao guilherme","email":"joaoguilhermearujo@gmail.com","login":"joaogui1","count":1},{"name":"jsr-p","email":"jsr-p@sodas.ku.dk","login":"jsr-p","count":1},{"name":"kuruczgy","email":"57020850+kuruczgy","login":"kuruczgy","count":1},{"name":"kzvi","email":"38590027+kzvi","login":"kzvi","count":1},{"name":"locriacyber","email":"74560659+locriacyber","login":"locriacyber","count":1},{"name":"lu-bulhoes","email":"153877324+lu-bulhoes","login":"lu-bulhoes","count":1},{"name":"Бакиновский Максим","email":"m.bakinovsky@cognitivepilot.com","login":null,"count":1},{"name":"Yuri de Wit","email":"yuri.dewit@frevvo.com","login":null,"count":1},{"name":"Olivier Taïbi","email":"github@olitb.net","login":null,"count":1},{"name":"Fynn Schmitt-Ulms","email":"fynnsu@outlook.com","login":"fynnsu","count":1},{"name":"Gabe","email":"66077254+MrBrain295","login":"MrBrain295","count":1},{"name":"Gabriel Dahia","email":"gdahia","login":"gdahia","count":1},{"name":"Giles Shaw","email":"62542365+gilesgshaw","login":"gilesgshaw","count":1},{"name":"Hagb (Junyu Guo 郭俊余)","email":"hagbgreen@yahoo.com","login":"Hagb","count":1},{"name":"Hikaru Hasegawa","email":"drumscohika@gmail.com","login":"telumo","count":1},{"name":"Ikko Eltociear Ashimine","email":"eltociear@gmail.com","login":"eltociear","count":1},{"name":"Aaron Tomb","email":"aarontomb@gmail.com","login":"atomb","count":1},{"name":"JadAbouHawili","email":"jad-abou-hawili@hotmail.com","login":"JadAbouHawili","count":1},{"name":"James Oswald","email":"jamesoswald111@gmail.com","login":"James-Oswald","count":1},{"name":"Jan Hrcek","email":"2716069+jhrcek","login":"jhrcek","count":1},{"name":"Jeremy Salwen","email":"jeremysalwen@gmail.com","login":"jeremysalwen","count":1},{"name":"Jerry Wu","email":"netfirewall@gmail.com","login":"pzread","count":1},{"name":"Jesse Alama","email":"jessealama","login":"jessealama","count":1},{"name":"Jesse Wright","email":"63333554+jeswr","login":"jeswr","count":1},{"name":"Josh Pollock","email":"joshpollock1997@gmail.com","login":"joshpoll","count":1},{"name":"Joshua Seaton","email":"josh.a.seaton@gmail.com","login":"joshuaseaton","count":1},{"name":"Alex","email":"josojo@hotmail.de","login":"josojo","count":1},{"name":"Andrei Cheremskoy","email":"acheremskoy@gmail.com","login":"AndrewCh","count":1},{"name":"AxelBoldt","email":"axelboldt@yahoo.com","login":"AxelBoldt","count":1},{"name":"Benjamin Shi","email":"aiifabbf@outlook.com","login":"aiifabbf","count":1},{"name":"Chase Johnson","email":"cjohnson19@pm.me","login":"cjohnson19","count":1},{"name":"Christian Krause","email":"86738237+Bergschaf","login":"Bergschaf","count":1},{"name":"Connor Baker","email":"ConnorBaker01@Gmail.com","login":"ConnorBaker","count":1},{"name":"Dax Fohl","email":"dax.fohl@gmail.com","login":"daxfohl","count":1},{"name":"Derrik Petrin","email":"derrik@petrin.tech","login":"dfpetrin","count":1},{"name":"Elazar Gershuni","email":"elazarg@gmail.com","login":"elazarg","count":1},{"name":"Elias Theis","email":"eliastheis.sg@gmail.com","login":"eliastheis","count":1},{"name":"Enrico Borba","email":"enricozb","login":"enricozb","count":1},{"name":"Eric Rodriguez","email":"37984851+ericrbg","login":"ericrbg","count":1},{"name":"Evan Chen","email":"evan@evanchen.cc","login":"vEnhance","count":1},{"name":"Evgenia Karunus","email":"lakesare@gmail.com","login":"lakesare","count":1},{"name":"Filippo A. E. Nuccio","email":"filippo.nuccio@univ-st-etienne.fr","login":"faenuccio","count":1},{"name":"Matthew Toohey","email":"contact@mtoohey.com","login":"mtoohey31","count":1},{"name":"Matthias Hetzenberger","email":"mhetzenberger@gmail.com","login":"hetzenmat","count":1},{"name":"Max Carr","email":"m@mcarr.one","login":"suaviloquence","count":1},{"name":"Michael Burge","email":"michaelburge@pobox.com","login":"MichaelBurge","count":1},{"name":"Michael Sammler","email":"MackieLoeffel","login":"MackieLoeffel","count":1},{"name":"Michał Dobranowski","email":"michal.dobranowski@gmail.com","login":"mdbrnowski","count":1},{"name":"JOSHCLUNE","email":"josh.seth.clune@gmail.com","login":"JOSHCLUNE","count":1},{"name":"MoritzBeroRoos","email":"56820109+MoritzBeroRoos","login":"MoritzBeroRoos","count":1},{"name":"Nadja Yang","email":"nadja@njy.dev","login":"nadja-y","count":1},{"name":"Osman Yasar","email":"osmanyas05@gmail.com","login":"osmanyasar05","count":1},{"name":"Parker Bjur","email":"38863599+parkerbjur","login":"parkerbjur","count":1},{"name":"Patrick Stevens","email":"patrick+github@patrickstevens.co.uk","login":"Smaug123","count":1},{"name":"Paul Brinkmeier","email":"paul.brinkmeier@gmail.com","login":"pbrinkmeier","count":1},{"name":"Peiran Wu","email":"15968905+wupr","login":"wupr","count":1},{"name":"Phil de Joux","email":"philderbeast@gmail.com","login":"philderbeast","count":1},{"name":"Pim Otte","email":"otte.pim@gmail.com","login":"pimotte","count":1},{"name":"Plamen Dimitrov","email":"plamen.dimitrov@intra2net.com","login":"pevogam","count":1},{"name":"Formally Verified Waffle Maker","email":"76637701+FormallyVerifiedWaffleMaker","login":"FormallyVerifiedWaffleMaker","count":1},{"name":"Juan Pablo Romero","email":"jpablo.romero@gmail.com","login":"jpablo","count":1},{"name":"Julien Michel","email":"120744578+michelsol","login":"michelsol","count":1},{"name":"Justin King","email":"jcking@wulver.com","login":"jcking","count":1},{"name":"Mitchell Lee","email":"130885647+trivial1711","login":"trivial1711","count":1},{"name":"Kartik Singhal","email":"kartiksinghal@gmail.com","login":"k4rtik","count":1},{"name":"KaseQuark","email":"79633239+KaseQuark","login":"KaseQuark","count":1},{"name":"Kenny Lau","email":"kc_kennylau@yahoo.com.hk","login":"kckennylau","count":1},{"name":"Kevin Buzzard","email":"k.buzzard@imperial.ac.uk","login":"kbuzzard","count":1},{"name":"Lars - he/him","email":"l.b.vandenhaak@gmail.com","login":"sakehl","count":1},{"name":"Li Xuanji","email":"xuanji@gmail.com","login":"ldct","count":1},{"name":"Liu Yuxi","email":"ubikium@gmail.com","login":"crvdgc","count":1},{"name":"Lorenz Leutgeb","email":"lorenz@mpi-inf.mpg.de","login":"lorenzleutgeb","count":1},{"name":"MJ141592","email":"95647331+MJ141592","login":"MJ141592","count":1},{"name":"Malhar A. Patel","email":"142735852+Mal-Pat","login":"Mal-Pat","count":1},{"name":"Malvin Gattinger","email":"malvin@w4eg.de","login":"m4lvin","count":1},{"name":"Mateja Petrovic","email":"mateja176@gmail.com","login":"mateja176","count":1}],"past_year_committers":[{"name":"Leonardo de Moura","email":"leomoura@amazon.com","login":"leodemoura","count":578},{"name":"Sebastian Ullrich","email":"sebasti@nullri.ch","login":"Kha","count":417},{"name":"Kim Morrison","email":"477956+kim-em","login":"kim-em","count":402},{"name":"Lean stage0 autoupdater","email":"","login":null,"count":285},{"name":"Sebastian Graf","email":"sgraf1337@gmail.com","login":"sgraf812","count":264},{"name":"Henrik Böving","email":"hargonix@gmail.com","login":"hargoniX","count":240},{"name":"Joachim Breitner","email":"mail@joachim-breitner.de","login":"nomeata","count":225},{"name":"Markus Himmel","email":"markus@lean-fro.org","login":"TwoFX","count":196},{"name":"Mac Malone","email":"tydeu@hatpress.net","login":"tydeu","count":164},{"name":"Wojciech Różowski","email":"wojciech@lean-fro.org","login":"wkrozowski","count":144},{"name":"Paul Reichert","email":"6992158+datokrat","login":"datokrat","count":103},{"name":"Cameron Zwarich","email":"cameron@lean-fro.org","login":"zwarich","count":94},{"name":"Kyle Miller","email":"kmill31415@gmail.com","login":"kmill","count":74},{"name":"David Thrane Christiansen","email":"david@davidchristiansen.dk","login":"david-christiansen","count":66},{"name":"Garmelon","email":"joscha@plugh.de","login":"Garmelon","count":65},{"name":"Marc Huisinga","email":"mhuisi@protonmail.com","login":"mhuisi","count":48},{"name":"Sofia Rodrigues","email":"sofia@algebraic.dev","login":"algebraic-dev","count":44},{"name":"Eric Wieser","email":"efw@google.com","login":"eric-wieser","count":40},{"name":"Rob23oba","email":"152706811+Rob23oba","login":"Rob23oba","count":32},{"name":"Robert J. Simmons","email":"442315+robsimmons","login":"robsimmons","count":28},{"name":"dependabot[bot]","email":"49699333+dependabot[bot]","login":"dependabot[bot]","count":21},{"name":"jrr6","email":"7482866+jrr6","login":"jrr6","count":12},{"name":"Wojciech Nawrocki","email":"13901751+Vtec234","login":"Vtec234","count":7},{"name":"Julien Cretin","email":"git@ia0.eu","login":"ia0","count":7},{"name":"Jason Yuen","email":"jason_yuen2007@hotmail.com","login":"int-y1","count":6},{"name":"Luisa Cicolini","email":"48860705+luisacicolini","login":"luisacicolini","count":6},{"name":"Thomas R. Murrills","email":"68410468+thorimur","login":"thorimur","count":6},{"name":"Vladimir Gladshtein","email":"55004725+volodeyka","login":"volodeyka","count":5},{"name":"Alok Singh","email":"alokbeniwal@gmail.com","login":"alok","count":5},{"name":"Aaron Liu","email":"aaronliu2008@outlook.com","login":"plp127","count":5},{"name":"Bhavik Mehta","email":"bhavikmehta8@gmail.com","login":"b-mehta","count":4},{"name":"François G. Dorais","email":"fgdorais@gmail.com","login":"fgdorais","count":4},{"name":"Tom Levy","email":"tomlevy93@gmail.com","login":"tom93","count":4},{"name":"Wrenna Robson","email":"wren.robson@gmail.com","login":"linesthatinterlace","count":4},{"name":"Michael Rothgang","email":"rothgang@math.uni-bonn.de","login":"grunweg","count":3},{"name":"Marcelo Lynch","email":"marcelomlynch@gmail.com","login":"marcelolynch","count":3},{"name":"Jovan Gerbscheid","email":"56355248+JovanGerb","login":"JovanGerb","count":3},{"name":"Copilot","email":"198982749+Copilot","login":"Copilot","count":3},{"name":"Anne Baanen","email":"Vierkantor","login":"Vierkantor","count":3},{"name":"leiko","email":"wewamemokoto@gmail.com","login":"leiko1337","count":2},{"name":"Théophile Wallez","email":"theophile@wallez.net","login":"TWal","count":2},{"name":"Potato Hatsue","email":"berberman@yandex.com","login":"berberman","count":2},{"name":"Nicolas Rouquette","email":"nicolas.f.rouquette@jpl.nasa.gov","login":"NicolasRouquette","count":2},{"name":"Mario Carneiro","email":"di.gama@gmail.com","login":"digama0","count":2},{"name":"Keith Seim","email":"keith@firestitch.com","login":"kjsdesigns","count":2},{"name":"Jon Eugster","email":"eugster.jon@gmail.com","login":"joneugster","count":2},{"name":"Johannes Tantow","email":"44068763+jt0202","login":"jt0202","count":2},{"name":"George Rennie","email":"georgerennie@gmail.com","login":"georgerennie","count":2},{"name":"Francisco Giordano","email":"fg@frang.io","login":"frangio","count":2},{"name":"Eric Paul","email":"eric.1334@icloud.com","login":"ericluap","count":2},{"name":"Chris Henson","email":"46805207+chenson2018","login":"chenson2018","count":2},{"name":"pandaman","email":"kointosudesuyo@infoseek.jp","login":"pandaman64","count":2},{"name":"Yaël Dillies","email":"yael.dillies@gmail.com","login":"YaelDillies","count":1},{"name":"Yang Song","email":"yangsong@alumni.princeton.edu","login":"yangsong97","count":1},{"name":"Violeta Hernández Palacios","email":"vi.hdz.p@gmail.com","login":"vihdzp","count":1},{"name":"Tobias Grosser","email":"tobias@grosser.es","login":"tobiasgrosser","count":1},{"name":"Sébastien Boisgérault","email":"Sebastien.Boisgerault@gmail.com","login":"boisgera","count":1},{"name":"Sebastian Miele","email":"iota@whxvd.name","login":"whxvd","count":1},{"name":"Robert Maxton","email":"robert.maxton42@gmail.com","login":"robertmaxton42","count":1},{"name":"Plamen Dimitrov","email":"plamen.dimitrov@intra2net.com","login":"pevogam","count":1},{"name":"Parth Shastri","email":"31370288+cppio","login":"cppio","count":1},{"name":"Osman Yasar","email":"osmanyas05@gmail.com","login":"osmanyasar05","count":1},{"name":"Nadja Yang","email":"nadja@njy.dev","login":"nadja-y","count":1},{"name":"MoritzBeroRoos","email":"56820109+MoritzBeroRoos","login":"MoritzBeroRoos","count":1},{"name":"Michał Dobranowski","email":"michal.dobranowski@gmail.com","login":"mdbrnowski","count":1},{"name":"Yuri de Wit","email":"ydewit@gmail.com","login":"ydewit","count":1},{"name":"Zhao Yuyang 赵雨扬","email":"zhao.yu-yang@foxmail.com","login":"FR-vdash-bot","count":1},{"name":"ayhon","email":"43295942+ayhon","login":"ayhon","count":1},{"name":"brett koonce","email":"koonce@gmail.com","login":"brettkoonce","count":1},{"name":"crStiv","email":"cryptostiv7@gmail.com","login":"crStiv","count":1},{"name":"damiano","email":"adomani@gmail.com","login":"adomani","count":1},{"name":"ecyrbe","email":"ecyrbe@gmail.com","login":"ecyrbe","count":1},{"name":"emberian","email":"ember@lunar.town","login":"emberian","count":1},{"name":"fiforeach","email":"249703130+fiforeach","login":"fiforeach","count":1},{"name":"jcreedcmu","email":"jcreed@gmail.com","login":"jcreedcmu","count":1},{"name":"maxwell3025","email":"44588341+maxwell3025","login":"maxwell3025","count":1},{"name":"Hikaru Hasegawa","email":"drumscohika@gmail.com","login":"telumo","count":1},{"name":"Giles Shaw","email":"62542365+gilesgshaw","login":"gilesgshaw","count":1},{"name":"Gabe","email":"66077254+MrBrain295","login":"MrBrain295","count":1},{"name":"Evan Chen","email":"evan@evanchen.cc","login":"vEnhance","count":1},{"name":"Elazar Gershuni","email":"elazarg@gmail.com","login":"elazarg","count":1},{"name":"Derrik Petrin","email":"derrik@petrin.tech","login":"dfpetrin","count":1},{"name":"Dax Fohl","email":"dax.fohl@gmail.com","login":"daxfohl","count":1},{"name":"Christian Krause","email":"86738237+Bergschaf","login":"Bergschaf","count":1},{"name":"Benjamin Shi","email":"aiifabbf@outlook.com","login":"aiifabbf","count":1},{"name":"AxelBoldt","email":"axelboldt@yahoo.com","login":"AxelBoldt","count":1},{"name":"Alexander Bentkamp","email":"bentkamp@gmail.com","login":"abentkamp","count":1},{"name":"Alex Meiburg","email":"timeroot.alex@gmail.com","login":"Timeroot","count":1},{"name":"Alex Keizer","email":"alex@keizer.dev","login":"alexkeizer","count":1},{"name":"JOSHCLUNE","email":"josh.seth.clune@gmail.com","login":"JOSHCLUNE","count":1},{"name":"JadAbouHawili","email":"jad-abou-hawili@hotmail.com","login":"JadAbouHawili","count":1},{"name":"Jesse Alama","email":"jessealama","login":"jessealama","count":1},{"name":"Joe Hendrix","email":"joehx@amazon.com","login":"joehendrix","count":1},{"name":"Junyan Xu","email":"junyanxu.math@gmail.com","login":"alreadydone","count":1},{"name":"Kenny Lau","email":"kc_kennylau@yahoo.com.hk","login":"kckennylau","count":1},{"name":"Kitamado","email":"47292598+Seasawher","login":"Seasawher","count":1},{"name":"Leni Aniva","email":"107011294+lenianiva","login":"lenianiva","count":1},{"name":"MJ141592","email":"95647331+MJ141592","login":"MJ141592","count":1},{"name":"Marcus Rossel","email":"marcusrossel@icloud.com","login":"marcusrossel","count":1},{"name":"Michael Sammler","email":"MackieLoeffel","login":"MackieLoeffel","count":1},{"name":"nnarek","email":"49597137+nnarek","login":"nnarek","count":1}],"commits_url":"https://commits.ecosyste.ms/api/v1/hosts/GitHub/repositories/leanprover%2Flean4/commits","host":{"name":"GitHub","url":"https://github.com","kind":"github","last_synced_at":"2026-10-18T00:00:09.420Z","repositories_count":8429420,"commits_count":1278030029,"contributors_count":58531929,"owners_count":1798071,"committers_count":3845436,"icon_url":"https://github.com/github.png","host_url":"https://commits.ecosyste.ms/api/v1/hosts/GitHub","repositories_url":"https://commits.ecosyste.ms/api/v1/hosts/GitHub/repositories"}}