Batch-Invariant Inference, Formalized in TorchLean

A research note on why temperature-zero LLM serving can still vary under dynamic batching, and how to turn that systems problem into Lean-checked contracts for schedules, attention, serving, and a small CUDA certificate.

Example repo: TorchLean Verified Examples

TorchLean: Verified Neural Networks in Lean

A note on why neural networks need precise meanings: shapes, graph semantics, gradients, certificates, CUDA boundaries, and scientific claims that Lean can check.

Project site: TorchLean

The Dead Ends Are the Map

Why mathematical and scientific AI systems should remember failed approaches, obstacles, partial results, and source trails, not only finished theorems.

Built with Codex over five straight days of collaborative iteration, including multiple agents for code, citations, interface cleanup, and deployment.

Companion project: Failure Atlas