Do you require the translation to be true to the original or just any valid proof? Also, does it still count if a human needs to be involved in translating the theorem statement?

True to the original, has to translate the statement as well.

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.

What do you mean by arbitrary proofs? Does this mean all proofs? Only most of them? If something could formalize most routine proofs but fails at complicated ones would that count? What if it fails for only especially complex proofs?

@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."

If I could short one person it would be this guy (if two, Nate Silver…)

Would an average math PhD be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Answer: No)

@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