Week of Jul 9, 2026

Edition 21: 8 items published for Jul 2 to Jul 9, 2026.

Kim Morrison releases first packages of Hex, a computational algebra library

The first Hex packages provide dense matrices, row reduction, Gram-Schmidt, and a verified implementation of the LLL lattice basis reduction algorithm, plus a version that delegates computation to the C library fplll while verifying a certificate. Specifications are written first, then AIs implement code and proofs, and a blog post runs the Coppersmith attack on RSA.

Checked against: kim-em.github.io kim-em/hex

Verification Jul 6

Logos Research proves an F# program and its Python rewrite equivalent

In a Logos Research prototype, a deterministic translator turns both the original and the rewrite into Lean, and a theorem prover proves the two compute the same result on every input. For iCPPI, a portfolio-insurance algorithm, the machine-checked proof ran to some 22,000 characters, with floats modelled as exact real numbers.

Checked against: logosresearch.ai

Lean core May 13

Kim Morrison releases sos, a sum-of-squares tactic for Lean

The sos tactic is a sum-of-squares decision procedure for nonlinear real arithmetic, closely following John Harrison's HOL Light implementation. It calls the CSDP semidefinite programming library and rebuilds a fully certified result in Lean. Kim Morrison calls it a prototype and notes that frontier models have become very good at Lean metaprogramming.

Checked against: kim-em.github.io LinkedIn post

Lean core Jul 1

Joachim Breitner adds automatic try? suggestions to Lean at common proof sites

A merged pull request by Joachim Breitner makes Lean suggest try? output for empty by blocks, unsolved goals, and sorry tactics, gated by three options that default to off. It replaces the tactic.tryOnEmptyBy option from an earlier pull request with a different implementation.

Checked against: lean4#13830

Lean core Jul 6

Leo de Moura adds rw and case tactics to Lean's sym mode

Merged pull requests by Leo de Moura implement the rw tactic and the case tactic (relevant for vcgen) in sym => mode, fix universe constraints and unresolved-instance reporting in SymM, add a hygienic parameter to intro-like functions, and speed up instance assignment when the goal type is ground.

Checked against: lean4#14287 lean4#14278 lean4#14277 lean4#14280 lean4#14279 lean4#14330 lean4#14314

Lean core Jun 30

Wojciech Różowski opens Lean pull requests for stateful linters and unusedVariables hint

A now-closed pull request adds stateful linters: command linters that thread state from one command to the next, so a linter can accumulate information across a file. A merged pull request adds a hint to the unusedVariables linter, suggesting to rename the unreferenced name with an underscore.

Checked against: lean4#14225 lean4#14259

Lean core Jul 3

Mac Malone merges new Lake APIs for dynamic libraries and linking

Lake adds Dynlib.runtimeOnlyDeps, for transitive dependencies that should not be linked but must be preloaded when precompiling, plus an API for retrieving the complete set of core dynamic libraries. A third change lets custom build targets link shared libraries or executables from a module without copying the code in LeanExe.recBuildExe.

Checked against: lean4#14254 lean4#14220 lean4#14219 lean4#14240

Papers and events Jul 1

Dwarkesh Patel relays idea of AIs forking Mathlib into parallel mathematics

In a post on X, Dwarkesh Patel described Grant's speculation that AIs could fork Mathlib, the Lean library of formalized math concepts and proofs, and build a "parallel math civilization." Dwarkesh Patel wrote that Lean guarantees any new conjectures would be logically valid, and that whether they would be interesting is another matter.

Checked against: @dwarkesh_sp on X