Week of Feb 26, 2026

Edition 8: 3 items published for Feb 19 to Feb 26, 2026.

Rutgers group formalizes the upcoming IEEE-P3109 floating-point standard in Lean

Santosh Nagarakatte's group built FLoPS, which formalizes the upcoming IEEE-P3109 standard for low-precision floating-point arithmetic in Lean. The work found errors in the draft standard, which were reported to the working group and fixed, and established properties of algorithms such as Fast2Sum in the context of P3109.

Checked against: mathstodon.xyz

Lean core Feb 16

Leo de Moura merges isDefEq transparency change into Lean core

The pull request stops isDefEq from raising transparency to .default when checking implicit arguments, which was creating scalability problems in Mathlib. The PR calls it a very disruptive change, reversible with set_option backward.isDefEq.respectTransparency false. Separately, Lean published the second release candidate for v4.29.0.

Checked against: lean4#12179 lean4 v4.29.0-rc2

Papers and events Feb 25

Emilio Jesús Gallego Arias built a Lean DSL debugger with GPT-Codex 5.3

In the blog post "Vibe-coding a debugger for a DSL", Joachim Breitner describes a small language embedded in Lean with a visual debugger in Lean's Info View and VSCode debugger support via the DAP protocol, built in one day of coding with GPT-Codex 5.3.

Checked against: joachim-breitner.de