Week of Jan 8, 2026

Edition 1: 4 items published for Jan 1 to Jan 8, 2026.

Verification Dec 25, 2025

Logical Intelligence shares AI-generated verified λ-calculus to CPS compiler in Lean

Logical Intelligence posted on X an AI-generated, formally verified compiler from λ-calculus to CPS, written in Lean4. The post explains formal verification as code that comes with a mathematical proof, checked by the computer, that it works correctly in all cases, not just the ones tested.

Checked against: @logic_int on X

Lean core Dec 30, 2025

Leo de Moura adds benchmarks showing SymM beating MetaM on intros/apply

A merged Lean 4 pull request by Leo de Moura adds performance comparison tests between the new SymM monad and the standard MetaM for intros/apply operations. Results show a 10-20x speedup, rising from 10.8x at size 1000 to 22.0x at size 6000.

Checked against: lean4#11838 leanprover/lean4

Papers and events Jan 8

Lean Community holds Lean Together 2026 virtually via Zoom, January 19 to 23

Lean Together is an annual meeting for users, developers, and fans of the Lean programming language and theorem prover, covering formalized mathematics, software verification, infrastructure, and outreach. The meeting is open to everyone without cost, and talks will be recorded with speakers' permission and posted to the leanprover community YouTube channel.

Checked against: leanprover-community.github.io

Papers and events Dec 30, 2025

Math, Inc. releases full conversation with Terry Tao on mathematics' future

Math, Inc. posted a full conversation in which Fields medalist Terry Tao sits down with Math Inc's @jessemhan and @jdlichtman to discuss the future of mathematics. Terry Tao says this style of writing proofs shows the inputs and outputs of a proof more clearly and predicts that "the definition of a mathematician will broaden."

Checked against: @mathematics_inc on X