zone411

These resolve 6 entries in my top 500 open problems list (LLM ranked, https://www.proofatlas.ai/open-problems/) and there is partial progress on #3 overall (Yang–Mills Existence and Mass Gap):

Kakeya conjecture — #38

Fourier restriction conjecture — #46

Local smoothing for wave equations — #187

Bochner–Riesz conjecture — #190

Exponential Time Hypothesis — #43

Strong Exponential Time Hypothesis — #63

Thrusters pointed straight back will be illegal on public roads and racetracks, as they'd throw debris at people and cars behind them. However, pointing them upward and forward could give them a chance of being legal and functional, especially for braking.

Gemini 4 Argon: https://x.com/LechMazur/status/2111255403216384046 GPT-6 Pro: https://x.com/LechMazur/status/2111255536666644932 Opus 5.5: https://x.com/LechMazur/status/2111258566539493402

Off-topic, but collatz(x) == 1 for all positive 64-bit integers (actually, this has been verified up to 2^71: https://link.springer.com/article/10.1007/s11227-025-07337-0). I recently made this tool if anyone wants to try it with 1,000-digit integers or ranges: https://www.proofatlas.ai/explore/collatz/.

By category in the top 500:

  +----------------------------------------------------+------+---------+-----------------+
  | Category                                           | Full | Partial | Matched / total |
  +----------------------------------------------------+------+---------+-----------------+
  | Geometry and topology                              |   25 |       7 |         32 / 74 |
  | Algebra, representation and category theory        |   17 |       2 |         19 / 53 |
  | Analysis and PDE                                   |   11 |       6 |         17 / 40 |
  | Number theory and arithmetic geometry              |    4 |      13 |        17 / 117 |
  | Probability, ergodic theory and dynamics           |   11 |       5 |         16 / 37 |
  | Combinatorics and discrete geometry                |    7 |       2 |          9 / 34 |
  | Theoretical computer science                       |    4 |       4 |          8 / 57 |
  | Mathematical physics                               |    5 |       1 |          6 / 19 |
  | Applied and computational mathematics              |    2 |       2 |           4 / 8 |
  | Quantum information and computation                |    2 |       1 |          3 / 17 |
  | Cryptography, coding, information and optimization |    1 |       1 |          2 / 26 |
  | Logic, foundations and set theory                  |    1 |       1 |          2 / 18 |
  +----------------------------------------------------+------+---------+-----------------+
  | Total                                              |   90 |      45 | 135 / 500 (27%) |
  +----------------------------------------------------+------+---------+-----------------+

Except that Claude wasn't used.

There was A LOT of drama about this release.

A quick check shows that this list claims to fully solve 90 of the top 500 open problems in math (https://proofatlas.ai/open-problems/).

The highest ranked would be:

| 22 | Hilbert’s tenth problem over ℚ |

| 29 | Unique Games |

| 31 | Anderson-model extended states |

| 37 | Spacetime Penrose inequality |

| 48 | Nonexistence of Landau–Siegel zeros |

| 52 | Baum–Connes |

| 78 | Abundance |

| 80 | Hadwiger |

| 87 | Bose–Einstein condensation |

| 92 | Two-dimensional entanglement area law |

Yes, you can see the latest resolved ones here: https://www.proofatlas.ai/open-problems/#resolved-problems. I'm currently doing updates in batches, but I'm about to switch to daily updates.

Right now, I'm having LLMs audit the actual math in claimed arXiv solutions because despite its policy changes, arXiv is still a dumping ground. The audits have already found six faulty proofs that caused status issues for problems that should still clearly be fully open.

I maintain an LLM-ranked list of the 500 most important open problems in math at https://www.proofatlas.ai/open-problems/. This problem was ranked #159, and it also resolved #244, "All-Pairs Shortest Paths in Truly Subcubic Time." It is formalized in Lean.

But what's crazy is that within the last day or so, we've also gotten LLM-assisted solutions to #95, the Kannan–Lovász–Simonovits (KLS) conjecture, by three different authors in parallel (all extending Song–Zhang's key criterion introduced on Oct. 1), #278, the Mumford–Shah conjecture, and #227, Zauner's conjecture on SIC-POVM existence in every dimension, which also represents a major claimed advance on Hilbert's twelfth problem (#36) for real quadratic fields.

This is likely because OpenAI's solutions to 100 open conjectures are expected to drop any day, so everyone is in a hurry not to get scooped.

The article presented facts and data. If that's a problem for you, that sounds more faith-based than whatever Anthropic is doing.

Completely misleading.

This is all you need to read and understand for Anthropic's FLT formalization:

  import Mathlib
  import Theorems.Thm_fermat_last_theorem

  /-- Solution side: the same statement, binder for binder, proved by this tree's `fermat_last_theorem`. -/
  theorem FLT_for_comparator (n : ℕ) (hn : 3 ≤ n) (a b c : ℕ) (ha : 0 < a) (hb : 0 < b) (hc : 0 < c) :
    a ^ n + b ^ n ≠ c ^ n :=
  fermat_last_theorem n hn a b c ha hb hc

  /-- Mathlib's named proposition, by the one-line bridge from the elementary statement
  (the bridge is restated inline so that this file depends only on `Theorems.Thm_fermat_last_theorem`). -/
  theorem FLT_mathlib_for_comparator : FermatLastTheorem :=
  fun n hn a b c ha hb hc => fermat_last_theorem n hn a b c (Nat.pos_of_ne_zero ha) (Nat.pos_of_ne_zero hb) (Nat.pos_of_ne_zero hc)

The actual proof is 13 million lines of Lean.

I don't:

"Problems solved before a model's training cutoff can be filtered out, and all models compared on the remaining problems" means that the problems an older model actually solved are the ones that get filtered out, while the remaining problems are the ones it already tried and failed on. So older models end up with 0s on the filtered set and you can't really use this to compare new models to older ones.

Also, since these are known public problems, you can't stop people from spending far more than your arbitrary time and $ limits on them. So the number of clean problems will go down over time.

A complete mischaracterization, as usual for HN lately when discussing AI or LessWrong. Obviously, even average levels of persuasion are enough to convince some people. And nobody is air-gapping AI.

So why don't companies in other industries rush to prove their products are dangerous weapons? Maybe because it would be a really dumb PR stunt?

And how do people saying this know the capabilities of yet unreleased models?

How is it in their interest? Scaring customers, worrying employees, and inviting regulators to act is in their interest?

It's not good marketing for them. This is a talking point with zero evidence that people repeat mindlessly. Scaring customers, worrying employees, and inviting regulators to act would be the worst marketing idea ever devised.

Yes, definitely not a new idea. I had a multi-turn composite model in 2024 that was outperforming the top models across benchmarks: https://x.com/LechMazur/status/1828804485033992514.

That's not proof. Emergent intelligence is not consciousness.

I’ve tested this model on four of my benchmarks:

https://github.com/lechmazur/buyout_game 10th out 36.

https://github.com/lechmazur/pact/ 14th out 25.

https://github.com/lechmazur/nyt-connections/ 60th out 81.

https://github.com/lechmazur/debate 16th out of 29.

100%. It's sad to see that this attitude has spread to HN

I actually tried using GPT-5.5 Pro on this problem recently. It thought it was making progress on one path, but it made so many mistakes that it didn't feel worth it pushing further. It'll be interesting to check whether it's the same route. I got partial results (proved in Lean) that improve on the best-known results for four Erdős problems with GPT-5.5 Pro

I built this benchmark this month: https://github.com/lechmazur/sycophancy. There are large differences between LLMs. There are large differences between LLMs. For example, Mistral Large 3 and GPT-4.1 will initially agree with the narrator, while Gemini will disagree. I swap sides, so this is not about possible viewpoint bias in the LLMs. But another benchmark shows that Gemini will then change its view very easily in a multi-turn conversation while Kimi K2.5 or Grok won't: https://github.com/lechmazur/persuasion.

I built two related benchmarks this month: https://github.com/lechmazur/sycophancy and https://github.com/lechmazur/persuasion. There are large differences between LLMs. For example, good luck getting Grok to change its view, while Gemini 3.1 Pro will usually disagree with the narrator at first but then change its position very easily when pushed.

Hmm, maybe in the next edition, Opus gets expensive. I should probably run GPT-5.4 xhigh too if I do that for fairness...