Week of Feb 5, 2026

Edition 5: 7 items published for Jan 29 to Feb 5, 2026.

Predictable Machines explains why it chose Lean for Predictable Code

In an article, Predictable Machines, Inc. explains why it chose Lean as the foundation for Predictable Code, saying Lean's combination of a programming language and a theorem prover makes it possible to formally verify that AI-generated code stays aligned with specifications as systems evolve.

Checked against: LinkedIn post predictablemachines.com

Verification Jan 29

Gavin Mendel-Gleason used GPT-5.2 and Lean to verify a citation-streaming program

Gavin Mendel-Gleason reports that opencode, GPT-5.2 and lean-lsp-mcp produced a provably correct citation streaming program for a RAG answering system in two hours with no interventions. Gavin Mendel-Gleason argues that LLMs increase software generation faster than software understanding, and calls the approach vericoding (vibe-coding using programme verification).

Checked against: LinkedIn post

Lean core Feb 5

Leo de Moura's Lean change stops simp from simplifying instances by default

The pull request, merged on 2026-02-05, ensures simp does not "simplify" instances by default, since doing so creates non-standard instances that cause problems in Mathlib. The old behavior can be retrieved with simp +instances, and the backward compatibility flag for dsimp also deactivates the change.

Checked against: lean4#12244

Lean core Feb 2

New leancall library lets Python code call Lean functions directly

A post titled "Calling Lean Functions As Python Functions" introduces leancall, a Python library for Lean-Python interop built on LeanInteract, which gives a Lean REPL as a Python library. Examples include a Lean controller balancing a gym cartpole environment and a Lean ray tracer displayed with Python plotting tools.

Checked against: philipzucker.com

Lean core Feb 5

Leo de Moura fixes Lean's type class resolution cache

A merged pull request to leanprover/lean4 makes the type class resolution cache properly cache results for type classes containing output parameters. Output parameter arguments, and universe levels that only appear in output parameter types, are erased from the cache key to avoid cache misses.

Checked against: lean4#12286

Papers and events Jan 29

Stan Fedotov compares two AI-assisted math papers, one checked in Lean

In a LinkedIn post, Stan Fedotov argues the field is "moving towards automated verification in most domains," while noting Lean is "only useful when the standard library supports your field." In one paper, only a somewhat elementary part of the proof was verified in Lean, while the authors proved the deeper parts.

Checked against: LinkedIn post

Papers and events Feb 2

Blog post formally models a Cyberchase episode's dragon game in Lean

A post on shadaj.me, "Formally Verifying PBS Kids with Lean4," uses Lean to model the Cyberchase episode "Problem Solving in Shangri-La," a variant of Nim where players remove 1, 2, or 3 dragons. It proves the Cybersquad's poison-number strategy wins, introducing tactics such as rw, simp, split, and omega along the way.

Checked against: shadaj.me