Post #1421410

From @xenaproject https://tinyurl.com/JacobianChallenge a challenge to AI companies to autoformalise a nontrivial piece of well-known 19th century mathematics that will need new definitions etc that aren't in mathlib. Can an AI system adequately build the foundational material and 'API' for it that can then be used to give serious results? Unlike eg the sphere-packing formalisation by Math Inc that used a large amount of work by people that set up all the scaffolding in Lean (not to mention the rich Blueprint document that stated all the needed results for at least the 8-dim case)