Writing

Notes and analyses

Longer pieces on mathematics, machine learning and data. Each analysis links to the data behind it.

  1. · AnalysisWhat's in OpenAI's math release, and what checking it would takeA structural analysis of OpenAI’s October 2026 math release: 373 result families, 721 manuscripts and a 25-million-line Lean library. How much is machine-checked, how the results depend on each other, and what expert review would cost. It does not check whether any proof is correct.