I'm happy to announce pabst: a tool for Property-Based Testing in JavaScript/TypeScript. Annotate your functions with properties they're supposed to have, run `pabst test` to try to invalidate those claims, and watch the bugs come crawling out. Install via `npm install pabst-checker`,

Taking off now to A Coruña for the 2026 Web Engines Hackfest! Tons of great stuff on offer. Take a look at the program:

2026 Web Engines Hackfest

Web Platform community event for people working on the different engines (Chromium/Blink/V8, Safari/WebKit/JSC, Firefox/Gecko/SpiderMonkey, Servo, Ladybird), on the testing side (WPT, Test262), on…

webengineshackfest.org

Watching Terence Tao's cleanup of a Lean proof to meet Mathlib guidelines, I'm struck by the problem we're in of there being too much math. There are so many good Lean proofs coming out but essentially only one blessed outlet for them. "MathOverflow" indeed! www.youtube.com/watch?v=l3SC...

Golfing and stylistically aligning a proof using Claude Code

In this video, I demonstrate how an AI agent can be used to help check if a body of Lean code (intended for upstreaming to Mathlib) can be "golfed" (streamlined in presentation), and aligned with the…

youtube.com

I'm in Tsukuba, Japan for FLOPS 2026! After last week's Formal Methods symposium, this will be another packed week of learning. I'll be presenting a tutorial on Lean, extracted from my TypeScript-to-Lean compiler. functional-logic.org/events/flops...

Symposium on Functional and Logic Programming 2026 | Functional Logic Programming

18th International Symposium on Functional and Logic Programming

functional-logic.org

New blog post: On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications. proofsandintuitions.net/2026/05/18/p... The gist: randomised testing can validate formal specs. It's very cheap and powerful: we found bugs in specs of VERINA and CLEVER benchmarks.

Getting ready to attend day 1 of AI, Proof and Verification (AIPV) at Formal Methods 2026 in Tokyo. aipvconf.org

I'm on my way to Japan to attend Formal Methods. The agenda is absolutely packed with great stuff; really excited to learn a ton. It'll be my first time at FM. If you're interested in Lean & program verification, let's talk! conf.researchr.org/home/fm-2026

FM 2026

conf.researchr.org

I'm happy to announce Thales, a TypeScript compiler and JS engine in Lean. Thales compiles a subset of TypeScript to Lean via a shallow embedding. Thales is a bridge for TS programmers into Lean's program verification toolset. Check out github.com/jessealama/t... to get started.

Just learned about the Lean kernel arena from this post by Leo de Moura. With all the attention in the #lean space going to new features, massive growth of Mathlib, new initiatives like CSLib, this is something I'd never thought much about. leodemoura.github.io/blog/2026-3-...

Who Watches the Provers? — Leonardo de Moura

Leonardo de Moura — Creator of Lean and Z3

leodemoura.github.io

There are many tools for unprivileged sandboxing on Linux. You should probably go use one of them. But I wrote shandbox to scratch my itch muxup.com/shandbox /home/$user/sandbox shows up as /home/sandbox within the shared sandbox, which otherwise can only access explicitly mapped files/dirs.

shandbox

A simple shared sandbox using unshare+nsenter.

muxup.com

The program for Leaning In! 2026 is settled. We've got 11 (!) wonderful talks lined up. This is going to be a wonderufl time for digging into Lean, Registration is open, but space is limited so if you're thinking of coming, please do register soon. See you in Berlin! leaning.in/2026/

Leaning In! 2026

A workshop for the Lean community - Thursday, March 12, 2026

leaning.in

Amazing work on an Erdős problem (whose original statement needed to be tweaked), demonstrating the power of AI-assisted proving in math. mathstodon.xyz/@tao/1158558...

Lean Together 2026 starts today! It'll be four days of juicy Lean stuff. It's a remote-only conference, so feel free to join. See you there! leanprover-community.github.io/lt2026/

Really alarming to see this story of "LLM psychosis".I first saw it in a video by Nate Jones. It looks like there's an attempt to solve the wildly difficult Navier-Stokes problem, backed up by a Lean formalization. youtu.be/AzOJ9QLgfIk

If This Can Happen to an Ex-DeepMind Leader, It Can Happen to You

My site: https://natebjones.com Full Story w/ Self-Audit Framework:…

youtu.be

Claude Code helps me so much with the household chores. The dishes get washed more frequently, the apartment is appreciably tidier, the vacuum cleaner spends an above-average amount of time turned on, the trash gets taken out more quickly.

💥 Breaking news from my Inbox 💥 I saved 251 hours on email with @SaneBox in 2025 #UnwrapYourInbox See for yourself 👉 www.sanebox.com/unwrap/2pktu...

Get rid of email clutter

Try SaneBox today and get 2 weeks for free!

sanebox.com

TIL there's a JSON Schema validator for #lean at github.com/CAIMEOX/json... It seems to be abandoned, though (no activity for a year).

Enjoying the video from the December 2025 Mathlib community call.

Mathlib Community Meeting December 12, 2025

youtube.com

We''ve landed a few more talks since the last update! * Sorrachai Yingchareonthawornchai: The CSLib initiative * Simon Sorg: Machine learning for Lean * Jannis Limperg on Lean metaprogramming for AI * Will Turner on the new ProofBench effort Come join us for a day of #lean! leaning.in

Leaning In! 2026

A workshop for the Lean community - Thursday, March 12, 2026

leaning.in

Incredible results with #lean and Gemini Deep Think by Tao in the Erdős Problem. It feels like a lot of doors in the formalization space, whether that's math or hardware/software verification, are opening quickly. mathstodon.xyz/@tao/1155914...

The 2026 edition of the ITP (Interactive Theorem Proving) conference back in October featured a #lean event. It was great to be there and connect with so many Lean folks. The videos are finally available: www.youtube.com/playlist?lis...

ITP 2025 Lean Workshop

Share your videos with friends, family, and the world

youtube.com

Leaning In! 2026 is ON! If you like #lean and are in Berlin, Germany, Europe, or anywhere on Earth, you are invited. We've got a room at Spielfeld in Berlin. See you on March 12th! More information, including tickets and the CfP, here: leaning.in/2026/

Fascinating talk by Kevin Buzzard about where he sees math going, why it has a big problem (for some time now, even predating the internet), and why #lean might be part of the solution. hackaday.com/2025/10/08/w...

Where Is Mathematics Going? Large Language Models And Lean Proof Assistant

If you’re a hacker you may well have a passing interest in math, and if you have an interest in math you might like to hear about the direction of mathematical research. In a talk on this top…

hackaday.com

Really excited to see the #lean Mathlib Initiative take off. Here’s their new web page. Mathlib is such a huge, and growing, project; this help from Renaissance Philanthropy is very welcome.

The Mathlib Initiative

The Mathlib Initiative supports the development of mathematical libraries in the Lean theorem prover.

mathlib-initiative.org

TIL In Lean you can output the axioms that a proof depends on using a simple `#print axioms` command.

Even if you didn't have the chance to listen to any of the amazing Igalia Chats - it's time for you to start with a really good chat about #Webassembly, with the one and only @wingolog.org . open.spotify.com/episode/0DmQ...

Wingo on Wasm

open.spotify.com

I was reminded of the Blueprint tool for sketching mathematical profs in Lean. I haven’t used it yet but I’m going to see if this can help me structure my work. Also curious to see how Blueprint applies in other scenarios such as software verification.

GitHub - PatrickMassot/leanblueprint: plasTeX plugin to build formalization blueprints.

plasTeX plugin to build formalization blueprints. Contribute to PatrickMassot/leanblueprint development by creating an account on GitHub.

github.com

Some reflections by Terence Tao on different levels, of formalization and rigor in math. This was offered as a discussion topic in the afternoon session of the Lean workshop at ITP 2026 but we didn’t really get around to it.

There’s more to mathematics than rigour and proofs

The history of every major galactic civilization tends to pass through three distinct and recognizable phases, those of Survival, Inquiry and Sophistication, otherwise known as the How, Why, and Wh…

terrytao.wordpress.com

This is a real eye-opening article where @ghuntley.com builds a compiler for a new language using LLVM and the amazing technique he calls Ralph Wiggum.

Ralph Wiggum as a "software engineer"

😎Here's a cool little field report from a Y Combinator hackathon event where they put Ralph Wiggum to the test. "We Put a Coding Agent in a While Loop and It Shipped 6 Repos Overnight"…

ghuntley.com

I haven’t yet dived in to git worktrees but as I continue to learn and reflect more on AI-assisted working, I realize this is pretty much the feature i need. This article made things click.

Claude Code - AI Pair Programming Assistant | ClaudeCode.io

Transform your development workflow with Claude Code, the most advanced AI coding assistant powered by Claude Opus 4.1 and Claude Sonnet 4.5.

claudecode.io