Featured blogs

Andrews-Curtis formalization card with generators, presentations, exact AC moves, and an equivalence diagram

Andrews-Curtis conjecture formalization

June 2026Harmonic + Lean
Spec versus runtime refinement card with real-valued spec, executable runtime semantics, and an error-bound refinement statement

Spec vs runtime refinement

June 2026Harmonic + TorchLean
Verifiable transformer checkpoint visual with a compact symbolic model and Lean trace

Verifiable transformers in Lean

June 2026Lean + Transformers
Batch-invariant TorchLean inference visual with deterministic serving and verified token alternatives

Batch-invariant inference, formalized in TorchLean

May 2026TorchLean + CUDA
TorchLean visual with tensors, neural network layers, proof checks, and certificates

TorchLean: verified neural networks in Lean

May 2026Lean + ML
Abstract map of research paths, dead ends, and source trails

The dead ends are the map

May 2026AI + Math