Lean Hackathon @ ETH-ITS Zurich

Venue:
ITS Seminar Room B 15.2, Scheuchzerstrasse 70, Zurich

Organizer:
Dr. Sorrachai Yingchareonthawornchai (ETH-ITS Junior Fellow)

Abstract:
Despite the success of Mathlib in establishing Lean as a leading platform for formalized mathematics, a significant gap remains in its support for algorithmic reasoning and analysis. In contrast to other proof assistants such as Isabelle and Coq, where substantial infrastructure exists for reasoning about programs and complexity, Lean currently lacks a unified and reusable foundation for formalizing algorithms. This limitation reduces its applicability in theoretical computer science, particularly in areas that require precise reasoning about efficiency and correctness.

This Lean hackathon will focus on developing foundational infrastructure for algorithm analysis in Lean, with the long-term goal of contributing to CSLib. Topics will include, but are not limited to, core definitions of graphs, data structures, and time complexity, providing the building blocks for rigorous reasoning about algorithms.