traes

"I made this proof myself, but the designer is someone else" is an extremely unconvincing claim to ownership.

If there was any real money in it Stockfish would not be the best chess engine.

That's clearly just for the tokens, this doesn't really answer OP's question.

Given that OpenAI pays their employees with stock surely a breathtaking number, but not a very meaningful number now that the infrastructure is in place and the models are trained. AI could never get better and it would still be incredibly disruptive.

A fundamental difference being that no one was actually paid to find good moves in chess and go like they are to solve math problems and write code. You're comparing the digital camera and the automobile.

It's a very important clarification if it took $2000/problem on 20 problem attempts or on 1,000 problem attempts for each successful one. That may be the deciding factor on whether or not it's economically viable to replace a mathematician with a ChatGPT subscription.

Not much point to pure math being kept secret, in all honesty. There isn't really industrial value, its only purpose (to them) is showing off their model's capabilities. More realistically they'll just stop paying for it.

Edit: Oh, are you suggesting they just use it to privately improve their models? I imagine a few more correct proofs would have a very marginal benefit, if any. Also, they'll probably just get extracted, meaning it still gets out but OpenAI doesn't get to fancily announce it themselves.

That seems to have been more of a sensationalized joke. Even your link has a disclaimer in it now. Read this chat from the researcher who did this:

https://leanprover.zulipchat.com/#narrow/channel/270676-lean...

> Also, have there been examples of researchers not affiliated with OpenAI (or another LLM creator), who have done something similar?

A couple small ones that I've seen (example here [0]), but not anything of the magnitude that OpenAI and Anthropic have put out. Likely just related to token limits.

> Another question I have is whether or not OpenAI 'simply' hired capable combinatorics researchers to work on problems, and they have, and the use of the model is incidental / secondary to their work.

I think their output has reached a level that precludes this possibility, but I of course don't have any hard proof.

[0]: https://www.reddit.com/r/math/comments/1uxj3cy/after_openais...

This isn't really a productive way to think about these things, IMO. It's quite possible it would take hundreds of years for any specific group of PhDs to solve them. Or one individual PhD could have the correct flash of insight and solve it in a month. There's absolutely no way to predict this, besides trying to gauge the apparent simplicity of the proof or counterexample (which is likely to be misleading). Until someone actually runs an experiment like this it's not a viable metric.

Every time someone makes a comparison to chess I die inside. Chess is a spectator sport primarily funded by a few eccentric billionaires. Players artificially constrain themselves in timed environments knowing that they will never be able to produce better moves than a smartphone because a select few people find it interesting. Only ~30 top professionals actually make enough money to have a full career playing chess, maybe a few hundred more can sustain a meager lifestyle with coaching gigs. I shudder to imagine what will happen to the tens of thousands of non-Fields medalist caliber mathematicians if math goes the way of chess. Perhaps Terence Tao and a few other famous mathematicians will be funded by Peter Thiel to report on how well humanity can keep up with the machines? How do you expect any mathematician to be optimistic about this comparison.

I'm not an expert at it myself, but my understanding is there are numerous ways to "cheat" in a Lean proof (via `sorry` and similar). They're taking responsibility for fully verifying that none of these cheats were used (and that the theorem statements themselves were all correctly formalized.)

Perhaps not, but I interpreted it as an intended counterexample to the GP's claim

> You'd have a hard time convincing most American families to purchase anything with a >$1000 price tag...

Which I am skeptical of.

Is it really wrong to blame this one on philosophy? The source of the disagreement was inherently philosophical, lead by a philosopher, backed up by other mainstream philosophers, and undeniably held back physics. I don't mean to imply that philosophy is fundamentally evil or useless even when applied to physics; most early physicists also considered themselves philosophers. I'm just pointing out a mildly interesting pattern that I have noticed while reading about the history of physics. I recall that Einstein credited many of his insights to the field of philosophy. He also famously rejected quantum mechanics due to his philosophical beliefs, which many consider a slight stain on his legacy.

I have personally never met someone with a personal robotic lawnmower, and I suspect that if you have you live in a bubble that is severely biasing your view of the average American.

It was indeed sexism, but it was not sexism from the math department, who very much wanted to hire her. In fact, the Chair of Mathematics David Hilbert (of Hilbert space fame) personally recruited her.

A very interesting story that's worth reading up on. "Natural philosophers" of the day refused to accept the idea of a particle too small to directly observe on purely philosophical grounds. They essentially bullied him out of the field for championing the idea of the atom, despite his math yielding numerous correct results. They fruitlessly pursued the idea of energetics instead. (One of the many instances of die hard philosophers playing the villain in physics history. See also why Emmy Noether wasn't given a professorship despite a letter of recommendation from Albert Einstein.)

This makes it perhaps not a particularly good example of the phenomena being discussed, as he was suicidal not because of what he had discovered, but because no one believed what he had discovered.

The author recently published a retranslation of the Odyssey, that has rocketed to the top of best seller lists thanks to the movie. I'm sure her bank account provides her plenty of direct evidence that this is happening.

Writing a screenplay adaptation of a poem and writing a translation in contemporary language are entirely different endeavors.

I would guess almost none, less than single digit percent. Only a small fraction of undergraduate math majors who happen to be interested in algebraic geometry would be able to understand this. The average HN user knows far less math than an average undergraduate math major. Of course there are also math PhDs and the like on here, but vanishingly few compared to the bulk of the site.

1) How do you know this structure is the correct one a priori

2) You are starting at 10^500 possibilities. "Much" smaller is not enough, the order of magnitude of the order of magnitude needs to be changed.

3) You still need all of the other assumptions, which were completely unfounded

Impossible.

Honestly just try it. You'll figure out the problem very quickly.

This is not true at all. The parameter space is absolutely MASSIVE. The counterexample is a degree 7 polynomial in 3 variables, which means 360 coefficients. There's no particular way to bound these coefficients or even the degree or number of variables apriori, but assume you somehow did. Also assume you were confident that it would work with integer coefficients bounded from -12 to 12. Now you have to iterate over 360 degrees of freedom, verify that the Jacobian is a nonzero constant, and somehow show uninvertibility of the transformation, which is not a particularly simple task.

If you searched for coefficients from -12 to 12, this would be 25^360 = 2 * 10^503 different possibilities. A common reference point is that there are 10^80 atoms in the observable universe. Sure you could probably reduce this a bit with clever tricks, but the starting point makes the method completely unviable, even with the knowledge: A) a counterexample exists, B) it's in 3 variables, C) it's in degree 7 or less, D) it's in integer coefficients, E) those coefficients are 12 or lower.

Perhaps there was something in the prompt or settings preventing this, but I'm surprised (and slightly disappointed) that none of the models approached this the way I would: download an image of the Mona Lisa, run all of the drawing functions many times to construct a forward model of the drawing implements, and attempt to solve some kind of explicit inverse problem through either ML or a classical algorithm to minimize some difference metric. Were they just restricted from running code or are the models unindustrious without a very specific prompt?

That is exclusive to engineering PhDs, entirely irrelevant to the discussion of math PhDs.

As someone who has met a lot of math majors and a lot of CS majors, I am skeptical of your supposition that CS majors are better at finding and applying novel abstractions than math majors who know how to code.

I didn't watch it myself, but there was a recent Netflix documentary on the subject where Magnus claims he was misled by chess.com into believing that they had more concrete evidence than they did.

From Cambridge dictionary:

obscure (adjective)

not known to many people:

- an obscure island in the Pacific

- an obscure 12th-century mystic

Why does its use in production matter? Perhaps the syntax itself is obscure, but we're not discussing syntax but general awareness. Anyway, the most common "real" use of brainfuck is to prove Turing completeness of other things by finding a way to compile them into brainfuck.

What? Brainfuck is the single least obscure esoteric programming language. It's the most famous example of a simple Turing complete language and its provocative name gets it a fair amount of media coverage outside its niche.

This is true, but the crushing response to this scandal is clearly disproportionate. Millions of views on videos making crude sexual jokes about a 19 year old is already an incredibly unfortunate situation, and his career got completely halted for years due to (what are now clearly) false accusations.