flâneur

The Jacobian Challenge Retro

rkirov.github.io · 2,030 words · saved by 1 readers

AI Disclosure: Draft was written fully by a human. Heavy use of AI for editing. In April 2026, Kevin Buzzard posed the following challenge for Lean AI autoformalization: can an AI system both define the Jacobian variety in Lean and prove basic properties about it? (zulip thread, github gist). The motivation behind this challenge, as far as I can tell, was to point the autoformalization community at a specific problem chosen by Kevin, instead of letting people choose freely from the vast number of known missing formalizations. Because few are incentivized to publish their failed attempts, there were doubts about whether recent successes reflected general capability or just clever problem selection.

AI Disclosure: Draft was written fully by a human. Heavy use of AI for editing. In April 2026, Kevin Buzzard posed the following challenge for Lean AI autoformalization: can an AI system both define the Jacobian variety in Lean and prove basic properties about it? (zulip thread, github gist). The motivation behind this challenge, as far as I can tell, was to point the autoformalization community at a specific problem chosen by Kevin, instead of letting people choose freely from the vast number of known missing formalizations. Because few are incentivized to publish their failed attempts,…

saved by

related reading