AI solves an 18-year-old open problem, and Lean verification itself comes under scrutiny

According to an article published on DEV Community on November 7, an AI research system this week proved an open problem in quantum complexity theory that had been open for 18 years. More notably, the proof came with a complete Lean formalization that was accepted by the Lean kernel. The article observes that when an AI-generated proof passes a formal verifier, the usual first reaction is to ask whether the mathematics is correct, but that is no longer the only question worth asking. A kernel-verified proof is only as trustworthy as the system, definitions, libraries and toolchain it relies on, the author argues, so the verification step itself also needs to be audited.

Beyond that, the available material does not name the specific problem that was proved, identify the AI system involved, or describe how the formalization was received by the Lean kernel. No other reporting has yet confirmed the result, so the situation currently stands at the point of a single published claim: an AI-assisted proof with a complete Lean formalization, with the trustworthiness of the verification layer itself now under scrutiny.