It's the same reason I was nervous moving our company domain to a .ai TLD; your entire presence, identity and trust is now beholden to the whims and political winds of a Caribbean island smaller than Topeka.
It's not anymore: "in April 2026 the implementation of the agreement was put on an indefinite hold due to opposition from US President Donald Trump." So whatever ICANN was going to do with .io, it's all on hold for now.
Is this not what programming alongside or with an AI agent is these days? Brainstorming, reviewing, debugging. The only difference is there's no second human building a working knowledge of the code being written.
They're not human. When I interact with AI, it's an emotionless chat bot computer program. When I interact with a human, a whole other sections of my brain necessarily light up, because they do have emotions, they do judge me and I care about those opinions about me, and they have long term memory, all thanks to the millions of years of evolution around social interactions with other humans.
To be clear, this is not the kind of thing where a Lean formalization provides any value at all. It's like formalizing the answer to a high school algebra problem. The counterexample is obviously correct.
Indeed. I was mainly responding to the comment about waiting for "independent seasoned mathematicians to verify", whereas in this case it is easy enough to convince oneself of the counterexample's correctness.
