We are deeply grateful to ACM SIGPLAN for recognizing #LeanLang with the Programming Languages Software Award 2025 at #PLDI2025.

The citation states: "The Lean theorem prover is a remarkable software artifact. Grounded on strong theoretical and engineering foundations, Lean has had and continues to have a broad impact on industrial practice and scientific research."

Unquestionably, this recognition belongs to the community as much as it does the original authors - especially to the many mathematicians and contributors who have helped to build Mathlib to over 1.8M lines of code. As Soonho Kong said on accepting the award: "This award goes to the actual Lean community and all the people who love Lean and using Lean."

Thank you to everyone who has contributed to making formal mathematics more accessible and reliable!

#LeanProver #FormalMathmatics

#LiquidTypes are a lightweight way to specify and check code properties. What stands in the way of more widespread adoption?

Friday at 10:30, Catarina Gamboa presents our #PLDI2025 paper (with Abigail Reese and @alcides "Usability Barriers for Liquid Types."

Heading to #PLDI2025! Looking forward to the conference and excited to catch up with friends, colleagues, and collaborators from around the world.