Huh? Nobody's talking about that because it's old news. We already talked about it the first few times that AI made notable progress on a difficult math problem. Now, most people who care about the intersection of AI and math just assume that Lean was involved.