The hype cycle

When Twitter solves an open problem

Every few weeks, a thread announces that an AI just cracked a famous conjecture. Some of these are real and genuinely important. Many are not — and telling them apart is getting harder, not easier, because the usual proof of authority (a formal checkmark) doesn't actually settle the question.

You know the shape of it by now. A screenshot, a confident thread, sometimes a green checkmark: "[model] just proved [open problem]." It gets thousands of reposts in an afternoon. A few days later, if you're still paying attention, a working mathematician quietly points out that the problem was already solved in 1978, or that step 7 assumes the thing being proved, or that the "formally verified" statement isn't the theorem anyone cared about. By then the claim has done its lap.

The reflexive responses are both wrong. Cheerleading ("math is solved") ignores how often these fall apart. Pure cynicism ("it's all hype") ignores that some are real, and that AI has genuinely started to contribute. The useful skill is triage: knowing the categories, and knowing which piece of evidence actually settles the question.

The real ones

Start with the good news, because it's important and it's easy to miss under the noise. AI has produced legitimately new and checkable mathematics. AlphaProof reached silver-medal-level performance on International Mathematical Olympiad problems under formal conditions — its solutions were Lean proofs, machine-checked, not prose to be taken on faith. Search-based systems have turned up new constructions and improved bounds in combinatorics and algorithm design that hadn't been found by humans. Large models are increasingly useful as collaborators: proposing lemmas, filling routine steps, translating arguments into Lean.

What the credible results tend to share is not a personality or a lab — it's that the claim comes attached to something a third party can independently check: a formal proof, an explicit construction you can verify by hand, a bound you can recompute. The result survives contact with someone who wants to break it. That's the tell.

The failure modes, in rough order of subtlety

When one of these claims doesn't hold up, it usually fails in one of four ways.

1. It was already solved

The most common and least interesting. A problem sits on a list marked "open," a model produces a correct-looking argument, and the announcement declares a breakthrough — but the result has been in the literature for years, and the model has, at best, rediscovered or retrieved it. This isn't fraud; it's the gap between "labeled open on a website" and "actually open," combined with nobody checking the references before hitting post. A whole viral cycle can run its course before someone who knows the field says "this is a known theorem."

2. The prose proof has a gap

A natural-language proof that reads beautifully and is wrong at one load-bearing step — a case not handled, a "clearly" that isn't, a quantifier silently swapped. This is the classic failure of informal mathematics, and models are fluent enough to produce very convincing versions of it. The proof looks complete because every sentence is locally plausible; it takes a domain expert reading adversarially to find the seam.

3. The problem got quietly rewritten

The model (or the person prompting it) restates the problem in a way that's easier — a special case, a weakened bound, an extra hypothesis — and then solves that. Everything downstream is correct. It's just no longer the theorem in the headline. Often nobody did this on purpose; it's what happens when an informal problem gets pinned down without enough care.

4. It's formally verified — and still wrong

This is the new one, and the dangerous one, because it wears the strongest-looking badge in mathematics: a machine-checked proof. The proof passes the Lean kernel. The checkmark is genuine. And the formal statement being proved is not the problem people think it is.

Why the checkmark doesn't settle it

A proof assistant certifies exactly one thing: that the proof establishes the statement as written. It does not — cannot — certify that the statement faithfully encodes the intended problem. A theorem can type-check perfectly while carrying a hypothesis that's secretly contradictory, a definition that's subtly off, or one of Lean's total-function conventions (a divergent sum defined as zero, division by zero as zero) that makes the claim hold for reasons unrelated to the mathematics. None of that is a type error, so the kernel stays silent. (I wrote up the mechanics of this separately.)

This is not a hypothetical worry about the future. In their July 2026 survey of the field, Terence Tao and collaborators point directly at a case where a machine-verified proof of an Erdős problem was circulated whose formal statement did not match the intended problem — the kind of result that looks completely settled and isn't. Their conclusion is blunt:

Research-level formal mathematics requires not just powerful provers but also robust autoformalization with human-in-the-loop verification for high-stakes claims. Machine verification of an incorrect specification provides false confidence that may be worse than no verification at all.

— Tao et al., “From Solvers to Research,” arXiv:2607.07779

Worse than no verification, because the badge travels. A prose proof invites scrutiny — people know to check it. A green "formally verified" stamp shuts scrutiny down: it reads as the final word, so the one question that still matters — is this even the right statement? — never gets asked. And that question is precisely the one no tool can currently answer for you. As the researchers building automated faithfulness checkers put it, as of mid-2026 there is still "no reliable automated method for checking whether a formal statement faithfully captures its informal counterpart" (arXiv:2606.02588). It takes a mathematician who knows the problem well enough to notice what the formalization quietly leaves out.

Why the noise wins the first 48 hours

The dynamics are stacked in favor of the premature claim, and it's worth being honest about why.

• Claiming is instant; checking is slow. A thread takes minutes to write and seconds to read. Verifying a research-level proof — informal or formal — can take a specialist days, and there are only so many specialists.
• A checkmark is legible; a caveat is not. "✓ formally verified in Lean" fits in an image. "The statement omits the finite-dimensionality hypothesis, so it's a weaker theorem" does not, and the people who could say it are outnumbered.
• The incentives point up. Attention, credibility, and in some cases fundraising all reward the announcement. The correction, when it comes, gets a fraction of the reach.

So the timeline reliably resolves a theorem before any mathematician has finished checking it. Sometimes the timeline is right. The problem is that you can't tell which times from inside the first 48 hours.

How to read the next one

A short checklist for the next thread that crosses your feed:

• Is the problem actually open? Check the literature (or wait for someone who has). "Listed as open" is not the same as open.
• Is there something independently checkable — a formal proof, an explicit construction, a computable bound — or just prose and confidence?
• If it's formalized, what exactly is the formal statement? Read the theorem, not the headline. Do the hypotheses and conclusion match the real problem? Are the definitions the standard ones?
• Who checked the statement — someone other than the claimant? The proof is the machine's job. The statement is a human judgment, and it should be made by someone with no stake in the answer.
• Has a little time passed? The single most reliable filter. Real results get more solid under scrutiny; the others quietly don't.

The optimistic reading of all this is that we're living through the early, messy part of something genuinely important: machines are starting to do real mathematics, and formalization is what will let us trust the results at scale. The realistic reading is that "at scale" is doing a lot of work in that sentence. The bottleneck is no longer producing proofs. It's deciding which ones to believe — and a green checkmark, it turns out, is the beginning of that question, not the end.

Disclosure: I'm building Qed, which pairs formalized results with independent mathematicians who audit the statement and definitions — so I have a stake in this. The claims here stand on their sources regardless; corrections welcome.