The fifth question from this post: https://garymarcus.substack.com/p/dear-elon-musk-here-are-five-things
The full text is: "In 2029, AI will not be able to take arbitrary proofs from the mathematical literature written in natural language and convert them into a symbolic form suitable for symbolic verification."
Judgment will be by me, not Gary Marcus.
Ambiguous whether this means start or end of 2029, so I have set it for the end.
I will accept if there is an AI that can do this for >=75% of the proofs published on the arxiv math categories in 2029.
Related questions
Closely related: https://manifold.markets/market/will-an-ai-be-able-to-convert-recen
@Aleph I also still endorse my comment there about there being notable paths to improving Lean (or Coq, etc.) code generation.
@TomBouley "I will accept if there is an AI that can do this for >=75% of the proofs published on the arxiv math categories in 2029."
@SG No, definitely not. I certainly couldn't. But Marcus isn't claiming to be capturing human capabilities exactly so I think this isn't "unfair", and it's an interesting question anyway