“Embracing change and resetting expectations” By Terence Tao

I was just thinking this morning, would it be possible to train an LLM for deep integration with some type of proof system, so that it would write a declarative logical description of a solution would could be automatically verified. Then it could have training on iterating if the verification failed.

Or maybe if the LLM output is pretty fast, it could be packaged with some programming language and evaluation environment so, given a problem in this domain, it could code a solution, check and fix/improve it automatically.