Posts
-
A Vericoding Exercise
LeetCode 1171, with a specification and a proof in Lean.
In September 2026, OpenAI reported that about 10,000 of its AI agents had found a singularity in the three-dimensional Navier–Stokes equations, the subject of one of the Millennium Prize Problems, and that another AI model had formalised the proof in Lean, which checked it (Quanta Magazine). Mathematicians are still examining the result, and who deserves credit is disputed. I wondered: if AI is this capable, why does vibe coding still produce buggy code?
Read more -
Building This Site with Verso and GitHub Pages
This site is written in Lean 4 with Verso, an authoring tool for Lean. Every page is a Lean file, and Lean code on a page is type-checked when the site is built. GitHub builds the site and publishes it with GitHub Pages.
This post documents how I built it, milestone by milestone, as a practical guide for people who do mathematics and want a website like it. For now it has one section, on how GitHub builds and publishes the site; the others follow as the site is finished.
Read more
Categories
None yet.