@lean-lang.org.bsky.social
Supporting the Formal Mathematics revolution
Thorsten Altenkirch explains Gödel's Incompleteness Theorem on @computerphile.bsky.social, and shows some definitions in #LeanLang! 🎯
Watch here: www.youtube.com/watch?v=IuX8...
We're excited to share the Lean FRO Year 3 Roadmap today! It builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026.
➡️ Read the roadmap at lean-lang.org/fro/
#LeanProver #FormalMathematics #FormalVerification
From the journal "Aims and Scope": "We expect papers to be accompanied by formal proof artifacts...[and] reviewers and interested readers to look at code artifacts alongside papers." 🎉
15.07.2025 20:16 — 👍 2 🔁 1 💬 1 📌 0The first volume of the new Open Access journal "Annals of Formalized Mathematics" was released today!
➡️ afm.episciences.org/volume/view/...
#FormalMath #Mathematics #OpenAccess
IMO 1996 P3: Lean 4 formalization. ~ David Renshaw. youtu.be/5NbYtDfXfR4 #ITP #LeanProver #Math
15.07.2025 07:04 — 👍 6 🔁 3 💬 0 📌 0Markus Himmel has written a blog post about how to write a simple imperative program in Lean and then how to verify that the program is bug-free.
markushimmel.de/blog/my-firs...
Yes! Great post by Markus! And it provides a bit of a preview of some upcoming #LeanLang version 4.22 features. 😏
11.07.2025 20:09 — 👍 1 🔁 0 💬 0 📌 0
In the continuing saga of surprising things users do: This post over on LinkedIn features a custom made #LeanLang environment intended to replace a Jupyter Notebook, because, you know - why not? 👀
www.linkedin.com/posts/philip...
(With apologies to @jupyter.org ❤️)
Right? But incredibly endearing.
08.07.2025 21:04 — 👍 2 🔁 0 💬 0 📌 0
This is an... unexpected use of the #LeanLang InfoView: unnamed.website/posts/bad-ap...
But we love the creativity!
#LeanProver #DevTools #Metaprogramming
📣 We're excited to share the new lean-lang.org!
Relaunching our website was a key deliverable in our Year 2 roadmap to provide "improved navigation and access to valuable content, resources, and tools." We hope you like it!
#LeanLang #LeanProver
Computers can check whether mathematical proofs are correct, but only if they have been translated into a machine-readable form first. Now, AI has got surprisingly good at this translation - which could transform the way maths is done.
07.07.2025 10:15 — 👍 9 🔁 3 💬 0 📌 1
Thanks for the fix!
30.06.2025 21:36 — 👍 0 🔁 0 💬 0 📌 0
Really enjoyed this talk by @harrisongoldste.in that demonstrates inventive uses of the #LeanLang InfoView enhanced by metaprogramming techniques to display real-time testing data.
#LeanProver #Metaprogramming #VSCode #PropertyTesting
📣 #LeanLang v4.21 is released! This release brings 295 changes, including feature additions, bug fixes, refactors, documentation improvements and performance improvements, in support of our Y2 roadmap: lean-fro.org/about/roadma...
➡️ See the full changelog here: lean-lang.org/doc/reference/
Core Memory #22 with @ashleevance.bsky.social features a conversation with @adammarblestone.bsky.social and @anastasiag.bsky.social on science funding and FROs with a segment on #LeanLang and its importance to formal verification and AI research.
🎥 www.youtube.com/watch?v=Gbu6...
In this 10-minute UCLA Connect talk, Terence Tao provides an accessible and compelling argument for "citizen math" and broad collaboration in research #mathematics via #formalverification using proof assistants like #LeanLang.
🎥 www.youtube.com/watch?v=K376...
This belongs to our amazing community - mathematicians building Mathlib (1.8M+ lines!), engineers at AWS/Microsoft/beyond doing critical verification work, and researchers pushing formal methods forward.
Thank you to everyone making formal mathematics and software verification more accessible! 🙏
The citation states: "The Lean theorem prover is a remarkable software artifact... Lean has had and continues to have a broad impact on industrial practice and scientific research... formal methods based on Lean will play a central role in mathematics in the years to come".
20.06.2025 04:04 — 👍 2 🔁 1 💬 1 📌 0
Incredibly grateful to @sigplan.bsky.social and @sigplan-pldi.bsky.social for awarding #LeanLang the Programming Languages Software Award 2025 at #PLDI2025!
#LeanProver #FormalMethods #ProgrammingLanguages #Mathematics #SoftwareVerification
Lean won the SIGPLAN Programming Languages Software Award 2025
#LeanLang #LeanProver
In a few days there will be a much better text at @lean-lang.org's site, but here is all I could gather today:
dev.to/adolfont/lea...
Thanks for sharing this great write up! We're thrilled that #LeanLang has been acknowledged by the SIGPLAN awards committee with this award. It's truly a testament to all the amazing work the community has accomplished in recent years!
19.06.2025 20:03 — 👍 1 🔁 1 💬 0 📌 0Congrats! We're excited to see what projects come from expMath!
19.06.2025 15:17 — 👍 2 🔁 1 💬 0 📌 0Cryspen is excited to announce it has been awarded a grant from the Ethereum Foundation to extend our hax verification toolchain with support for the Lean prover. Watch this space for more on this soon!
#FormalVerification #Lean #Rust
Very exciting! Looking forward to learning more!
18.06.2025 15:58 — 👍 1 🔁 0 💬 0 📌 0We're grateful to the PLDI organizers for this opportunity to share Lean's journey with such a vibrant community. For those attending or interested in formal verification, this promises to be an insightful discussion about where our field is headed!
17.06.2025 23:12 — 👍 1 🔁 0 💬 0 📌 0
📣 This week, #LeanLang Chief Architect Leonardo de Moura will deliver a keynote in Seoul at #PLDI2025 titled "Lean: Machine-Checked Mathematics and Verified Programming, Past and Future."
#pldi #formalmethods #programminglanguages #leanprover
Oh gosh. Thanks @haskell.org. 🤩
16.06.2025 22:59 — 👍 2 🔁 0 💬 0 📌 0
🎉 #LeanLang 0.1 was released 11 years ago today!
Lean had been in development since July 15, 2013, but Lean 0.1 was a major milestone. The screencap is a @waybackmachine.bsky.social 06/26/2014 snapshot from the @lean-lang.org GitHub, "Updated 10 days ago"!
#LeanProver #ProgrammingHistory
