AI, Math, the document-drop. Non-Tech Thoughts

So what to make of OpenAI and the future of Math? Here are some points I've either:thought of myself or heard from a human or read from an AI.Throughout this post I use the term AI to mean an AI system that produces mathematical results. I decline to say OpenAI or Anthropic as generic terms since about 20 years ago I used Intrade as a generic term for Betting Markets---then Intrade went out of business. I wish I had bet on that happening. Oh well.1) Some of the proofs were Lean-formalized and some were not. If a proof is Lean-verified do we know the proof is valid? The issue is not bugs in Lean. The issue is that coding a theorem/proof into Lean may be done incorrectly. So Lean might be verifying a proof of a theorem different than what was intended.Peter Woit, is a string-theory skeptic and a Lean-skeptic. See hereAlexander Bastounis, Fabian Circelli, Anders Hansen argue that the Lean formalization does not correspond to the natural-language proof. See here My impression/predictions…