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

@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