> I think too much credit in the AI math discussion is being given to LLMs rather than to Lean,
For sure math and software people know this, as it's kind of hard to ignore.
Developers who are totally disinterested in nerdy stuff like theorem proving will very quickly hit a wall without letting their models indulge in test suites (regardless of whether they ever even glance at the tests themselves). Physics nerds get it, and if they are on more on the experimental side then they are working to give it some kind of sandbox, all the other science wonks are getting it or will get it as they work with their more computationally inclined colleagues, same for general engineering.
There's a real danger here though in that there is no reason the general public will ever become very much acquainted with the verification/validation steps that all these systems actually need to be reliable. They just hear about this or that nearly impossible thing finally being accomplished as if by magic, and they won't do the work to think about what's in scope, out of scope, or how anything can be checked iteratively.
For sure math and software people know this, as it's kind of hard to ignore. Developers who are totally disinterested in nerdy stuff like theorem proving will very quickly hit a wall without letting their models indulge in test suites (regardless of whether they ever even glance at the tests themselves). Physics nerds get it, and if they are on more on the experimental side then they are working to give it some kind of sandbox, all the other science wonks are getting it or will get it as they work with their more computationally inclined colleagues, same for general engineering.
There's a real danger here though in that there is no reason the general public will ever become very much acquainted with the verification/validation steps that all these systems actually need to be reliable. They just hear about this or that nearly impossible thing finally being accomplished as if by magic, and they won't do the work to think about what's in scope, out of scope, or how anything can be checked iteratively.