Posts tagged #lean4
-
Theorem-Screened Experiments
A three-step decision rule for running fewer, better experiments: check your theorem library before you touch a GPU. Calibration checks, falsifier traps, and parameter compression from the physicist mode of ML research.
-
Naming What Fails: The Obstacle Taxonomy
25+ preregistered kills over six weeks of compression research. The tempting story is "compression is hard." The physicist story is better: 25 kills, ~10 structural failure patterns, one Lean theorem per class.
-
Two Research Modes, and Why the Second One Needs Lean 4
AI makes hypothesis generation cheap. Evaluation stays expensive. Lean 4 proofs are the filter that changes the economics: a proved theorem screens an entire family of candidates before GPU time is allocated.
-
Zero-Sorry Discipline: What a Lean 4 Appendix Actually Costs
Two theorems in this paper — MoEGauge and JensenFloor — had to reach zero sorries before the paper shipped. What that process looks like, why sorry is dangerous, and what JensenFloor actually says.
-
A Survey as a Living Document
What it means to maintain a formal proof corpus that stays in sync with its own coverage badge, and what happened when RWKV was added as a new architectural family without invalidating existing theorems.
-
Lean 4 as a Soundness Oracle for Security Properties
Type stubs catch misuse at type-check time. But can we prove they are sound — that a well-typed program cannot trigger the dangerous code path? Enter Lean 4.
-
The Microsite as Interactive Publication
Building a GitHub Pages research microsite with d3 widgets, a Lean 4 theorem status page, and a reproducibility shim. One gotcha with Jekyll and markdown-inside-divs. One real answer to whether live widgets are worth the effort.