Lightnews — Scholar-powered news

Lean Focused Research Organization @lean-lang.org · 2d

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...

1 6

Lean Focused Research Organization @lean-lang.org · 14d

FYI: The tutorials were recorded at @simonsfoundation.org Lean Workshop for Mathematics and Physical Sciences. Read more here: leanprover-community.github.io/blog/posts/s...

1 2

Lean Focused Research Organization @lean-lang.org · 14d

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...

1 3 13

Lean Focused Research Organization @lean-lang.org · 15d

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

1 4

Lean Focused Research Organization @lean-lang.org · 20d

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...

5

Lean Focused Research Organization @lean-lang.org · 20d

Fun to see snippets of #LeanLang interspersed into this fantastic @3blue1brown.com guest video by @bensyversen.bsky.social about Euclid's Elements!

Grant Sanderson @3blue1brown.com · 20d

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

4

Lean Focused Research Organization @lean-lang.org · 22d

🎉 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

5 20

Lean Focused Research Organization @lean-lang.org · 28d

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

6 11

Reposted by Lean Focused Research Organization

dan @danabra.mov · Sep 2

⚛️📝 New on Overreacted: Lean for JavaScript Developers

Lean for JavaScript Developers — overreacted

Programming with proofs.

overreacted.io

5 14 98

Lean Focused Research Organization @lean-lang.org · Sep 5

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...

7 15

Lean Focused Research Organization @lean-lang.org · Aug 15

🎉 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

1 7 24

Reposted by Lean Focused Research Organization

Emma R. Hasson @dodecalemma.bsky.social · Aug 7

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

6 23

Lean Focused Research Organization @lean-lang.org · Aug 6

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

2 4

Lean Focused Research Organization @lean-lang.org · Aug 6

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

5 8

Lean Focused Research Organization @lean-lang.org · Aug 5

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

Lean Programming Language

Lean is a theorem prover and programming language that enables correct, maintainable, and formally verified code.

lean-lang.org

5 11

Lean Focused Research Organization @lean-lang.org · Jul 15

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." 🎉

1 1 2

Lean Focused Research Organization @lean-lang.org · Jul 15

The first volume of the new Open Access journal "Annals of Formalized Mathematics" was released today!

➡️ afm.episciences.org/volume/view/...

#FormalMath #Mathematics #OpenAccess

1 3 10

Reposted by Lean Focused Research Organization

José A. Alonso @jalonso.bsky.social · Jul 15

IMO 1996 P3: Lean 4 formalization. ~ David Renshaw. youtu.be/5NbYtDfXfR4 #ITP #LeanProver #Math

IMO 1996 P3: Lean 4 Formalization

YouTube video by David Renshaw

youtu.be

3 6

Reposted by Lean Focused Research Organization

xenaproject.bsky.social @xenaproject.bsky.social · Jul 6

Markus 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...

My first verified (imperative) program

One of the many exciting new features in the upcoming Lean 4.22 release is a preview of the new verification infrastructure for proving properties of imperative programs. In this post, I’ll take a fir...

markushimmel.de

1 7 18

Lean Focused Research Organization @lean-lang.org · Jul 11

Yes! Great post by Markus! And it provides a bit of a preview of some upcoming #LeanLang version 4.22 features. 😏

1

Lean Focused Research Organization @lean-lang.org · Jul 8

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 ❤️)

[New Blog Post] Doing Lean Dirty: Lean as a Jupyter Notebook Replacement https://lnkd.in/ejy9hE5z #lean4 | Philip Zucker

[New Blog Post] Doing Lean Dirty: Lean as a Jupyter Notebook Replacement https://lnkd.in/ejy9hE5z #lean4

www.linkedin.com

2 5

Lean Focused Research Organization @lean-lang.org · Jul 8

Right? But incredibly endearing.

3

Lean Focused Research Organization @lean-lang.org · Jul 8

This is an... unexpected use of the #LeanLang InfoView: unnamed.website/posts/bad-ap...

But we love the creativity!

#LeanProver #DevTools #Metaprogramming

“Bad Apple!!” But It’s 3288 Lean Tactics Spamming VSCode

Writing the most useless Lean tactic ever

unnamed.website

1 7 16

Lean Focused Research Organization @lean-lang.org · Jul 7

📣 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

2 10 28

Reposted by Lean Focused Research Organization

New Scientist @newscientist.com · Jul 7

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.

AI could be about to completely change the way we do mathematics

Computers can help ensure that mathematical proofs are correct, but translating traditional maths into a machine-readable format is an arduous task. Now, the latest generation of artificial intelligence models is taking on the job, and could change the face of maths research

www.newscientist.com

3 9