I was listening to the new conversation between DHH and Lex and got this eerie feeling that it all applies to mathematics almost verbatim. Why would you still write mathematics by hand if you can type it up in a semi-formal or formal way while you think? Agentic tools are getting better, so we can focus on ideas and delegate technical lemmas to agents. And with formal proofs, you don't even have to trust them: Lean checks their work. Maths has it easier than code here. Switching languages becomes cheap too, so you can force your agent to translate from one mathematical jargon to another and keep pushing the solution in this new language. Massive collaboration will become a necessity in an age where everything moves so fast. People doing maths by hand and in solitude will be like those indie developers who seek a certain feeling. And once open-weight models catch up and anyone can run them at home, we will have an explosion of abundance. Time to prepare for this: learn agentic coding+Lean and find your collaborators.