pfdietz

> Do you want the approval of the mathematical community? A badge of legitimacy?

I don't think that's why the AI companies are doing this.

What's more, it's quite possibly one of the best ways to improve AI, as math provides both a large corpus of training data and an objective way to measure capability. IMO this is likely why the AI companies are working on this, with improvement in math reasoning bleeding over into improvement in general reasoning.

Really, mathematicians should be thrilled about this, as this could be the biggest practical payoff of thousands of years of investment in math, bigger even than all the preceding science and engineering payoffs. We're told one of the benefits of a math education is learning how to think; was it really so unpredictable if that also applied to machines? This sort of payoff would justify wide open checkbooks for more math research, even by humans.

It's like saying writing is the convex hull of 26 letters (plus punctuation).

It's like the spinoff argument for NASA, which is also nonsense.

From Siegel Zero to Siegel Hero.

I know, right?

Communism was a horror for multiple reasons, but two big ones were: the planners didn't have the data or ability to actually plan (the interactions in a market economy did that much better), and not doing the work you were assigned was a crime (that is, slavery).

AGI and AGLabor solves both these problems. If you don't need workers, you don't need to coerce them into work. And planning and massive data collection (and management in general) sounds like something AGI would work very well at. The conceit that the lower classes are disempowered before the capitalists never struck me as well founded.

Freeman Dyson said no scientific (or, I think, technological) project should last more than about five years, because the context under which it was conceived changes too much in that time.

If the mathematicians refuse to use LLMs they will be superseded by a new set of Mathematicians 2.0 willing to do so. Eventually, the flow of money and students for bespoke artisanal manual math will dry up.

Is almost entirely fossil-fuel created doesn't mean it has to be almost entirely fossil-fuel created. You know, just like observing that cars are almost entirely burning fossil fuels doesn't mean cars must burn fossil fuels.

Hydrogen leaked into the troposphere is quickly oxidized back to water. Only very little makes it to the very upper atmosphere where it can escape.

Storage of hydrogen in underground caverns is demonstrated technology.

If working on these is causing improvement in general reasoning (beyond math) then I expect they'll keep doing it.

They can burn non-fossil fuels.

Of course. But the point was that it could also be burned in these turbines, and is also storable underground like methane.

That were not formalized.

OpenAI has kicked things over. Dealing with that is the math community's problem. OpenAI had absolutely no obligation to defer to that community's deficiencies. If this has upset their reward system and historical traditions, tough luck.

It's when theorems are proved by True Scotsmen.

> healthy community

This is code for "they keep paying us".

Moravec's argument strikes again.

I'm told there are another two large tranches of results to be dumped.

Because there's demand for it and he's the best they have to do it?

Cope comes in a wonderful variety of forms.

I think it shows even theorem proving oracles can have a sense of humor.

I know, I know. Don't anthropomorphize AIs. They hate it when you do that.

"Civilization advances by extending the number of important operations which we can perform without thinking of them."

― Alfred North Whitehead, "An Introduction to Mathematics" (1911)

Whatever you do, you should get comfortable working with AI. That will be necessary in just about any job.

That's the issue, but they can't come out and just say it, because that horse left the barn long ago for other professions. It's socially just fine to obsolete entire lines of work, and has been for centuries.

"This ruins my life, so I'm going to be really petty!"

They still have the mic; I've been told there are another two such proof drops coming.

> But if you think they got them illegitimately, then how did they get them?

Obviously they stole them from the Proof Fairy.

It's grapes so sour they could etch metal.

Oh the proof can be understood quite well: it is understood to be wrong.

Finding new simpler proofs happens in traditional manual mathematics too.