Producing machine verifiable formal proofs is an activity somewhat amenable to self play. To the extent that some parts of physics are reducible to ZFC oracle queries, maybe AI can solve those.
To do something other than produce ZFC proofs, the AI must be learning what real in practice maths looks like. To do this, it needs large amounts of human generated mathematical content. It is plausible that the translation from formal maths to human maths is fairly simple, and that there is enough maths papers available for the AI to roughly learn it.
The Putnam archive consists of 12 questions X 20 years=240 questions, spread over many fields of maths. This is not big data. You can’t train a neural net to do much with just 240 examples. If aliens gave us a billion similar questions (with answers), I don’t doubt we could make an AI that scores 100% on putnam. Still it is plausible that enough maths could be scraped together to roughly learn the relation from ZFC to human maths. And such an AI could be fine tuned on some dataset similar to Putnam, and then do well in putnam. (Especially if the examiner is forgiving of strange formulaic phrasings)
The Putnam problems are a unwooly. I suspect such an AI couldn’t take in the web page you linked, and produce a publishable paper solving the yang mills mass gap. Given a physicist who understood the question, and was also prepared to dive into ZFC (or lean or some other formal system) formulae, then I suspect such an AI could be useful. If the physicist doesn’t look at the ZFC, but is doing a fair bit of hand holding, they probably succeed. I am assuming the AI is just magic at ZFC, that’s self play. The thing I think is hard to learn is the link from the woolly gesturing to the ZFC. So with a physicist there to be more unambiguous about the question, and to cherrypick and paste together the answers, and generally polish a mishmash of theorems into a more flowing narrative, that would work. I’m not sure how much hand holding would be needed. I’m not sure you get your Putnam bot to work in the first place.
Producing machine verifiable formal proofs is an activity somewhat amenable to self play. To the extent that some parts of physics are reducible to ZFC oracle queries, maybe AI can solve those.
To do something other than produce ZFC proofs, the AI must be learning what real in practice maths looks like. To do this, it needs large amounts of human generated mathematical content. It is plausible that the translation from formal maths to human maths is fairly simple, and that there is enough maths papers available for the AI to roughly learn it.
The Putnam archive consists of 12 questions X 20 years=240 questions, spread over many fields of maths. This is not big data. You can’t train a neural net to do much with just 240 examples. If aliens gave us a billion similar questions (with answers), I don’t doubt we could make an AI that scores 100% on putnam. Still it is plausible that enough maths could be scraped together to roughly learn the relation from ZFC to human maths. And such an AI could be fine tuned on some dataset similar to Putnam, and then do well in putnam. (Especially if the examiner is forgiving of strange formulaic phrasings)
The Putnam problems are a unwooly. I suspect such an AI couldn’t take in the web page you linked, and produce a publishable paper solving the yang mills mass gap. Given a physicist who understood the question, and was also prepared to dive into ZFC (or lean or some other formal system) formulae, then I suspect such an AI could be useful. If the physicist doesn’t look at the ZFC, but is doing a fair bit of hand holding, they probably succeed. I am assuming the AI is just magic at ZFC, that’s self play. The thing I think is hard to learn is the link from the woolly gesturing to the ZFC. So with a physicist there to be more unambiguous about the question, and to cherrypick and paste together the answers, and generally polish a mishmash of theorems into a more flowing narrative, that would work. I’m not sure how much hand holding would be needed. I’m not sure you get your Putnam bot to work in the first place.