{"692939":{"#nid":"692939","#data":{"type":"event","title":"Frontiers of Artificial Intelligence Seminar: CSLib: The Lean Computer Science Library ","body":[{"value":"\u003Cdiv\u003E\u003Cp\u003E\u003Cstrong\u003EAbstract:\u003C\/strong\u003E Following Mathlib\u0027s success in building a shared foundation for formalized mathematics, CSLib is a community-oriented effort to build a similar infrastructure for computer science and software in the Lean theorem prover.\u003C\/p\u003E\u003Cp\u003EIn this talk, I will present CSLib\u0027s current state, including its architecture, governance, organization, and how to contribute. Rather than giving only a high-level overview, I will use minimal working examples to illustrate the library\u0027s current API. I will showcase abstractions and definitions already available, ranging from computational paradigms to modeling and programming languages, logics, algorithms, and infrastructure to verify their properties.\u003C\/p\u003E\u003C\/div\u003E\u003Cp\u003EI will also introduce the CSLib Initiative, supported by Renaissance Philanthropy, which aims to coordinate and accelerate the development of the library and its surrounding ecosystem. I will discuss the CSLib Initiative roadmap\u003C\/p\u003E\u003Cp\u003EFinally, I will show how CSLib is already being used beyond the library itself, through community projects, textbooks, courses, and large-scale verification efforts. These include Software Foundations in Lean, the Functional Algorithms Design and Computational Semantics with Lean, and the port of Amazon\u0027s s2n-bignum formal proofs to Lean.\u003C\/p\u003E\u003Cp\u003E\u003Cstrong\u003EBio:\u003C\/strong\u003E Alexandre Rademaker is the Director of the CSLib Initiative at Renaissance Philanthropy. CSLib is a global open-source effort to build a library of formalized computer science in Lean. He also cooperates with NYU in DARPA\u0027s ExpMath program, which aims to accelerate mathematics research with AI.\u003C\/p\u003E\u003Cp\u003EAlexandre is also a professor at EMAp\/FGV (Applied Mathematics School, Getulio Vargas Foundation), where he has been teaching for about 20 years. He worked at IBM Research for 12 years until April 2025, when he left to lead the Specification IDE project at Atlas Computing, part of the Formal Verification of Software initiative funded by Schmidt Sciences under their Science of Trustworthy AI program.\u003C\/p\u003E\u003Cp\u003EDuring his PhD, he held research fellowships at Microsoft Research, working with the Z3 SMT solver team, and at SRI International. He has published more than 100 papers and spent much of his career leading open-source research collaborations with international communities, working with computational linguistics and building language resources. He was publication chair of the Language Resources and Evaluation Conference (LREC) and has served on the boards of research associations in Brazil and internationally.\u003C\/p\u003E\u003Cp\u003EAlexandre received a PhD in Computer Science from PUC-Rio, where his thesis on proof theory for description logics was published by Springer, and is based in Rio de Janeiro.\u003C\/p\u003E","summary":"","format":"limited_html"}],"field_subtitle":"","field_summary":[{"value":"\u003Cp\u003EIn this talk, I\u0026nbsp;will\u0026nbsp;present\u0026nbsp;CSLib\u0027s\u0026nbsp;current\u0026nbsp;state,\u0026nbsp;including\u0026nbsp;its\u0026nbsp;architecture,\u0026nbsp;governance,\u0026nbsp;organization,\u0026nbsp;and\u0026nbsp;how to contribute. Rather than giving only a high-level overview, I will use minimal working examples to illustrate the library\u0027s current API.\u0026nbsp;\u003C\/p\u003E","format":"limited_html"}],"field_summary_sentence":[{"value":"Featuring | Alexandre Rademaker - Professor, EMAp\/FGV (Applied Mathematics School, Getulio Vargas Foundation) "}],"uid":"27863","created_gmt":"2026-09-30 15:47:28","changed_gmt":"2026-09-30 16:08:59","author":"Christa Ernst","boilerplate_text":"","field_publication":"","field_article_url":"","field_event_time":{"event_time_start":"2026-10-05T15:00:00-04:00","event_time_end":"2026-10-05T16:00:00-04:00","event_time_end_last":"2026-10-05T16:00:00-04:00","gmt_time_start":"2026-10-05 19:00:00","gmt_time_end":"2026-10-05 20:00:00","gmt_time_end_last":"2026-10-05 20:00:00","rrule":null,"timezone":"America\/New_York"},"location":"Classroom 2456 @ Klaus Advanced Computing Building and Virtual","extras":[],"related_links":[{"url":"https:\/\/gatech.zoom.us\/j\/99195619305?pwd=5vH1cHNyTRPP3vE9Dtlf48qA04laHM.1","title":"Access Via Zoom"}],"groups":[{"id":"322011","name":"College of Computing Events"},{"id":"545781","name":"Institute for Data Engineering and Science"}],"categories":[],"keywords":[],"core_research_areas":[],"news_room_topics":[],"event_categories":[{"id":"1795","name":"Seminar\/Lecture\/Colloquium"}],"invited_audience":[{"id":"78761","name":"Faculty\/Staff"},{"id":"177814","name":"Postdoc"},{"id":"174045","name":"Graduate students"},{"id":"78751","name":"Undergraduate students"}],"affiliations":[],"classification":[],"areas_of_expertise":[],"news_and_recent_appearances":[],"phone":[],"contact":[],"email":[],"slides":[],"orientation":[],"userdata":""}}}