@davidaugust Well, there have actually been successes by connecting LLMs to proof assistant and computer algebra programs. As this post rightly puts, the LLM is not capable in itself to perform computations reliably, but it can write commands sent to the computer algebra programs, or proof candidates sent to the proof assistant; which can answer that the proof is incorrect, and the process goes on until a correct proof is produced. See also uses by pro mathematicians: https://bsky.app/profile/wildverzweigt.bsky.social/post/3miua4ulxhk2f Also see Terence Tao