lg5689

Many of these latest results are very important to theoretical math. Some are also theoretical physics and CS.

Real-world applications are far off, but developing mathematical understanding does tend to leak over into applied physics and CS.

A cynic might say this is all just intellectual games, and though there's a grain of truth, it's too cynical imho. This isn't like 8 queens where there's no hope for applications or generalizations. A lot of this stuff fundamentally affects our understanding of how numbers and systems behave, what are the limits of computation, etc.

Even if someone doesn't care about theoretical results, it's still exciting that AI has become superhuman in a domain as broad as math. That shows there's potential to be superhuman in other domains as well.

It doesn't have to want to kill humans; indifference is sufficient. There's an exact analogy with humans: we have caused extinction and endangerment for many species, not out of malice, but indifference.

There are also many plausible arguments why our ability to train them to be helpful/trusting/aligned can fail. The smarter AIs get, the harder it is to be sure they're trained correctly. There are already reports that AIs are able to detect whether they're in a training environment and change their behavior accordingly.

Even if these are low probability scenarios, the risk-reward is terrible, so I think it's rational to be extremely cautious about AI risk.

AI vs AI chess, played from the standard opening position, is pointless--it's always a draw. Human vs human chess is doing well but AI is banned from it.

The chess-math analogy would imply AI could bring us into a golden era of math competitions for humans. But I don't think it says anything good about prospects for humans in research math.

Tbh this sounds perfectly normal to me. Companies often don't think it's worth defending themselves if theres no actual financial damage, and certainly don't want random employees to be doing it. It can be very frustrating, both for employees who want to defend their reputation and for the public who want the truth, but companies can be extremely conservative about chosing their public relations battles.

IANAL, but yes, I'd assume the license is unenforceable on the AI content.

No, an AI's output can still violate copyright.

LLMs are indeed very special compared to past efforts at automated theorem proving. The search tree for proofs is enormous, even short textbook exercises (i.e. a few dozen lines of Lean) were difficult with GOFAI techniques. Adding a few orders of magnitude to your compute budget barely moves the needle, since the search space increases exponentially for every line of the proof.

Now LLMs have produced multi-thousand line Lean proofs. This is impossible by simply "try everything and see what sticks". LLMs are able to target their efforts to only promising proof strategies. Yes it helps that they work at superhuman speed, so they can try thousands of strategies where a human might try a dozen. But their results cannot be explained only by compute increases; they need genuine mathematical insight.

There was recently an announcement that a group trying to formalize it found a gap exactly where other mathematicians were pointing. So to the extent there was any doubt, it should be gone now--the proof was incorrect.

But I agree LLMs have a lot of potential for checking proofs--both informally (they can read quickly and find gaps) and formally (by attempting to formalize).

I believe that "single source of truth" is a principle that should always be followed. If there's duplicated code where it'd be a bug if they diverge, then you should refactor. It creates a long-distance coupling in your code that may be invisible to future developers until a bug emerges.

But with that in mind, I mostly agree with the article: if it's not a violation of "single source of truth", then abstractions are just a convenience. If it starts being inconvenient, then it's not doing its job and there's no reason to use it. It's a serious code smell if a function needs several flags for custom behavior; that means it's probably the wrong abstraction or violating the single responsibility principle. If there is a legit need for lots of customization, an often-good way to handle is to take a function/functor as an argument for the customization. E.g., rather than `solve(f:double -> double, max_iters = 99, x_abs_tol = 1e-15, x_rel_tol = 1e-15, ...)` you can do `solve(f:double -> double, stopping_criteria: StoppingCriteriaClass)`

One of the authors said in a reddit comment (and I hope I am summarizing accurately) that it's impossible to show a diagram as the smallest instance of the technique gives like 10^1000000 points.

The problem was pretty well known, and had many human attempts. There's some room to argue that the right humans hadn't attempted it, as the solution used advanced methods from another field of math. But imho, whereas many prior AI victories could be explained by not enough human attention, there is no such excuse in this case, and one should acknowledge this is a notable achievement.

This is happening to other forms of competitive programming too. The most recent AIs have problem solving skills rivaling top humans, and so if AI can't be easily banned, the competition is dominated by AI agents.

I thought code golf would take longer for AIs because there's so little training data (it's more niche), but we're seeing AIs starting to match expert humans there too. Sucks because golf has been my favorite type of programming puzzle.

It's crazy how far AIs have come in problem solving ability.

You can't do this for general functions, but it's fine to do in cases where the definition of f naturally embeds into the rationals. For example, a polynomial over Z is also a polynomial over Q or C.

The movement from R to C can be done rigorously. It gets hand-waved away in more application-oriented math courses, but it's done properly in higher level theoretically-focused courses. Lifting from a smaller field (or other algebraic structure) to a larger one is a very powerful idea because it often reveals more structure that is not visible in the smaller field. Some good examples are using complex eigenvalues to understand real matrices, or using complex analysis to evaluate integrals over R.

You can go farther and say that you can't even construct real numbers without strong enough axioms. Theories of first order arithmetic, like Peano arithmetic, can talk about computable reals but not reals in general.