tim.awkronos.com
What if?
A blog that answers absurd questions by doing the math.
Every post bottoms out in a kernel-checked Lean 4 theorem. Zero unchecked axioms. The calculation is the post. One question per theorem, one theorem per question.
- When output outruns labor.American unemployment is rising. Corporate profit margins are at a record. The math that makes both true at once.published april 8, 2026 · 202 theorems · 0 sorry
The shape
Each post starts with a concrete, absurd, calculable hypothetical. The kind a child asks and an adult waves away.
The answer is the calculation. Numbers, not adjectives. The calculation bottoms out in a real Lean 4 theorem from the corpus. The theorem is the receipt.
Every post ends with #print axioms. Clean, or oh no.