AIでConwayの予想を証明した話

I Vibed a Proof of Conway's Conjecture

数学に詳しくない筆者が、ClaudeとChatGPTを駆使して、50年前にJohn Conwayが提起した超現実数の「omnific integers」に関する未解決予想のLean証明を試みた。1ヶ月と大量のトークンを費やし、独立検証はまだだが、Palomar registryの機械的チェックを通過し、専門家からも声明が正しいとの意見を得ている。AIとの対話から生まれた証明の舞台裏を綴る。