I think there's a pretty good case to be made that LLMs paired with automated theorem provers will become a useful tool to working mathematicians in the next fe

I think there's a pretty good case to be made that LLMs paired with automated theorem provers will become a useful tool to working mathematicians in the next few years. Another thread here links to a lecture from a professor of mathematics who makes this point about halfway in, based solely on Alpha Proofs current abilities (https://www.youtube.com/watch?v=vYCT7cw0ycw https://www.youtube.com/watch?v=vYCT7cw0ycw [54min]). Terence Tao, well-known mathematician at UCLA has been saying similar things for years. He's blogged about LLMs helping to learn new tools (like Lean) and occasionally helping with brainstorming. At this stage, the point they're making isn't 'OMG AGI!!!' but rather something like 'having an enthusiastic, often wrong undergrad assistant who's available 24/7 can be useful, if you use it carefully.'