University of Toronto mathematician Daniel Litt says AI's math capabilities are bottlenecked on verification: "My sense is the reason [AI models are] not producing long, complicated proofs is that they cannot. The ability to check correctness is not yet there." "If you ask the models to produce a short proof, you can then ask, 'Is that correct?' And they will often say no... The problem with producing a very long thing is they might not know they're wrong." "What I wonder is, presumably internally, OpenAI and Anthropic have probably solved a lot more problems than they've released. And I imagine quite a few of them, they're just not sure if they're true." "Someone recently posted a claimed proof of resolution of singularities in positive characteristic, which was 800 AI-generated pages. I haven't read it, I haven't found an error, but there's no way it's correct. This would be a major result... Definitely no human has read it. Definitely the models are not able to check this kind of thing yet." @littmath @lishali88(a16z)