Week of Jul 23, 2026

Edition 23: 9 items published for Jul 16 to Jul 23, 2026.

Tau Ceti, a "Mathlib for AIs" from the Lean FRO, is released

Alex Kontorovich announced the release of Tau Ceti, which Alex Kontorovich describes as the brainchild of Kim Morrison at the Lean FRO and a "Mathlib for AIs". The stated aim is to move fast and get a whole lot more formalized math than can be done at the scale of human review.

Checked against: @AlexKontorovich on X

Lean core Jul 15

Lean v4.33.0 release candidate 1 is out

The Lean developers published release candidate 1 for Lean v4.33.0, which centers on a more responsive editor, automatic try? proof suggestions, improved lia and grind tactics, a Float type that is no longer opaque, and kernel soundness fixes. It also enables backward.isDefEq.respectTransparency.types by default, the change most likely to need attention when porting.

Checked against: v4.33.0 release notes lean4 v4.33.0-rc1

Lean core Jul 22

Patrick Hulin reports a kernel check gap allowing a proof of False

In leanprover/lean4#14484, Patrick Hulin reports that the kernel does not reject free variables in opaque declaration bodies, letting an adversarial metaprogram prove False with no axiom dependencies. The report, largely generated with AI, suggests applying the closure check used for definitions and theorems, and the issue is now closed.

Checked against: lean4#14484

Lean core Jul 11

Sebastian Ullrich proposes prefix trees in oleans to speed up Lean imports

An open pull request by Sebastian Ullrich replaces hash maps built at import time with per-module prefix trees precomputed when oleans are written, cutting import Lean wall clock by 28% and mathlib's import phase by 21%, for about 6% larger stdlib oleans. A separate pull request by Sebastian Ullrich upgrading Lean to mimalloc 3 was merged.

Checked against: lean4#14362 lean4#7786

Lean core Jul 14

Sebastian Graf adds frame inference and contract syntax to Lean's vcgen

Merged pull requests extend vcgen, described as a verification condition generator over the Std.Internal.Do metatheory, with automatic frame inference and with loop invariants and def contracts (require and ensures clauses) that vcgen discharges automatically. A showcase repository collects imperative Lean programs verified with one 'vcgen ... with finish'.

Checked against: lean4#14389 lean4#14195 sgraf812/vcgen-showcase leanprover/lean4

Lean core Jul 18

Leo de Moura adds grind hom attributes to replace ToInt typeclasses

Leo de Moura merged pull requests adding a [grind homo] attribute, since renamed [grind hom] and [grind hom_pred], and migrated the standard library to them. The new approach will replace the ToInt typeclasses used in grind. Andres Erbsen has already successfully tried and prototyped it.

Checked against: lean4#14446 lean4#14468

Lean core Jul 17

Leo de Moura merges grind discharger support for Sym.simp and three fixes

Leo de Moura merged pull requests letting grind discharge hypotheses in conditional Sym.simp theorems, preventing grind timeouts on definitional equality checks for match-expression conditions, fixing a canonicalizer bug that made grind miss valid contradictions, and fixing grind dropping E-matching theorems from custom grind attributes.

Checked against: lean4#14425 lean4#14444 lean4#14439 lean4#14426

Lean core Jul 16

lean4web enables deflate compression for large websocket messages

A merged pull request by Jason (@jcreedcmu) enables per-message deflate compression for messages larger than 16MB in the websocket server behind lean4web, aiming to improve responsiveness of live.lean-lang.org. Full completions with Mathlib imported produce 20-40MB jsonrpc responses, which compress by a factor of 8-9x.

Checked against: lean4web#133

Papers and events Jul 16

Son Ho speaks at the 3rd Lean in Munich meetup

Son Ho's talk at the meetup, hosted by UTUM Venture Labs, previewed Formal Spec driven Development: AI implements a spec and generates its constraints using autoformalisation, while humans write the spec and check that the constraints cover it. Lean FRO's Munich-based team, including Head of Engineering Sebastian Ullrich, attended.

Checked against: LinkedIn post