Jesse Alama

Jesse Alama

@jessealama.net

Math and programming. Lean, JS, Racket. American. Igalian.

183 followers60 following174 posts

Jesse Alama reposted

sawyer
@sawyer-p.me

I love formal verification + fuzzing techniques but am wary that we're quickly speedrunning towards a future where people are generating enormous incomprehensible correctness proofs about their programs, but are none-the-wiser on what properties have actually been proven.

Joe Fabisevich@mergesort.me

I don't say this lightly: this approach is clearly the future of software development. I have a blog post brewing that touches on the subject, but fuzz testing and formal verification at scale will make all software an order of magnitude better, safer, and more reliable.

anthropic.comLLMs are making formal software verification feasible at a much larger scaleClaude formally proved security properties in the compiled code of 123 open-source libraries. Along the way, it found bugs that had eluded detection for years.
Jesse Alama
@jessealama.net

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`,

View full thread
Jesse Alama
@jessealama.net

I was inspired to make pabst after organizing a session at @igalia's Web Engines Hackfest, dedicated to the general topic of getting better at testing our JavaScript. github.com/Igalia/weben...

github.comBeyond testing and type checking JavaScript: Can we be bothered? · Issue #77 · Igalia/webengineshackfestLogistics Date & Time: Wednesday 17th June at 12:00 CEST (local time) URL: https://meet.jit.si/WEH2026-js-testing Notes: https://github.com/Igalia/webengineshackfest/wiki/2026-Beyond-testing-and-ty...
Jesse Alama
@jessealama.net

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`,

Jesse Alama
@jessealama.net

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

youtube.comGolfing and stylistically aligning a proof using Claude CodeIn 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…

Jesse Alama reposted

Ilya Sergey
@ilyasergey.bsky.social

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.

proofsandintuitions.netOn the Unreasonable Effectiveness of Property-Based Testing for Validating Formal SpecificationsIn this post, we show that property-based testing (PBT) is surprisingly effective for validating LLM-synthesised specifications of Lean programs: it is a cheap alternative to symbolic proofs, which he...
View full thread
Jesse Alama
@jessealama.net

Currently, we support JSDoc-style assertions such as `@total`, `@pure` to express the totality (program terminates on all arguments without exceptions) and purity (no mutation) of JS functions. But that's just the tip of the iceberg. Stay tuned for more assertions and program properties.

Jesse Alama
@jessealama.net

A longer-term aim is to complete the deep embedding of TypeScript into Lean (which will exist alongside the current shallow embedding), which will enable all sorts of features such as LSP interaction. One can even imagine an MCP server that can help harden TS programs with AI assistance.

Jesse Alama
@jessealama.net

Thales development proceeds along two arcs: (1) growing the subset of TS that we support, and (2) surfacing Lean and its program verification toolkit in TS programs, which is done via JSDoc-style comments.

Jesse Alama
@jessealama.net

As Lean becomes a load-bearing system, there's increasing pressure to makie sure that the kernel is safe.I love the idea of having an extensibile kernel and applaud the new kernel arena effort to increase transparency around that.

Jesse Alama
@jessealama.net

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.

Jesse Alama
@jessealama.net

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

mathstodon.xyzTerence Tao (@tao@mathstodon.xyz)Over at the Erdos problem website, AI assistance is now becoming routine. Here is what happened recently regarding Erdos problem #367 https://www.erdosproblems.com/367 : 1. On Nov 20, Wouter van…
Jesse Alama
@jessealama.net

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

hackaday.comWhere Is Mathematics Going? Large Language Models And Lean Proof AssistantIf 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…
Jesse Alama
@jessealama.net

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.comGitHub - 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.
Jesse Alama
@jessealama.net

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.

terrytao.wordpress.comThere’s more to mathematics than rigour and proofsThe 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…
Jesse Alama
@jessealama.net

Just had my first success using the new grind tactic in a #lean proof. I didn't know it was even going to work; I was stuck and reached for it only as a hail-mary desparation move. It worked! Mind blown.