"Proof of the Hodge Conjecture"

[kbuzzard]

The repo's formalization of the Hodge conjecture leaves a lot to be desired. There are several issues with it, but the proof in this PR (written by Claude) highlights one of the problems: the field points in Variety.lean lines 57-69 must be in bijection with all scheme morphisms Spec ℂ ⟶ X, but this is huge because the complexes have a ridiculously large number of automorphisms. Furthermore points must inject into some ℙ^N(ℂ), so this can't happen unless X has no complex points, and the Hodge conjecture is clear for such X.

I would recommend that you get an AI tool to review this part of the repo, there is a bunch of data which is not pinned down at all (hodge_subspace, cycle_class etc) and is instead characterised by properties, of which there are far too few for it to be possible to conclude that these objects represent what we want them to represent in the Hodge conjecture. I believe that the Hodge conjecture files in this repo should come with a prominent warning that this is very much a rough sketch of what is going on and is far from a correct formal statement of the conjecture. I would imagine that AI tools could fix these problems now but at the cost of many thousands of lines of extra code, defining the objects correctly rather than asserting their existence and writing down some of their properties (and not enough to characterise them uniquely).

[Robertboy18]

Thanks Kevin. Confirmed independently: your file compiles against main with only the standard axioms, and the argument is right. points ≃ (Spec ℂ ⟶ X) is a hom-set in Scheme, not over Spec ℂ, so every SmoothProjectiveVariety ℂ in the repo has no points.

Fixing the points does not rescue the statement. cycle_class and hodge_subspace are free data, and with cycle_class := 0 the current ClayHodge forces H^0 = 0 for any variety with a point, so the statement would go from vacuous to false. We agree the Hodge files are a sketch, not a formal statement of the conjecture.

Plan: add the warning you suggest to the README, the registry and the docstring, and remove Hodge from the prize-target table; keep your file as a compiled test under a Tests library (scratch/ is not built today) so it stops compiling once the statement is rewritten; treat a faithful statement (analytic topology on X(ℂ), a defined Hodge decomposition and cycle-class map) as a longer-term project rather than patch it. We ran an independent review of the whole repository today and are fixing the other statements as well; details will follow in the README.

OK with us merging the PR in that form, with the file moved and the theorem renamed to say what it shows?

[kbuzzard]

Please feel free to do what you like with this PR! I don't mind at all if it's merged, closed, whatever. It was AI-generated.

The background to it is that I am running a workshop this week on formalising mathematical conjectures, and I am interested in a correct formalization of the Hodge conjecture. I was doing a survey of what was out there in an attempt to understand what needs to be done. My observation is simply that AI is now good enough to give you very coherent comments on whether a formal statement is the Hodge conjecture or not. Correctly stating the Hodge conjecture using only mathlib might still be quite a hard problem.

[Robertboy18]

Thanks Kevin! Your proof is now included in the compiled tests, with your authorship preserved. The warnings point to it, and Hodge remains marked as incomplete. Closing this since your contribution has been incorporated.