So exciting!
Two big autoformalization projects announced today!
One is @scottnarmstrong's (see below) formalizing his 2025 Inventiones PDE paper. Congrats Scott!!
Another is Buzzard's Jacobian Challenge, which @radokirov, Michael Douglas, Michal Wallace, Jack McCarthy, and others announced on zulip.
So we're in the realm of possibility for moderately difficult automatic formalization! Still no autoformalization of all of FLT, nor Zaremba; but much evidence points in that direction...
The next order challenge is auto-cannonization: we only get the positive feedback loop of people being able to build reliably on top of these projects, if they're fixed up, "cannonized", and PR'ed to Mathlib. The maintainers are capable of that task; we need AI that can help speed up their workflow!
