zone411

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.

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?