Over three days the UW Math AI lab, in collaboration with the UW PLSE Lab hosted students, faculty, and industry friends to hack with Lean, an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code. Teams worked on a variety of projects, including Formalized Origami; Rubik's cube solvers; and an Overleaf-to-Lean trust layer. Judges included academics and industry representatives, including Varun Pant (Amazon), Eric Klavins (ECE Chair), Jarod Alper (Math & Google DeepMind), Jesse Han (Math.Inc) and Sean Jensen-Grey; and the Hackathon was sponsored by the Amazon Automated Reasoning Group and organized by Jarod Alper, Gilbert Bernstein, Vasily Ilin, Eric Klavins, Zachary Tatlock, Ruofan (Michael) Zeng, Dhruv Bhatia and Oliver Flatt. The Hackathon started with a UW-PIMS Colloquium by Leonardo de Moura, the creator of Lean.