#leanlang — Public Fediverse posts
Live and recent posts from across the Fediverse tagged #leanlang, aggregated by home.social.
-
I've been trying to get a better idea about how the LEAN theorem prover works. I found their documentations pretty useless - incoherent walls of text. Youtube wasnt much better, except for this video that manages to explain the fundamental proposition=type equivalence all the way to using Lean to prove there are infinitely many primes, all within about 30 minutes.
https://m.youtube.com/watch?v=0QZI_m8WZ0Q
If anyone can recommend other good Lean intros I'd be grateful.
-
I've been trying to get a better idea about how the LEAN theorem prover works. I found their documentations pretty useless - incoherent walls of text. Youtube wasnt much better, except for this video that manages to explain the fundamental proposition=type equivalence all the way to using Lean to prove there are infinitely many primes, all within about 30 minutes.
https://m.youtube.com/watch?v=0QZI_m8WZ0Q
If anyone can recommend other good Lean intros I'd be grateful.
-
𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings 208 changes, including a more responsive editor, automatic proof suggestions, and 𝙵𝚕𝚘𝚊𝚝 no longer being an opaque type. Notable improvements include:
⚡ Editing feels smoother: the editor now preserves your progress when you press return after a tactic, and proof-search tactics respond faster near the top of long files
✨ 𝚝𝚛𝚢? can now suggest proofs automatically at empty proofs, unsolved goals, or 𝚜𝚘𝚛𝚛𝚢, with no change needed to how proofs are written
🧠 The 𝚕𝚒𝚊 and 𝚐𝚛𝚒𝚗𝚍 tactics can now close more goals automatically, including ones involving 𝚖𝚒𝚗/𝚖𝚊𝚡 and bitvector arithmetic
🔧 𝙵𝚕𝚘𝚊𝚝 numbers now have a logical model behind them, letting downstream libraries build and verify their own theorems about floating-point behavior
𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lean-lang.org/doc/reference/latest/releases/v4.33.0/
#LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification
-
𝐋𝐞𝐚𝐧 𝟒.𝟑𝟑.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release brings 208 changes, including a more responsive editor, automatic proof suggestions, and 𝙵𝚕𝚘𝚊𝚝 no longer being an opaque type. Notable improvements include:
⚡ Editing feels smoother: the editor now preserves your progress when you press return after a tactic, and proof-search tactics respond faster near the top of long files
✨ 𝚝𝚛𝚢? can now suggest proofs automatically at empty proofs, unsolved goals, or 𝚜𝚘𝚛𝚛𝚢, with no change needed to how proofs are written
🧠 The 𝚕𝚒𝚊 and 𝚐𝚛𝚒𝚗𝚍 tactics can now close more goals automatically, including ones involving 𝚖𝚒𝚗/𝚖𝚊𝚡 and bitvector arithmetic
🔧 𝙵𝚕𝚘𝚊𝚝 numbers now have a logical model behind them, letting downstream libraries build and verify their own theorems about floating-point behavior
𝐅𝐮𝐥𝐥 𝐫𝐞𝐥𝐞𝐚𝐬𝐞 𝐧𝐨𝐭𝐞𝐬: https://lean-lang.org/doc/reference/latest/releases/v4.33.0/
#LeanLang #LeanProver #ProofAssistant #OpenSource #FormalVerification
-
Lean 4.32.0 is released, with 102 changes total, including the new do elaborator, introduced experimentally in 4.29, is now the default. The legacy elaborator remains available via backward.do.legacy for anyone who needs it.
Also in this release:
A new module linter framework, letting checks run once per module instead of after every command, useful for enforcing whole-module conventions.
A round of fixes and refinements to mvcgen' and grind, making the two easier to use together in a single proof.
Several performance improvements, including roughly 10% faster Mathlib imports and a much faster way to combine large collections of bitvectors.Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.32.0/
-
Lean 4.32.0 is released, with 102 changes total, including the new do elaborator, introduced experimentally in 4.29, is now the default. The legacy elaborator remains available via backward.do.legacy for anyone who needs it.
Also in this release:
A new module linter framework, letting checks run once per module instead of after every command, useful for enforcing whole-module conventions.
A round of fixes and refinements to mvcgen' and grind, making the two easier to use together in a single proof.
Several performance improvements, including roughly 10% faster Mathlib imports and a much faster way to combine large collections of bitvectors.Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.32.0/
-
Lean 4.31.0 is released.
This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.
Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.
Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.31.0/
-
Lean 4.31.0 is released.
This consolidation-heavy release brings 305 changes. For those working on verified software: repeat/while loops are now verifiable without requiring source changes, expanding through whileM to support a one-step unfolding lemma. The new experimental mvcgen' tactic, reimplemented from the ground up on the SymM-based symbolic evaluation framework, can outperform mvcgen by a factor of over 100x on some synthetic benchmarks.
Library authors and package maintainers also gain a built-in linting framework through lake lint, with linters upstreamed from Batteries and Mathlib.
Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.31.0/
-
#LeanLang 0.1 was released 12 years ago today! The creator of Lean is Brazilian. His name is Leonardo de Moura. xcancel.com/leanprover/s...
-
#LeanLang 0.1 was released 12 years ago today! The creator of Lean is Brazilian. His name is Leonardo de Moura. xcancel.com/leanprover/s...
-
The Proof in the Code: How a Truth Machine Is Transforming Math and AI
by Kevin Hartnett
#LeanLang #Lean4 #LeanProver
https://amzn.to/4xnAIj8 -
The Proof in the Code: How a Truth Machine Is Transforming Math and AI
by Kevin Hartnett
#LeanLang #Lean4 #LeanProver
https://amzn.to/4xnAIj8 -
"Can we prove that Signal's cryptography is secure — not just on paper, but in actual code?"
Signal Shot, launched today at the Software Verification in Lean workshop in Paris, is a public moonshot to formally verify the Signal protocol and its Rust implementation using Lean. A joint effort of Signal, the Beneficial AI Foundation, and the Lean FRO.
Open to contributions from anyone working on software verification, cryptography, protocol design, Rust, or Lean.
-
"Can we prove that Signal's cryptography is secure — not just on paper, but in actual code?"
Signal Shot, launched today at the Software Verification in Lean workshop in Paris, is a public moonshot to formally verify the Signal protocol and its Rust implementation using Lean. A joint effort of Signal, the Beneficial AI Foundation, and the Lean FRO.
Open to contributions from anyone working on software verification, cryptography, protocol design, Rust, or Lean.
-
Lean 4.29.0 released with 453 changes.
Highlights: reduced startup time through static initialization of closed terms, simpler 𝚗𝚘𝚗𝚌𝚘𝚖𝚙𝚞𝚝𝚊𝚋𝚕𝚎 semantics improving predictability, higher-order Miller pattern support in 𝚐𝚛𝚒𝚗𝚍's e-matching engine, and a significant overhaul to instance and reducibility handling.
Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.29.0/
-
Lean 4.29.0 released with 453 changes.
Highlights: reduced startup time through static initialization of closed terms, simpler 𝚗𝚘𝚗𝚌𝚘𝚖𝚙𝚞𝚝𝚊𝚋𝚕𝚎 semantics improving predictability, higher-order Miller pattern support in 𝚐𝚛𝚒𝚗𝚍's e-matching engine, and a significant overhaul to instance and reducibility handling.
Full release notes: https://lean-lang.org/doc/reference/latest/releases/v4.29.0/
-
"ZK proofs are headed for real-world deployment — but writing correct ZK statements is tricky.
Our new post by James Parker introduces zkLean, a Lean library that defines a domain specific language for specifying and formally verifying ZK statements."
#LeanLanghttps://www.galois.com/articles/zklean-a-dsl-for-zk-statement-verification
-
"ZK proofs are headed for real-world deployment — but writing correct ZK statements is tricky.
Our new post by James Parker introduces zkLean, a Lean library that defines a domain specific language for specifying and formally verifying ZK statements."
#LeanLanghttps://www.galois.com/articles/zklean-a-dsl-for-zk-statement-verification
-
Leanstral: Open-Source foundation for trustworthy vibe-coding
by Mistral AI
#LeanLang
https://mistral.ai/news/leanstral -
Leanstral: Open-Source foundation for trustworthy vibe-coding
by Mistral AI
#LeanLang
https://mistral.ai/news/leanstral -
The next bi-monthly #Mathlib community meeting is tomorrow Friday, 13th at 3pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with other contributors!
➡️ See all upcoming community events on our website: http://lean-lang.org/community/#events
-
The next bi-monthly #Mathlib community meeting is tomorrow Friday, 13th at 3pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with other contributors!
➡️ See all upcoming community events on our website: http://lean-lang.org/community/#events
-
I am deeply disappointed by Terence Tao's uncritical use of AI.
-
I am deeply disappointed by Terence Tao's uncritical use of AI.
-
The next Lean FRO office hours are Feb. 11 at 4pm UTC. Bring your questions, share your projects, or just come to learn from others in the community!
See our full calendar here: https://lean-lang.org/community/#events
-
The next Lean FRO office hours are Feb. 11 at 4pm UTC. Bring your questions, share your projects, or just come to learn from others in the community!
See our full calendar here: https://lean-lang.org/community/#events
-
CSLib
A Focused Effort on Formalizing Computer Science in Lean
#LeanLang
https://www.cslib.io -
CSLib
A Focused Effort on Formalizing Computer Science in Lean
#LeanLang
https://www.cslib.io -
I am new to #LeanLang. I notice resources like the Natural Number Game or the official recommended texts (https://lean-lang.org/learn/).
Just wanna ask whether there are people want to learn Lean together. Maybe form a small study group in Discord (or elsewhere).
-
ITP 2025 Lean Workshop videos https://youtube.com/playlist?list=PL0oY24ee23INkDNXVoUMBZZ-q_EzE6gwx
-
ITP 2025 Lean Workshop videos https://youtube.com/playlist?list=PL0oY24ee23INkDNXVoUMBZZ-q_EzE6gwx
-
New Lean use case: AWS's Cedar authorization policy language verified with Lean, using "verification-guided development", and integrated into Cedar's development workflow.
➡️Read more: https://lean-lang.org/use-cases/cedar
-
The Mathlib Initiative website is live!
#LeanLang
https://mathlib-initiative.org/ -
We released #LeanLang 4.22.0 yesterday. This release marks the culmination of our Year 2 roadmap, and we're particularly excited to announce the official release of:
The new 𝚐𝚛𝚒𝚗𝚍 tactic, an SMT-style tactic that includes theory-specific solvers (including cutsat) and a new Gröbner basis solver.
The new Lean compiler which closes many long-standing issues, and lays the foundation for many future features and performance improvements.
In addition, this release includes 468 changes total, with 185 feature additions and 85 fixes, setting the stage for more advancements as Lean FRO enters its third year of operations.
Full release notes here: https://lean-lang.org/doc/reference/latest/releases/v4.22.0/
-
Lean FRO Year 3 Roadmap https://www.youtube.com/watch?v=xIHGNZRivFM
-
We're excited to share the Lean FRO Year 3 Roadmap today! This roadmap builds on work completed in the first two years of Lean FRO operations and will guide all #LeanLang development through July 2026. Read the full document at https://lean-lang.org/fro/ for details on our seven key priority areas.
-
I'm learning how to write formal proofs with #LeanProver so I decided to formalize the introduction of some paper in #LeanLang. Unexpectedly, I found a typo in one equation after my attempt at proving it failed.
-
[New Blog Post] Using Lean like an External SMT Solver from Python https://www.philipzucker.com/lean_smt/ #LeanLang @leanprover
