Lean Focused Research Organization
LightNews LightNews
banner
lean-lang.org
Lean Focused Research Organization
@lean-lang.org
500 followers 54 following 110 posts
Supporting the Formal Mathematics revolution
Posts Replies Media Videos
lean-lang.org
From The Geometry of Machine Learning at Harvard CMSA in Sept: Jared Duker Lichtman's talk explores Math, Inc. Gauss's contributions to number theory and how these results are being formalized in #LeanLang.

Watch here: www.youtube.com/watch?v=Ko-P...
Jared Duker Lichtman | Gauss – towards autoformalization for the working mathematician
YouTube video by Harvard CMSA
www.youtube.com
October 24, 2025 at 11:09 PM
lean-lang.org
Looking for a lemma in #LeanLang / #Mathlib but don't know its name? Use Loogle! to search:

By pattern: _ * (_ ^ _) finds expressions matching the pattern
By conclusion: |- tsum _ = _ * tsum _ finds specific conclusion shapes

Combine searches with commas for precision!
loogle.lean-lang.org
Loogle - Search Lean and Mathlib
Loogle is a search tool for finding definitions, theorems, and lemmas in Lean 4 and Mathlib.
loogle.lean-lang.org
October 23, 2025 at 9:09 PM
lean-lang.org
𝐋𝐞𝐚𝐧 𝟒.𝟐𝟒.𝟎 𝐢𝐬 𝐥𝐢𝐯𝐞! This release improves the module system, strengthens the 𝚐𝚛𝚒𝚗𝚍 tactic, and advances the standard library.
Key improvements: 3.5x faster auto-completion, streamlined "try this" suggestions, new 𝚐𝚛𝚒𝚗𝚍 AC solver, enhanced 𝚖𝚟𝚌𝚐𝚎𝚗 syntax.

Read more: lean-lang.org/doc/referenc...
October 23, 2025 at 12:01 AM
lean-lang.org
Tactic tip: Lean's 𝚜𝚒𝚖𝚙? is an optimization tool that shows the minimal 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call needed to close a goal.

Use the 𝚜𝚒𝚖𝚙? "Try this" suggestion to insert the precise 𝚜𝚒𝚖𝚙 𝚘𝚗𝚕𝚢 call into your proof.

Learn more: lean-lang.org/theorem_prov...

#LeanLang #LeanProver #ProofAssistant
October 22, 2025 at 11:06 PM
lean-lang.org
"Theorem Proving in Lean 4" is the essential guide for anyone using Lean for mathematical proofs. Kept up-to-date with each new Lean release, it covers everything from basic tactics to advanced proof strategies.

Read the book here: lean-lang.org/theorem_prov...

#LeanLang #LeanProver #Mathematics
October 20, 2025 at 11:34 PM
lean-lang.org
Reservoir is #LeanLang's package registry, inspired by crates.io (thanks @rustfoundation.org!) Browse community-created packages and discover new tools: reservoir.lean-lang.org

Sharing is easy! GitHub repos meeting the inclusion criteria are auto-indexed: reservoir.lean-lang.org/inclusion-cr...
October 16, 2025 at 11:36 PM
lean-lang.org
Speed up your #LeanLang workflow in #VSCode with shortcuts:

ℹ️Ctrl/Cmd+Shift+Enter: Open the InfoView

🔡Ctrl/Cmd+Shift+O: List current file declarations, namespaces and sections

🔄Ctrl/Cmd+Shift+X: Restart the current file

See more in the Lean VS Code extension manual: github.com/leanprover/v...
github.com
October 15, 2025 at 7:02 PM
lean-lang.org
#LeanLang office hours are tomorrow (Wednesday the 15th) at 23:00 UTC. Bring your questions, share your projects, or just come to learn from others in the community.

➡ Find calendar and meeting links on our website: lean-lang.org/community/#e...
Lean Programming Language
Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.
lean-lang.org
October 14, 2025 at 11:19 PM
lean-lang.org
New use case on our website: AWS's Cedar authorization policy language verified with Lean, using "verification-guided development", and integrated into Cedar's development workflow.

➡️Read more: lean-lang.org/use-cases/ce...

#LeanLang #LeanProver #CedarPolicy #FormalVerification #AWS
Lean Programming Language
Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.
lean-lang.org
October 14, 2025 at 11:18 PM
Reposted by Lean Focused Research Organization
pietromonticone.bsky.social
We’re pleased to announce #ItaLean2025: Bridging Formal Mathematics and AI, an international conference dedicated to @lean-lang.org, Formal Mathematics, and AI4Math.

📍 University of Bologna
🗓 9–12 December 2025

Proudly supported by #Harmonic.

#LeanLang #FormalMath #AI4Math
October 14, 2025 at 7:44 AM
lean-lang.org
💡Did you know you can run #LeanLang in your browser without installing anything? The Lean Playground provides a full environment for experimentation, learning, and for sharing code snippets with others.

Try it out! live.lean-lang.org
October 10, 2025 at 4:17 PM
lean-lang.org
The next bi-monthly #Mathlib community meeting is tomorrow (Friday Oct 10) at 2pm UTC. Join to hear about ongoing #LeanLang formalization projects and connect with contributors.

See all community events on our website:
lean-lang.org/community/?u...
Lean Programming Language
Lean is an open-source programming language and proof assistant that enables correct, maintainable, and formally verified code.
lean-lang.org
October 9, 2025 at 3:25 PM
lean-lang.org
Did you know the Info View in #LeanLang's #VSCode extension updates in real-time as you write proofs? Click on any part of your code to see the current proof state, goals, and hypotheses at that exact point.

Learn more about the Lean VS Code extension: github.com/leanprover/v...
October 6, 2025 at 5:52 PM
lean-lang.org
We really loved this series of tutorials on #metaprogramming in #LeanLang by Heather Macbeth. It's a great intro to a complex topic for novice users of #LeanProver!

Pt 1: youtube.com/watch?v=cKvg...
Pt 2: youtube.com/watch?v=5er4...
Pt 3: youtube.com/watch?v=TJ8T...
September 24, 2025 at 7:11 PM
lean-lang.org
Two great talks at #HLF25 last week: Sanjeev Arora on superhuman AI mathematicians using #LeanLang, and David Silver on AI learning through experience with #LeanProver verification.

www.youtube.com/watch?v=q9MJ...

#AI #FormalMath #ReinforcementLearning
Spark Session | September 15
YouTube video by Heidelberg Laureate Forum
www.youtube.com
September 23, 2025 at 6:00 PM
lean-lang.org
ICYMI: A great summary on the #LeanLang Community Blog of the @simonsfoundation.org 2025 MPS (Math and Phys Sciences) Workshop on #LeanProver.

The post includes links to lecture slides, videos, and a list of proposed projects and participants!

leanprover-community.github.io/blog/posts/s...
September 18, 2025 at 7:52 PM
lean-lang.org
Fun to see snippets of #LeanLang interspersed into this fantastic @3blue1brown.com guest video by @bensyversen.bsky.social about Euclid's Elements!
3blue1brown.com Grant Sanderson @3blue1brown.com · Sep 18
Much of Euclid’s Elements is easily misunderstood. Some proofs seem to have logical gaps. Some constructions seem pointless, others seem needlessly convoluted.

Each of these provides a window into how the ancient Greeks thought about math and the philosophical role that geometry played.
Why ruler and compass? | Guest video by ⁨@bensyversen⁩
YouTube video by 3Blue1Brown
youtu.be
September 18, 2025 at 6:23 PM
lean-lang.org
🎉 Lean 4.23.0 is here! Includes many usability improvements, including:

🎯 Enhanced 'Go to Definition' supporting type class instances

🔧 Interactive error hints for faster debugging

Release notes: lean-lang.org/doc/referenc...

#LeanLang #LeanProver #OpenSource #Mathematics #FormalVerification
September 16, 2025 at 6:46 PM
lean-lang.org
Recently came across @filiplajszczak.bsky.social's series formalizing a 1967 math textbook in #LeanLang.

Designed for those "with no prior experience with formalization" - nice bridge for newcomers to #LeanProver!

Read the intro post here: filip.lajszczak.dev/lean-4-with-...
Lean 4 with a Math Textbook - Part 0 - Introduction — Some opinions, held with varying degrees of certainty.
filip.lajszczak.dev
September 10, 2025 at 7:44 PM
Reposted by Lean Focused Research Organization
danabra.mov
⚛️📝 New on Overreacted: Lean for JavaScript Developers
Lean for JavaScript Developers — overreacted
Programming with proofs.
overreacted.io
September 2, 2025 at 3:42 PM
lean-lang.org
If you're you curious about #LeanLang and want to understand the connection between #programming and #proofs, check out this great new video by Ank Yog. The analogy between Chess and true propositions is particularly compelling!

www.youtube.com/watch?v=QXQN...
September 5, 2025 at 3:58 PM
lean-lang.org
🎉 Lean 4.22.0 is here! It represents the culmination of our Year 2 roadmap! Including:

🧠 New grind tactic (SMT-style automated reasoning)

🏗️ New compiler (major performance foundation)

Read the release notes: lean-lang.org/doc/reference/latest/releases/v4.22.0/

#LeanLang #LeanProver
August 15, 2025 at 7:40 PM
Reposted by Lean Focused Research Organization
dodecalemma.bsky.social
A refreshingly nuanced take on AI v. the International Math Olympiad by none other than Emily Riehl (@emilyriehl.bsky.social) for @sciam.bsky.social
AI Crushed the Math Olympiad—Or Did It?
AI models supposedly did well on International Math Olympiad problems, but how they got their answers reminds us why we still need people doing math
www.scientificamerican.com
August 7, 2025 at 3:13 PM
lean-lang.org
Just saw this post on LinkedIn about a new #DiscreteMath game on the #LeanLang Game Server. The author, Shrey Vivek, won a "Best Poster" award at the SPMS Odyssey Research Symposium. 🎉

The Discrete Math game: adam.math.hhu.de#/g/shreyvive...

The LinkedIn post: www.linkedin.com/posts/shrey-...
Lean Game Server
You need to enable JavaScript to use the Lean Game Server, as it is built using React.
adam.math.hhu.de
August 6, 2025 at 5:51 PM
lean-lang.org
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...
Gödel's Incompleteness Theorem - Computerphile
YouTube video by Computerphile
www.youtube.com
August 6, 2025 at 1:46 PM