Log inSign up
Lean
777 posts
Image
user avatar
Lean
@leanprover
Lean is a dependently-typed programming language and theorem prover.
Seattle
lean-lang.org
Joined April 2018
50
Following
11.1K
Followers
  • user avatar
    Lean
    @leanprover
    Oct 24, 2023
    Nice, Terence Tao (Fields Medal 2006) found a bug in one of his papers using Lean 4. mathstodon.xyz/@tao/111287749…
    Image
    349K
  • user avatar
    Lean
    @leanprover
    May 28, 2025
    🔥 @GoogleDeepMind just dropped their "formal conjectures" project - formalizing statements of math's biggest unsolved mysteries in #LeanLang and #Mathlib! This Google-backed project is a HUGE step toward developing "a much richer dataset of formalized conjectures", valuable
    Image
    100K
  • user avatar
    Lean
    @leanprover
    Jul 7, 2025
    📣 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
    Image
    44K
  • user avatar
    Lean
    @leanprover
    Nov 19, 2023
    Terry Tao's blog post on the PFR project is essential reading for anybody interested in formal mathematics with Lean.
    Image
    Formalizing the proof of PFR in Lean4 using Blueprint: a short tour
    From terrytao.wordpress.com
    103K
  • user avatar
    Lean
    @leanprover
    Aug 15, 2025
    🎉 Lean 4.22.0 is here! This marks the culmination of our Year 2 roadmap. Two major highlights: 🧠 grind tactic: New SMT-style automated reasoning with theory-specific solvers and Gröbner basis support 🏗️ New compiler: Closes long-standing issues and sets the foundation for
    Image
    21K
  • user avatar
    Lean
    @leanprover
    Jun 3, 2025
    Terence Tao has released a new #LeanLang project that connects #FormalVerification with #MathematicsEducation: The companion to "Analysis I" is intended to provide a new avenue for engaging with the proofs and exercises in Tao's foundational "Analysis I" text. 👇
    24K
  • user avatar
    Lean
    @leanprover
    Nov 28, 2023
    DeepMind has formalized a theoretical result related to AI safety in Lean. 😍 Paper: arxiv.org/abs/2311.14125. Code: github.com/google-deepmin…
    arXiv logo
    arxiv.org
    Scalable AI Safety via Doubly-Efficient Debate
    The emergence of pre-trained AI systems with powerful capabilities across a diverse and ever-increasing set of complex domains has raised a critical challenge for AI safety as tasks can become too...
    91K
  • user avatar
    Lean
    @leanprover
    Oct 20, 2023
    We are super excited to see daily updates from Terence Tao describing his experience learning Lean. Terence Tao is one of the greatest living mathematicians and a Fields medalist.
    Showing that if a polynomial vanishes then all of its coefficients vanish. The fact that the monomials are given in descending order rather than ascending creates a surprisingly tricky obstacle to formally establishing this fact (basically one needs to encode the fact that reflection k -> n-k is injective on {0,...,n}).
    Terence Tao (@[email protected])
    From mathstodon.xyz
    69K
  • user avatar
    Lean
    @leanprover
    Oct 31, 2023
    Morph.so just announced Moogle (moogle.ai), a semantic search engine for Mathlib, the Lean mathematical library. You can now find theorems using natural language. 😍
    Image
    GIF
    43K
  • user avatar
    Lean
    @leanprover
    Jul 25, 2023
    We are excited to share the news of the Lean Focused Research Organization (FRO): lean-fro.org! A new nonprofit dedicated to advancing the Formal Mathematics revolution, we aim to tackle the challenges of scalability, usability, and proof automation in Lean.
    Lean Programming Language
    Lean Programming Language
    From lean-lang.org
    76K
  • user avatar
    Lean
    @leanprover
    Sep 11, 2025
    Congratulations to the @mathematics_inc team on their announcement! AI-assisted autoformalization is a promising area with significant potential impact. We're looking forward to the community discussion and seeing how this space evolves. #AI #ProofAutomation #FormalMathematics
    user avatar
    Math, Inc.
    @mathematics_inc
    Sep 11, 2025
    Today we're announcing Gauss, our first autoformalization agent that just completed Terry Tao & Alex Kontorovich's Strong Prime Number Theorem project in 3 weeks—an effort that took human experts 18+ months of partial progress.
    19K
  • user avatar
    Lean
    @leanprover
    Oct 20, 2025
    "Theorem Proving in Lean 4" is the essential guide for anyone using Lean for mathematical proofs. This comprehensive resource is kept up-to-date with each new Lean release, ensuring all examples and techniques remain current with the latest Lean developments. It covers
    Image
    17K
  • user avatar
    Lean
    @leanprover
    Jul 24, 2025
    Big day for Lean! Alex Gerko of XTX Markets is donating $10M to the Lean FRO and the new Mathlib Initiative to support the future of formal mathematics and machine-checked proofs. Thank you, Alex Gerko and Convergent Research, for believing in the mission. Read the full
    Image
    Lean FRO and Mathlib receive $10M from XTX Markets Founder Alex Gerko to further advance the use of...
    From renaissancephilanthropy.org
    14K
  • user avatar
    Lean
    @leanprover
    May 28, 2025
    We're excited to see #LeanLang featured in the new @Stanford course CS 99: 𝘍𝘶𝘯𝘤𝘵𝘪𝘰𝘯𝘢𝘭 𝘗𝘳𝘰𝘨𝘳𝘢𝘮𝘮𝘪𝘯𝘨 𝘢𝘯𝘥 𝘛𝘩𝘦𝘰𝘳𝘦𝘮 𝘗𝘳𝘰𝘷𝘪𝘯𝘨 𝘪𝘯 𝘓𝘦𝘢𝘯 4, led by Leni Aniva, Abdalrhman Mohamed and sponsored by Clark Barrett. ✨ The course hosts a fantastic
    13K

New to X?

Sign up now to get your own personalized timeline!

Create account

By signing up, you agree to the Terms of Service and Privacy Policy, including Cookie Use.

Terms of Service|Privacy Policy|Cookie Policy|Accessibility|Ads info|© 2026 X Corp.
Don't miss what's happening
People on X are the first to know.
Log inSign up