BEGIN:VCALENDAR
VERSION:2.0
PRODID:researchseminars.org
CALSCALE:GREGORIAN
X-WR-CALNAME:researchseminars.org
BEGIN:VEVENT
SUMMARY:Leo de Moura (Lean FRO and AWS)
DTSTART:20260119T173000Z
DTEND:20260119T183000Z
DTSTAMP:20260420T025042Z
UID:LT2026/6
DESCRIPTION:Title: <a href="https://researchseminars.org/talk/LT2026/6/">T
 he State of Lean</a>\nby Leo de Moura (Lean FRO and AWS) as part of Lean T
 ogether 2026\n\n\nAbstract\n2025 has been a transformative year for Lean. 
 We released 12 versions (4.15–4.26)\, landing thousands of changes acros
 s proof automation\, the compiler\, tooling\, website\, documentation\, an
 d the standard library. The grind tactic shipped with SMT-style automation
  and interactive proof search. The new compiler replaced the old one\, clo
 sing long-standing issues and setting the foundation for future optimizati
 ons. Lake gained remote caching and a local artifact cache. The language s
 erver became significantly faster (3.5× autocomplete speedup)\, added sig
 nature help\, and introduced module hierarchy navigation. We released the 
 module system\, coinductive predicates\, and a monadic verification framew
 ork (mvcgen). The standard library expanded substantially with iterators\,
  async primitives\, and hundreds of new lemmas. We launched a new website 
 and published the Lean Language Reference\, both built with Verso. This ke
 ynote summarizes these accomplishments and outlines our priorities for 202
 6.\n
LOCATION:https://researchseminars.org/talk/LT2026/6/
END:VEVENT
END:VCALENDAR