In 2029, will any AI be able to take an arbitrary proof in the mathematical literature and translate it into a form suitable for symbolic verification? (Gary Marcus benchmark #5)
98
1.2kṀ14k2030
83%
chance
1H
6H
1D
1W
1M
ALL
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.
This question is managed and resolved by Manifold.
Get 
1,000 to start trading!
1,000People are also trading
Related questions
By 2030, AI can autonomously prove mathematical theorems that are publishable in mathematics journals today?
63% chance
Will an AI model write the proof to the Riemann Hypothesis by the end of 2025?
2% chance
Will the majority of mathematicians rely on formal computer proof assistants before the end of 2040?
60% chance
In 2029, will any AI be able to construct "reasonably" bug-free code of >= 10k LOC from a natural language specification? (Gary Marcus benchmark #4)
80% chance
Will natural language based proof assistants be in common use by 2026?
25% chance
Will a blank-slate AI prove the infinitude of primes by 2025-11-03?
25% chance
Will aesop be able to replace >50% of mathlib proofs by 2025-11-26?
41% chance
Will an AI implement a full infinity-topos mathematical framework by end of 2025?
17% chance
Would an AI be capable of constructing a non-brute, ultraweak proof of chess for this board state by 2030?
49% chance
Will we have a formalized proof of the Modularity theorem by 2029-05-01?
65% chance