The Hodge Conjecture Formalization🔗

This guide explains the formalization of the Hodge conjecture in the HodgeConjecture repository, which will eventually appear in Formal Conjectures. The goal is to faithfully encode the statement of the Clay Millennium Prize Problem in Lean.

The conjecture is stated, not proved, though two of its cases are: codimension zero, and every codimension above the dimension. A few classical theorems surrounding the statement are not yet formalized either; Scope and status lists both sides of this.

The Lean code in this guide, including the terms that appear inside sentences, is elaborated when the site is built. Definitions are quoted in full, and the build checks that each quotation is definitionally equal to the declaration in the repository; theorems are listed with #check, and their statements appear on hover, as do the types and docstrings of all names. Names defined in this repository are underlined with dots wherever they appear, in code, in hovers, and in the text; every other name comes from Mathlib or from Lean itself, and the guide does not re-explain those. The site is generated with Verso.