LeanがLLMと融合したら9割の数学者はヤバいと、お前ら思わないのか?
小山信也はAIじゃ本当に創造的な数学はできないと言ってるが時間の問題かもしれん