@slowcoding@social.vivaldi.net @tao@mathstodon.xyz There is another major difference, which is that automatic theorem provers are exact. They produce a proof certificate and nothing else. In contrast, LLMs work in Natural language, meaning that in addition to a proof certificate, it produces other information that is not verified. A well known source of unverified information is definitions, specific choices of lemmas, and other concepts in the paper: we cannot be sure that the formal definitions and other concepts it produces actually correspond to anything useful or insightful (or even correct). An automatic theorem prover does not give any illusion of having generated 'insightful' definitions or concepts. But in my opinion, there are many other important sources of 'unverified' information contained in natural language. Unlike lean proofs, Natural language proofs guide mathematicians toward thinking in a certain way. We have no way of verifying that guidance. I think despite appearances, there is a substantial amount of 'philosophical' content to natural language proofs than mathematicians like to admit. A natural language proof conveys intuitions, interpretations of results, emphasis based on importance, connections to other fields, directions for future research, the personality and way of thinking of the writer, and more, all in its structure and word choice alone. Typically, they also convey many other things, like past related work, sources, inspirations, acknowledgements, etc, None of this information can be verified in the same way a purely formal proof can, and as a result, an LLM produces a lot more 'noise' than an automatic theorem prover does. It is this 'noise' that is the problem.