Will an AI be able to take arbitrary proofs from the mathematical literature and convert them into a symbolic form suitable for verification before 2030?
Question description
On May 31st, 2022, prominent deep learning skeptic and NYU professor emeritus Gary Marcus challenged Elon Musk to a bet on AGI by the end of 2029. His proposed bet consists of 5 AI achievements, of which he predicted no more than 2 would come to pass before 2030. This question is about Marcus' fifth prediction,
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.
Indicators
| Indicator | Value |
|---|---|
| Stars | ★★★☆☆ |
| Platform | Metaculus |
| Number of forecasts | 346 |
Capture
On May 31st, 2022, prominent deep learning skeptic and NYU professor emeritus Gary Marcus challenged Elon Musk to a bet on AGI by the end of 2029. His proposed bet consists of 5 AI achievements, of which he predicted no more than 2 would come to pass...
Embed
<iframe src="https://https://metaforecast.org/questions/embed/metaculus-11198" height="600" width="600" frameborder="0" />