iiinova — where your digital self keeps evolving

Jesse Alama @jessealama.net · 26/05/2026

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

functional-logic.org

Symposium on Functional and Logic Programming 2026 | Functional Logic Programming

18th International Symposium on Functional and Logic Programming

040

Reposted by Jesse Alama

Ilya Sergey @ilyasergey.bsky.social · 19/05/2026

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

On the Unreasonable Effectiveness of Property-Based Testing for Validating Formal Specifications

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

1114

Jesse Alama @jessealama.net · 18/05/2026

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

000

Jesse Alama @jessealama.net · 14/05/2026

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

conf.researchr.org

FM 2026

051

Jesse Alama @jessealama.net · 30/04/2026

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.

github.com

74712

Jesse Alama @jessealama.net · 18/03/2026

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

leodemoura.github.io

Who Watches the Provers? — Leonardo de Moura

Leonardo de Moura — Creator of Lean and Z3

110

Reposted by Jesse Alama

Alex Bradbury @asbradbury.org · 11/02/2026

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.

muxup.com

shandbox

A simple shared sandbox using unshare+nsenter.

1195

Reposted by Jesse Alama

Leaning In! @leaninginconf.bsky.social · 12/02/2026

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

Leaning In! 2026

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

002

Jesse Alama @jessealama.net · 19/01/2026

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/

leanprover-community.github.io

Home

A meeting all about Lean

Jesse Alama @jessealama.net · 10/01/2026

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

youtu.be

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:…

Jesse Alama @jessealama.net · 10/01/2026

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.

041

Jesse Alama @jessealama.net · 30/12/2025

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

sanebox.com

Get rid of email clutter

Try SaneBox today and get 2 weeks for free!

Jesse Alama @jessealama.net · 16/12/2025

Enjoying the video from the December 2025 Mathlib community call.

youtube.com

Mathlib Community Meeting December 12, 2025

Leaning In! @leaninginconf.bsky.social · 08/12/2025

Reposted by Jesse Alama

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

Leaning In! 2026

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

013

Jesse Alama @jessealama.net · 26/11/2025

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

Terence 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 · 14/11/2025

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

youtube.com

ITP 2025 Lean Workshop

Share your videos with friends, family, and the world

040

Reposted by Jesse Alama

Leaning In! @leaninginconf.bsky.social · 26/10/2025

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/

leaning.in

Leaning In! 2026

Leaning In! is a one-day workshop dedicated to the Lean programming language and proof assistant.

143

Jesse Alama @jessealama.net · 09/10/2025

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.

mathlib-initiative.org

The Mathlib Initiative

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

Paulo Matos @ocmatos.com · 03/09/2025

Reposted by Jesse Alama

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

open.spotify.com

Wingo on Wasm

192

Jesse Alama @jessealama.net · 05/10/2025

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

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.

Jesse Alama @jessealama.net · 04/10/2025

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

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…

011

Jesse Alama @jessealama.net · 03/10/2025

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.

claudecode.io

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.

000

Reposted by Jesse Alama

Nordic.js @nordicjs.com · 03/10/2025

No more juggling CommonJS and faux-ESM. @joyeecheung.bsky.social revealed how Node.js is moving to full ESM and why the future looks brighter for developers. #NordicJS #NordicJS2025

0112

Jesse Alama @jessealama.net · 02/10/2025

Just arrived in Reykjavik for the #lean workshop as part of ITP 2025 leanprover-community.github.io/itp-2025-lea... I'll be presenting some of my recent work. Looking forwrard to (re)connecting with some fellow Leaners!

leanprover-community.github.io

Home

Lean Workshop at Interactive Theorem Proving 2025 - 2 October 2025, Reykjavik, Iceland

032

Jesse Alama @jessealama.net · 22/09/2025

TIL pre-commit.com I was just browsing the #lean Mathlib repo toplevel directory and noticed a file with an unusual, but suggestive name. Took a look inside and...love it!

pre-commit.com

pre-commit

A framework for managing and maintaining multi-language pre-commit hooks.

000

Jesse Alama @jessealama.net · 26/08/2025

TFW you start to realize you're not going to win the game of type tetris.

000

Jesse Alama @jessealama.net · 26/08/2025

The Kimina theorem prover at Project Numina is an amazing piece of technology. This kind of targeted, special-purpose LLMs seems to be just what is needed. They don't even need to be large; "small" LLMs might be just fine. demo.projectnumina.ai

demo.projectnumina.ai

Kimina Prover Demo – AI-Powered Proof Validation in Action

Try the live demo of Kimina Prover – a new AI-powered assistant for interactive proof validation. Test it now!

000

Jesse Alama @jessealama.net · 23/08/2025

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.

Jesse Alama @jessealama.net · 22/08/2025

Happy to announce a new polyfill for the in-progress Ecma TC39 amount proposal! The proposal all about mathematical values together (optionally) with a unit and a precision (understood either as significant or fractional digitis)

npmjs.com

proposal-amount

Polyfill for TC39 Amount proposal. Latest version: 20250821.0.0, last published: 7 minutes ago. Start using proposal-amount in your project by running `npm i proposal-amount`. There are no other…

Jesse Alama @jessealama.net · 21/08/2025

Congratulations to the #lean team on the 4.22 release! This is an exciting one for me for two reasons: the new grind tactic and new support for verification of imperative programs using Hoare triples. lean-lang.org/doc/referenc...

lean-lang.org

Lean 4.22.0 (2025-08-14)

For this release, 468 changes landed. In addition to the 185 feature additions and 85 fixes listed below there were 15 refactoring changes, 5 documentation improvements, 4 performance improvements, 0…

000

Jesse Alama @jessealama.net · 21/08/2025

Delighted to see the new Institute for Computer-Aided Reasoning in Mathematics. With many overlapping and fellow-travelling communities in academia, industry, even citizen science, a new institute of this kind is probably what we need right now. www.cmu.edu/news/stories...

cmu.edu

New NSF Institute at CMU Will Help Mathematicians Harness AI and Advance Discoveries

The Institute for Computer-Aided Reasoning in Mathematics (ICARM) — one of just six mathematics institutes across the U.S. to receive NSF support — will help researchers modernize mathematical…

Jesse Alama @jessealama.net · 20/08/2025

The August 2025 Mathlib community call was really great to watch. Thanks for putting it on YouTube. youtu.be/dUWiG12ZQ4g

youtu.be

Mathlib Community Meeting August 8, 2025

110

Jesse Alama @jessealama.net · 01/08/2025

Great overview of the LeanDojo project by Kaiyu Yang from what appears to be a lunchtime CS talk at Stanford. This is all about custom LLM technology for #lean. I haven't kicked the tires on LeanDojo yet but it's on my shortlist of things to explore. youtu.be/qvaR_VXB4fA

youtu.be

LeanDojo: Theorem Proving with Retrieval-Augmented Language Models, Kaiyu Yang et al. - Stanford

main website; LeanDojo: https://leandojo.org/ paper: https://arxiv.org/abs/2306.15626

000

Jesse Alama @jessealama.net · 25/07/2025

I'm learning about zod, a JS package for working with TypeScript data schemes (going well beyond just types). I want to ensure that my compiled TypeScript enforces type checks at runtime in a JS engine. The TS compiler deletes such things, but I want them back! zod.dev

zod.dev

Intro | Zod

Zod 4

Jesse Alama @jessealama.net · 24/07/2025

Hacker News discussion of Markus Himmel's post on the upcoming verification framework for imperative code in #lean news.ycombinator.com/item?id=4449...

news.ycombinator.com

My first verified imperative program | Hacker News

Hopefully the proof would break if one tried to transfer it over?

000

Jesse Alama @jessealama.net · 24/07/2025

Just learned about template literal types in TypeScript. This kinda sorta helps me to turn regular expressions (at least, of a certain restricted kind of regexp) as bona fide types. www.typescriptlang.org/docs/handboo...

typescriptlang.org

Documentation - Template Literal Types

Generating mapping types which change properties via template literal strings.

100

Jesse Alama @jessealama.net · 23/07/2025

TIL PutnamBench leaderboard for benchmarking performance of LLMs on problems from the famous Putnam competition. Several models score really high, whereas e.g. GPT 4o can solve only one problem (in #lean). trishullab.github.io/PutnamBench/...

trishullab.github.io

PutnamBench Leaderboard

000

Jesse Alama @jessealama.net · 22/07/2025

I'm taking a look at the Goedel Prover v2 for doing #lean work. Seems quite impressive; I'm awaiting a system description paper on arXiv. goedel-lm.github.io

Jesse Alama @jessealama.net · 20/07/2025

Fascinating project by Google DeepMind on formalizing mathematical conjectures in #lean. Not necessarily solving them (many remain open), just formalizing them. They're also graded by their difficulty (research open question, high school problem, etc.). google-deepmind.github.io/formal-conje...

github.com

GitHub - google-deepmind/formal-conjectures: A collection of formalized statements of conjectures in Lean.

A collection of formalized statements of conjectures in Lean. - google-deepmind/formal-conjectures