New formalization target

Stream: mathlib4

[Matthew Ballard]

https://arxiv.org/pdf/2508.05105 is pretty far out of reach now but seems great for an aspirational target

[Ruben Van de Velde]

Do you want to write up a high-level checklist of things we'd need in an issue? :)

[Matthew Ballard]

For those not following,

In particular, we prove that a very general cubic fourfold is not rational.

This is a major problem in algebraic geometry. (Lest anyone read into this, I am not worried about correctness of the paper.)

[Matthew Ballard]

Ruben Van de Velde said:

Do you want to write up a high-level checklist of things we'd need in an issue? :)

We can start with two basic blocks

• classical Hodge theory of complex algebraic varieties
• genus zero Gromov Witten invariants

[Michael Rothgang]

Ooh, I would love for Gromov-Witten invariants to be formalised. (Though I care about them from a symplectic, not as much algebraic, perspective.)

[Junyan Xu]

Some talks from 1+ years ago which I didn't watch ... did they just finally write it up or are there new ingredients?

[Junyan Xu]

https://www.quantamagazine.org/string-theory-inspires-a-brilliant-baffling-new-math-proof-20251212/