Pinned post
Introducing hodge.computer: the first multiplayer open research challenge aiming to solve a case of the generalized Hodge conjecture.
Erdős problems can be stated using just simple objects: integers, sets, etc. This makes them amenable to attack using AI.
HC is not so. Its very statement involves deep objects, many of which are not even formalized in Lean (at least until recently): rational Betti cohomology of smooth projective varieties, complex differential forms and the Hodge decomposition, the cycle class map, etc.
My mission is to turn the Hodge conjecture into an Erdős problem. Today, I am beginning with a special case: the GHC for the invariant Hodge substructure H ⊂ H⁴(X, ℚ) in sextic fourfolds X ⊂ ℙ⁵ with an involution. Voisin first isolated this subcase; recent mathematical work on my part has made its prediction computationally effective.
To my knowledge, this is the first computational attack, of any kind, on any case of the generalized Hodge conjecture.
Math is undergoing a revolution (see quoted tweet for more remarks). Calling all enthusiasts and hobbyists! Calling all engineers! And academics, you too :) This is now your time to contribute to the single most fascinating problem in algebraic geometry. Let's go.
Erdős problems can be stated using just simple objects: integers, sets, etc. This makes them amenable to attack using AI.
HC is not so. Its very statement involves deep objects, many of which are not even formalized in Lean (at least until recently): rational Betti cohomology of smooth projective varieties, complex differential forms and the Hodge decomposition, the cycle class map, etc.
My mission is to turn the Hodge conjecture into an Erdős problem. Today, I am beginning with a special case: the GHC for the invariant Hodge substructure H ⊂ H⁴(X, ℚ) in sextic fourfolds X ⊂ ℙ⁵ with an involution. Voisin first isolated this subcase; recent mathematical work on my part has made its prediction computationally effective.
To my knowledge, this is the first computational attack, of any kind, on any case of the generalized Hodge conjecture.
Math is undergoing a revolution (see quoted tweet for more remarks). Calling all enthusiasts and hobbyists! Calling all engineers! And academics, you too :) This is now your time to contribute to the single most fascinating problem in algebraic geometry. Let's go.
Both sides are right. Math must adapt in the AI era. But it also must preserve the standards of stewardship, mentorship and communication that have made mathematics humankind's premier intellectual undertaking.View quoted post on X
Today, we are announcing hodge.computer, the first open autoresearch initiative targeting a special case of the generalized Hodge conjecture.
We believe that mathematics will increasingly be conducted in massively multiplayer, digitally coordinated research programs, with each individual contribution verified by Lean, and progress collected in a central, public leaderboard. At the same time, each such project needs a human mathematician who has pledged to accept responsibility for the cultivation and crystallization of all knowledge that ensues from the project, as well as the identification and crediting of all relevant prior work.
Early predecessors of this model can be found at least as far back as the Polymath projects of Gowers, Tao and their collaborators. More recently, erdosproblems.com has resoundingly demonstrated the viability of this research model.
The problem is that much of math—and Hodge theory perhaps most of all—is hard to formalize, and hard to make incremental progress on.
Thus, in the AI era, the most important task for a mathematician may well shift from
> can you solve this problem?
to
> can you reëxpress this problem in an equivalent form, which in turn is computationally effective?
The latter being done, we can subject the problem at hand to a massive open autoresearch program.
hodge.computer targets the GHC for the involution-invariant Hodge structure H ⊂ H⁴(X, ℚ), where X ⊂ ℙ⁵ is a smooth sextic hypersurface preserved by the involution on ℙ⁵ that changes the signs of three homogeneous coordinates. This important GHC subcase has been isolated and championed by Voisin. Recent work of Diamond has translated the prediction at issue into a computationally explicit form. We launch with 42 verified certificates and 19 open targets.
Now, everyone can contribute to the most fascinating problem in all of algebraic geometry. Visit hodge.computer for background and contribution instructions; feel free also to join our Discord.