M

🚀Metaculus Open-Source Rewrite is Live!

You're now enjoying a rewritten, open-source Metaculus, with a range of improvements and new opportunities for collaboration. Go here to learn more!

Question

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?

25
8
Total Forecasters127
Community Prediction85%

Make a Prediction

community: 85%
median 85.0%mean 74.8%
0%10%20%30%40%50%60%70%80%90%100%
Authors:
Matthew_Barnett
Opened:
Closes:
Scheduled resolution:
AI Demonstrations
Computing and Math
Artificial Intelligence
Elon Musk
Gary Marcus
Lean (proof assistant)
Coq

Comments

? comments