Alexandre Rademaker

Lean 4.30.0 is live! The release notes highlight four areas: a new 𝚜𝚢𝚖 => tactic, 𝚌𝚋𝚟 out of experimental, a completed LCNF compiler backend, and a full Lake cache overhaul. On 𝚜𝚢𝚖 =>: "Unlike 𝚐𝚛𝚒𝚗𝚍 =>, which eagerly introduces hypotheses and applies proof by contradiction, 𝚜𝚢𝚖 => gives users explicit control over each step." On the compiler: the expand reset/reuse port "results in a ~15% decrease in binary size and slight speedups across the board." Full release notes: lean-lang.org/doc/reference/…

Recordings and slides from Software Verification in Lean 2026 are now available. The one-day workshop and multi-day hackathon, held in Paris in April, brought together researchers from the Beneficial AI Foundation, @CryspenHQ, @ethereumfndn, @GoogleResearch, @leanprover, @MSFTResearch and others to share recent advances in building verified software. Recordings: youtube.com/playlist?list=… SVIL website: beneficial-ai-foundation.github.io/SVIL2026/ #LeanLang #LeanProver #FormalVerification #SoftwareVerification

"...the largest single-purpose Lean formalization in history." Wow. We're absolutely floored by this. Congrats to @SidharthHariha1 and @mathematics_inc!

Once we formalize the syntax of a language, the next step is to formalize its semantics: what programs mean and how they behave. There are three classical approaches. 1) Operational semantics Operational semantics defines meaning by describing how programs execute on an abstract machine. A machine state is typically just a term of the language, and evaluation proceeds by transitions between states. In small step semantics, execution is modeled as a sequence of reduction steps. In big step semantics, evaluation relates a term directly to its final value. Different operational presentations can model different levels of abstraction, and proving their correspondence amounts to proving implementation correctness. Operational semantics answers the question: how does this program run? 2) Denotational semantics Denotational semantics abstracts away from execution and maps programs directly to mathematical objects such as numbers, functions, or more structured semantic domains. Instead of describing steps of evaluation, we define an interpretation function from syntax to a semantic domain. This perspective enables equational reasoning, compositionality, and deep connections with domain theory. Denotational semantics answers the question: what mathematical object does this program denote? 3) Axiomatic semantics Axiomatic semantics shifts the focus from behavior to provable properties. Rather than defining execution and then deriving laws, it takes logical rules as primary. The meaning of a program is given by what can be proven about it. This tradition gave us foundational ideas such as invariants and Hoare logic, emphasizing reasoning as central to programming. Operational semantics models execution. Denotational semantics models mathematical meaning. Axiomatic semantics models provability. For students and engineers working in PL, compilers, or formal verification, understanding these three perspectives is essential. They are not competing views. They are complementary lenses on what programs are and what it means for them to be correct.

The CSLib steering committee recently announced the official launch of CSLib — an open-source effort to formalize computer science in Lean, inspired by the impact of Mathlib in mathematics. CS researchers, practitioners, and enthusiasts are invited to get involved to support formalizing essential computer science concepts, and building infrastructure for reasoning about real-world code with Lean. Learn more at: 🌐 cslib.io 📄 White paper: arxiv.org/abs/2602.04846 🤝 Contribute: github.com/leanprover/csl… #LeanLang #LeanProver #CSLib #OpenSource #FormalVerification

In this highly accessible talk, Terence Tao outlines the future of research mathematics and why formal verification, via Lean and other tools, enables human-AI collaboration at scale: "The reason why scaling and AI and broad participation actually is a net win is because we have formal verification... we have ways to filter out the untrustworthy inputs and keep the good ones." 📺 youtube.com/watch?v=SuTxpK… #LeanLang #LeanProver #FormalVerification

New from Steven Levy in @WIRED: a look at AI reliability and the hallucination problem. While opinions vary on agentic AI's future, formal methods stand out for tasks requiring mathematical rigor, and Lean is highlighted specifically for its verification capabilities. For tasks that can be modeled formally, verification makes the difference between unreliable and dependable. Read the full article: wired.com/story/ai-agent… #LeanLang #LeanProver #FormalVerification #AI

@vivobr péssima empresa ... reclameaqui.com.br/vivo-celular-f…

Simons Foundation Lean Workshop. ~ Antoine Chambert-Loir. Alex Kontorovich, Heather MacBeth. leanprover-community.github.io/blog/posts/sim… #ITP #LeanProver

14. @emiyazono on how to ensure American AI models are robust and reliable via a DOD-led red- and blue-teaming effort: ifp.org/preventing-ai-…

@mark_l_watson Did you try github.com/xenodium/chatg…? I didn’t know about ellama, thanks for sharing.

I am running Mistral’s new devstral model with Ollama and I configured Emacs+ellama and VSCode to use it. For a 24B model it really does a fine job as a local on-device chat and code completion assistant.

@srivatsamath @lisperati @stylewarning @leanprover Do you have any particular benchmark used to make this claim? I would be really interested in details about it.

@lisperati @stylewarning I defected to @leanprover

@stylewarning Note that I'm the guy who drew the cartoon, and I usually have a policy against posting AI pictures, but I just had to know...

I appreciate Matthias Zenger’s LispPad app for iPadOS/iOS/macOS that provides a workable Scheme implementation and IDE. Batteries included: lisppad.app/libraries/lisp…

We should be governing AI systems with rules, not values. I (finally) wrote up ~4k words on why we need complementary approaches to alignment. blog.atlascomputing.org/p/govern-ai-wi…

@mark_l_watson Interesting. I am trying to understand the details of some LLM low level parameters and templates exactly to overcome the limitations of using only Python libraries. Can you say more about what you learned so far?

For the last 12 years most of my paid work has used Python because the tools and infrastructure are there for machine learning, deep learning, and tooling around training and tuning LLMs. I was asking Google’s new AI Mode search about agentic frameworks written in Common Lisp - just a fun topic to ‘kick the tires’ and try out the Gemini experimental search integration (it is very good, BTW). One advantage of having LLM access via RESTful API calls to local models or commercial APIs is that developers of more complex AI applications and of agentic frameworks are free to now use Common Lisp, Haskell, Rust, Swift, or any other language they feel comfortable building (and maintaining!) complex systems. For certain applications Python is truly a wonderful language but it is not my personal choice for large software projects.

I just completed "Probably a Fire Hazard" - Day 6 - Advent of Code 2015 adventofcode.com/2015/day/6 #AdventOfCode in #Lean! Having some fun!

@TIMBrasil poderia cumprir sua parte já que estou cumprindo a minha de pagar o serviço conforme combinamos?

Internet no Brasil pela TIM… nosso 4G é isso!

Set Theory Game (An introduction to mathematical proof). ~ Daniel J. Velleman. adam.math.hhu.de/#/g/djvelleman… #ITP #Lean4 #Math