What happened
OpenAI released hundreds of claimed solutions to difficult maths problems this week. According to a report from TechCrunch AI, the release did not meet all the standards proposed by an advisory group of elite mathematicians. The group, AGMAI, noted that OpenAI tested on proprietary models against its advice. A separate paper from UK mathematicians also highlighted discrepancies between a model's natural language proof and its formalised code, questioning the translation process.
How the room's reading it
The mathematical community is framing this as a process problem, not just a performance one. Prominent mathematicians like Terence Tao argue that AI-generated proofs lack the necessary human engagement — the talks, papers, and seminars that build genuine understanding. The concern, echoed by researchers at Cambridge and King's College, is that models can 'mistranslate' their own reasoning from natural language into formal proof languages like Lean. This creates a trust gap. The consensus among these experts is clear: AI-generated proofs can't bypass the standard peer review process. Without a human in the loop to understand and take responsibility for the result, it's just a string of symbols.
Sailfish's take
We see this as a warning for more than just pure maths. It's for anyone shipping products that rely on an LLM for high-stakes logical work — from generating financial models to writing critical infrastructure code. The gap between a model's natural language explanation and its formal output is the crucial failure point. It's tempting to believe the prose and trust the code, but this shows they can diverge. We've learned that you can't have a model mark its own homework. If you're building anything where correctness is non-negotiable, you need an independent, formal verifier. We'd avoid any architecture that lets an LLM be the final arbiter of its own logic.