Compared to what OpenAI is claiming its word machine has solved (without any human verification for the claims so far, not even in OAI), the scribbles kinda are (just highschool math).

I am more skeptical. Even with Navier Stokes, I never heard anyone actually internalize the result and have trust in it. I just heard vague lean-dih waving.

Supposedly it’s 26000 subtheorems of goobledigook, feels untameable.

Mathematicians seemingly: Axioms are correct, we trust lean => Result correct.

As a physics, CS thinker: AI probably found a bug in our axioms. And/or usual self-referential math issue. And/or connected to Goedel’s incompleteness. Also I wonder why I even trust lean as much, havent even read its code. Most software works great until somebody starts poking at its limits.

How the robot proves these statement is by writing LEAN code that represents the math. If the lean compiles, the math was valid. If it doesn’t, it tries again.

It will do this forever until it finds a solution.

Goedel predicted this in 1933, btw. From his work on formal systems, he ascertained that since every mathematical statement is trivially true following from the rigorous application of the axioms of mathematics or entirely false, theorems could be checked and proven automatically.

These systems are able to prove statements at a scale beyond humans, because they have effectively infinite time to exhaustively explore applying every rule.

Unfortunately, this isn’t all that helpful for the various fields of math as a whole. Effectively they have a list of statements and a second column with ‘true’ or ‘false’, but the actual route taken by the models to get that answer is often incredibly indirect and therefore difficult to gain insight from and apply to new areas. The approach taken to produce an answer is often more valuable to the field than the answer itself.

The field moves forward when the people in it understand the new results and techniques sufficiently to begin asking new questions, simply giving the answer isn’t all that useful. The robots cannot (yet) do this. Someone has to, at a minimum, pose the question in formal mathematical language. There are an infinite number of true statements in mathematics ( trivial example 1=1, 2=2, …) asking the interesting questions is the important part. The field will still only advance as fast as the people in it are able to digest results.

Further, results in pure math do not generalize to the more applied fields that directly affect our ability to do things. Most engineering formulae are NOT rigorously true - they are weak approximations with envelopes of applicability. The same is true even in base physics. So while a robot can crank through ten million lines of lean to prove an obscure theorem, it cannot think about physics for a week and come up with a theory of quantum gravity.

Because the AI contribution was so huge was surely the reason openAI did not want to give any credit to the researches that worked on the foundation for that breakthrough.

Assume all that is true, AI can really do well in these fields, but there are some other fields it can’t do well in.

Now who is going to work on those fields? Who is going to take the risk of studying for it, practicing for years, being an expert in the field that takes maybe a decade, and the AI can suddenly solve your field too, and you don’t get anything.

Super fucking sorry that my finding a way around the paywall wasn’t good enough for you.

But of course, you couldn’t even link it either for some reason.

So here’s what I say we do:

You block me so you never see me putting effort in, you’d have came here, not seen my link or any discussion.

And then maybe you’d actually provide your paywall removed link for everyone instead of bitching.

Now I’m doing something to, don’t worry.

I’m going to block you, because obviously it’s hard for me to put up stupid shit like this.

And I just never want to see anything from you again.

Everyone wins champ.

I hate AI, but I’d much rather work for an AI over the idiot higher leadership at my company. They use AI for everything anyway, including literally answering emails.

I know people always say that, but there still needs to be executives so there’s still humans to be held accountable.

The vast amount of middle management are useless, but there has to be a human sitting in a chair above the chatbot for legal liability. Otherwise the board will just blame the chatbot for everything.

That also doesn’t mean they should be paid so much, just that a human needs to be above the chatbot as far as final authority

If you really thought that, you could have just typed what you thought I was wrong about instead of a literally useless comment…

In conversations with WIRED, the academics say they feel the field has become a playground for OpenAI and its rival Anthropic to show off their models as both prepare for blockbuster initial public offerings. In their rush to outdo each other, mathematicians say, traditional scientific processes for releasing and attributing results have been cast aside.

The most striking case so far came in September. OpenAI deployed thousands of agents to solve a legendary million-dollar Millennium Prize problem after hearing “rumors” that others were closing in on solutions. Tristan Buckmaster, a mathematician and professor at New York University, accused the company of front-running the work he had done toward solving an element of the problem in a personal collaboration with Anthropic employee Levent Alpöge. The pair hadn’t published their work but had been using OpenAI’s tools to help them.

Humans stole human work for their bots…

During an attempt to negotiate credit, Buckmaster claims, OpenAI researcher Sébastien Bubeck seemed to imply that Alpöge should be excluded from any paper, since that would make things complicated. (In response to a request for comment, Bubeck pointed to a previous public statement in which he denied asking for Alpöge to not be listed as an author.) Buckmaster said he refused. In a call, Bubeck claimed that there is some worry about what Anthropic is doing, according to meeting notes seen by WIRED. Levent must be talking to his leadership right now letting them know fucking OpenAI can get a Millennium Prize problem, he said, per the notes. What’s to stop Anthropic from giving all their compute to get a Millennium Prize problem?

The humans stole the credit from the other human to give it to chatbots…

According to the notes, Bubeck also seemed to suggest that Buckmaster would be ruining his career when Buckmaster threatened to tell the press about his belief that OpenAI had stolen his work. If you don’t want me to be nice, then I don’t have to be nice, Bubeck said, according to the meeting notes.

The humans at OpenAI threatened the human if he tried to claim credit.

But you really should read the full article

The cross-discipline general knowledge combined with the ability to churn huge datasets to find connections across already-known work, and extrapolate to or derive novel findings, is exactly one mode of superhuman success that AI companies have been trying to achieve.

Exactly.

Like in the quoted picture, there’s not a huge amount of people who have deep knowledge of Number Theory and the number of them who are also similarly versed in the math behind Quantum Physics could probably be counted on one hand and those people only have so much time.

Meanwhile, the only limitation in creating these AI systems is in how much RAM/compute we can manufacture.

It sounds more like when AI won in Go for the first time. People were looking at the game and saying “humans don’t play like that, we don’t understand those moves”.

I think it’s more that he’s saying “interesting approach, but not verified yet.”

I don’t think that’s what’s being said. More like the complexities of the solution are taking a while to understand because it is a complex solution using complex math. Even the smartest people in their fields can’t always look at a solution and at a glance understand everything without truly digesting what they’re seeing.

Can you expand on how you came to this conclusion?

That is not at all what he just said

In other words, it’s a political problem of control, not a technological problem of capability.

deleted by creator

The proofs are written in Lean so, like in all mathematics, you don’t have to trust the person because you can independently verify the proof.

deleted by creator

Looks like you have a misunderstanding of what a mathematical proof is. I have but a mere bachelor’s in applied mathematics and employed as a statistical engineer for a couple decades now. If a proof is successful at showing a mathematical statement is true, it’s a done deal. It doesn’t work like science which relies on mathematical models to explain its anecdotes.

Spot on, this is the thing people often miss out.

These problems aren’t actual problems in the way most people think about. They are problems in the way that they are exercises. Like the Navier Stokes problem is reporting in the news like one of the biggest problems in maths ever. Leading people to think we are stuck on it and can’t progress in some way without a solution. But in reality the limitations of the equation are well known and don’t impact normal every day use. And in cases where they would, we have other tools at our disposal.

The goal of these problems is to challenge mathematical people and push boundaries. Having a proof pop out of nowhere is like having someone tell you the answer to a question, where the whole goal was to formulate the answer yourself. The answer itself is meaningless, that’s why you get 0 points on the exam unless you show the workings out. It’s like having a movie spoiled for you, the goal wasn’t to know the outcome, the goal was the experience the story yourself.

Working backwards from some proof might lead to insights, but it also might not and be harder than working forwards. It also might pick a certain path, where there were multiple and we would be blind to the other paths. Those other paths might lead to more insights, if we had explored them.

The way OpenAI specifically has approached this is also very weird and awful in my opinion. Like they set their sights on yet again ruining some aspect of the world with AI and then throwing billions of dollars at it to make sure it’s properly ruined. For what purpose exactly? Not to make any money, that’s for sure, they are 2 trillion in the hole and counting.