I’m working on the front end of a transcription app. It’s a lot of moving buttons and labels around to get them where I want, but there’s no way I would ever be able to do it with a keyboard as fast as using an llm. Are we putting ourselves at a competitive disadvantage to big tech et. al. by being anti ai purists?
To be fair, there might still be human math not as we’ve known it. The first people documented as being replaced were hand-weavers. When the mechanical loom came along, they became the original Luddites. People still do work in textile production, though, even if the job of a mechanical loom operator is totally different.
At the very least, someone has to be able to verify the proof assistants are correct, in order to be able to verify that the proofs they verify are also correct. There’s also the task of training people in mathematical understanding for reasons other than proving theorems, which might include reverse engineering the goofy AI proofs back into something comprehensible.
Some hay has been made out of the fact the AIs which solved the Clay problem were fed a human mathematician’s approach, so I guess there’s prompt engineering, as well.