@ashblacquiere.bsky.social
Ops @leanprover
That sounds dizzying... Hope you got some sleep. 😴
17.06.2025 00:10 — 👍 0 🔁 0 💬 0 📌 0Sounds like an exciting talk! Will your slides be publicly available?
12.06.2025 17:16 — 👍 0 🔁 0 💬 1 📌 0
Bhavik Mehta delivered a talk about this at Big Proof this morning, and also announced that a substantial portion of the full proof has been completely *autoformalized* by Morph Labs' AI new model "Trinity".
www.youtube.com/watch?v=zLqh...
Here's the video: www.youtube.com/watch?v=zLqh...
12.06.2025 16:03 — 👍 3 🔁 0 💬 0 📌 0This is very cool. Nice to see #LeanLang verification via Aeneas!
10.06.2025 20:07 — 👍 1 🔁 0 💬 0 📌 0
The Lean Language Reference does some of this too. lean-lang.org/doc/referenc...
05.06.2025 00:16 — 👍 2 🔁 0 💬 0 📌 0chickenchase.swift? henhorse.swift? 😂
03.06.2025 20:41 — 👍 0 🔁 0 💬 1 📌 0
Check out these great UX improvements in Lean 4.18!
✅ New gutter decorations for errors/warnings
🔧 "Unsolved goals" markers to guide your proof
🐙 "Goals accomplished!" celebrations
▶️ Try these now in the Lean4 VSCode extension: marketplace.visualstudio.com/items?itemNa...
#LeanLang #LeanProver
Excited to share the recent @simonsfoundation.org talk by
@leodemoura.bsky.social: It's a great overview of how #LeanLang is paving the way to a more reliable and collaborative future in math, software & AI!
Watch here: www.youtube.com/watch?v=rmMY...
#LeanProver #FormalVerification #Mathematics
Big congrats to 14-y.o. Daniel whose #Exporecerca project using #LeanLang to formalize Math Olympiad problems netted him an award from the Royal Society for Sciences and Arts in Barcelona! #LeanProver engineer Anne Baanen had a great chat with him about his award-winning project!
19.03.2025 22:27 — 👍 9 🔁 1 💬 0 📌 1
👩💻Lean users: Lean 4.17 adds inlay hints for automatically-inserted implicit parameters: With autoImplicit enabled you’ll see in-editor visual feedback for parameters that Lean has automatically inferred, improving readability and making code less error-prone!
#LeanLang #LeanProver #DeveloperTools
The #LeanLang Standard Library, under active development at the Lean FRO, envisions providing a reliable and extensible basis for #softwaredevelopment, #softwareverification and #mathematics through verified components, a high-quality API, performance optimization, and best-in-class documentation.
05.03.2025 19:29 — 👍 8 🔁 4 💬 0 📌 0
Reservoir: More than a package registry - it's a leap forward in managing #LeanLang's ecosystem: Beyond storage to comprehensive compatibility and development. Our cloud build cache is live, preliminary private packages support is here, and FFI improvements are on the way.
➡️ reservoir.lean-lang.org
A logo for the Lean theorem prover
We're excited to join Bluesky! The Lean FRO develops Lean, an interactive theorem prover and functional programming language advancing mathematics, formal verification, and AI. Follow us for updates on our roadmap and community. #leanlang #leanprover #mathematics #formalverification #ai
26.02.2025 22:04 — 👍 36 🔁 12 💬 0 📌 0This article by @adammarblestone.bsky.social brilliantly illustrates how Lean and other proof assistants are enabling new forms of mathematical collaboration and verification in our AI-driven world. We're grateful for Adam's valuable guidance as a board member of the Lean FRO!
#LeanLang #LeanProver
