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...