YHK - yet another hacker news clone

Sharing AI Progress in Mathematics

202 points OfficialTurkey 1 hour ago 139 comments

https://github.com/openai/math

senderista 1 hour ago | parent

Good to see they're engaging with the mathematical community, even if they had to be publicly shamed into doing so.

karahime 1 hour ago | parent

Extremely unfortunate that gate keeping got to the point where they felt the need to ask for permission to share math.

bravoetch 52 minutes ago | parent

In previous math sharing there was speculation about stealing human researcher's results or progress, via prompt inputs from those researchers, and sharing that as their own result. They're adjusting their process, and it seems ok.

xpct 51 minutes ago | parent

Just to be very clear: they aren't asking for permission, they are framing it that way because of the bad press.

There's no gatekeeping here!

reasonableklout 31 minutes ago | parent

I think it's generally a good thing that OpenAI is noticing when their projects are harming human communities, and deciding to respect their norms, especially when their math discoveries do not have immediate application and build on the thousands of years of that community's work.

hgoel 18 minutes ago | parent

After how poorly OpenAI and Anthropic handled the previous cases, I approve of the more measured and cautious approach this time.

We cannot have them rushing to publish amidst tons of confusion, rumors of threats/scooping and outright plagiarism of existing work (by failing to cite said work).

If they're going to participate as scientists in these more rigorous fields, they're going to have to match that level of rigor, not lower it to the disastrous low that ML research publication is at.

binlog 1 hour ago | parent

So happy this is shared on GitHub rather than some gatekeeping paid journal. Truly a new age for science.

fph 52 minutes ago | parent

Most mathematical results are shared on Arxiv. Journals add peer review.

traes 41 minutes ago | parent

GitHub is a significantly worse place to store important results than Arxiv. Of course, slop does not belong on Arxiv, buy slop should also not get published.

adverbly 7 minutes ago | parent

End of an age for journals?

rafterydj 1 hour ago | parent

I don't know, this does not feel like the message hit OpenAI where it needed to hit, if this is their primary response.

osiris970 53 minutes ago | parent

You want them to stop doing math research?

k2xl 1 hour ago | parent

Can someone knowledgeable about the subject outline the most significant portions of the results?

sebmellen 1 hour ago | parent

It’s fascinating to read through the reasoning traces: https://github.com/openai/math/tree/main/reasoning_traces

Look at one of their examples of an initial prompt: https://github.com/openai/math/blob/main/reasoning_traces/re...

ndriscoll 57 minutes ago | parent

> Thus at most one informative i. So cheater chooses arbitrary g_{v_i}, on exact duplicated input matches and passes, independent of actual satisfiability!

No idea what it's so excited about, but it's cute that it "is." I for one welcome having access to a math buddy 24/7 that's way above my level but also always "willing" to talk at where I'm at.

adverbly 20 minutes ago | parent

> Look at one of their examples of an initial prompt

Interesting that its only an excerpt. I wonder what else they include but didn't share.

gizmodo59 1 hour ago | parent

This is significant progress and released without all the drama. Some very important progress in Reinmann, Hodge and unique games theorem. Point the repo to your agent and ask for the significance! In a way this is probably 50-100 years of math progress by humans

fspeech 49 minutes ago | parent

Math is the tool humans use to compress knowledge. So until we can comprehend it there really isn't much progress. Math theorems are tautologies, the truth of which are not dependent on proofs and proofs are erasable, at least classically. But the AI progress is exciting and AI proofs are a gold mine for humans (at least non domain experts) to explore.

gizmodo59 46 minutes ago | parent

>So until we can comprehend it there really isn't much progress.

Not really? We are at a point if an AI today can solve it, it can be stepping stone of understanding something deeper to tomorrows AI and it continues. Sort of like our limitations doesn't matter. Obviously there are many scenarios in this recursive loop but saying it isn't much progress is not how I view this as

fspeech 43 minutes ago | parent

If it changes how we think then yes it has an effect.

fspeech 45 minutes ago | parent

Another way to state this: math theorems are like programs without side effects; it is immaterial whether a program without side effects is ever run. We study math for the side effects: it changes how we organize our thoughts.

warkdarrior 44 minutes ago | parent

> Math theorems are tautologies

Proven math theorems are tautologies.

fspeech 43 minutes ago | parent

True.

fspeech 42 minutes ago | parent

Flt was no less a tautology before it was proved. We just weren't sure about it. Proofs only change us, not math.

binlog 43 minutes ago | parent

What makes you think no one can comprehend this? It has been less than an hour since it dropped and there is already a ton of online chatter from people explaining the results, pointing out their favorites and more. Some of it is happening on this very thread.

fspeech 38 minutes ago | parent

I didn't say that. I am responding to "In a way this is probably 50-100 years of math progress by humans." I am actually very excited about AI proof and I am working overtime in my own way to try to comprehend as much as I can.

gpt5 40 minutes ago | parent

Math is far more than that. If you can solve prime factorization for example, suddenly you can listen and interfere with almost every private conversation on the internet.

We are not far away from the moment where these models will be restricted, and sharing the results will be done more carefully.

fspeech 33 minutes ago | parent

This doesn't contradict what I said. But I do appreciate the fact AI can produce side effects not just humans. I made it sound like only human knowledges matter. That's too narrow.

caaqil 39 minutes ago | parent

> until we can comprehend it there really isn't much progress

Who is "we" here exactly?

fspeech 30 minutes ago | parent

Whoever wants to study the result.

caaqil 18 minutes ago | parent

> Whoever wants to study the result.

Right. Before all the AI disruption, pure Math traditionally welcomed anyone who wanted to study its esoteric proofs, right? I remember all the excitement of the average Math enthusiast casually reading Wiles' proof over coffee.

Bottom line is, the relevant people can still understand the generated proofs. The disorienting part is they are a little slower than they'd like, but they'll get there.

yieldcrv 17 minutes ago | parent

Academics have been treating it that way because they had no other choice, and its been a waste of everyone’s time and often times taxpayer resources

Look at that, taxpayer funding was cut and a private sector solution came in just the nick of time, far accelerating the holding patterns we’ve been in for decades

Humanity doesn’t need all iterations towards the blueprints, the blueprint is good enough, we all stand on the shoulders of giants

fspeech 7 minutes ago | parent

I think it would be helpful to people who want to understand what a formalized proof is to read Thomas Hales on this: https://www.math.stonybrook.edu/~bishop/classes/math536.S24/...

He spent years formalizing his sphere packing theorem because the proof (human produced) was already beyond the ability of peer review. Now his formalization efforts likely can be easily reproduced by a model. However one should read his experience about what a formal proof is: often the problem is the statement not the proof. The example he gave is the Jordan curve theorem. It's actually quite challenging to formalize the concept of a planar curve (there are space filling curves). So it is not necessary that someone can look at a formal statement and say aha it is about a planar curve, unlike FLT where there is not much problem in recognizing what the statement is about.

traes 43 minutes ago | parent

Not to pick on you specifically, but as someone who spends a lot of time unproductively reading AI math discourse it's truly shocking how incapable all the supposed math enthusiasts are of spelling Riemann.

xpct 40 minutes ago | parent

I just did a quick search on this and apparently the misspellings are German surnames as well:

https://en.wikipedia.org/wiki/Reimann

https://en.wikipedia.org/wiki/Reinmann

conformist 33 minutes ago | parent

Yes sure but they are different surnames and pronounced differently.

xpct 29 minutes ago | parent

I didn't mean to oppose OP's point, I just found it interesting as a non-German speaker!

traes 23 minutes ago | parent

I just don't understand how it happens. If they had ever taken an intro to real analysis class they would learn to spell his name. If they were just parroting what an AI told them... shouldn't they still just say his name? An individual could just be dyslexic or mistaken but it seems to be a substantial volume. I guess they just don't care enough about it to commit the correct name to memory, only remembering the "pattern" of the name and filling in the spelling via guesswork?

NewsaHackO 18 minutes ago | parent

People just don’t spell that seriously buddy, especially when it is so immaterial to the point.

traes 14 minutes ago | parent

My point is it is crazy to make public claims about how important or not important a mathematical result is when you can't spell Riemann. Yes, it technically doesn't matter, but it betrays a damning lack of familiarity with introductory mathematics.

ndriscoll 13 minutes ago | parent

Maybe they skipped straight to Lebeg integrals.

lanyard-textile 21 minutes ago | parent

They're mathematicians, not linguists :)

traes 16 minutes ago | parent

The mathematicians don't make this mistake, I assure you. I doubt there is a math professor on planet earth who would spell Riemann as Reinmann. In fact, I imagine no one who has ever heard the name pronounced would do so.

zone411 20 minutes ago | parent

There was A LOT of drama about this release.

enoether 1 hour ago | parent

Unique Games Conjecture [0] is a seminal conjecture in Complexity Theory, and is an underlying assumption for many, many inapproximability results. A valid proof is a big deal!

[0] https://en.wikipedia.org/wiki/Unique_games_conjecture [1] https://github.com/openai/math/blob/main/preprints/The-Uniqu...

impossiblefork 41 minutes ago | parent

Yeah, that's one of the big things of TCS. I think I see that as bigger than that Millenium Prize problem.

gregdeon 28 minutes ago | parent

This was the biggest highlight for me as well. Astounding...

inkysigma 11 minutes ago | parent

I also don't think there was general consensus on which way this would resolve prior to this (or is that a little out dated?) unlike some of the other major problem resolutions. I heard rumors that there would be a big result in TCS and speculation it would be UGC that or P neq PSPACE but I'm still a bit shocked.

Catloafdev 1 hour ago | parent

This is a pretty hilarious thing to read juxtaposed with AGMAI's requests.

Basically "Here you go, have fun with this, fuck all your demands, by the way we're gonna be releasing the model stay tuned!"

open592 59 minutes ago | parent

Let's hypothetically say I'm a PHD student who is half way through my studies and I have a halfway written version of one of these "preprints" - what do I do?

Seems like a lot of PHD students are doing to have to pivot the entire structure of their PHD studies? Or just produce something which is already written by OpenAI?

goalieca 57 minutes ago | parent

Don’t paste your research into these AI because they will train on it and then scoop you.

esafak 49 minutes ago | parent

I think that happened after word of the project reached OpenAI and they allocated resources to it.

binlog 57 minutes ago | parent

Use whatever is published as the new base for your research. Use AI tools to help you going forward.

xpct 48 minutes ago | parent

In other words, you've already taken a gambit with the first half of your PhD, now take a second gambit, praying that you have something to publish by the end of your PhD.

It has to feel awful to be in this position.

torben-friis 44 minutes ago | parent

Could be worse, imagine having years of experience in a profession these things can now handle by themselves.

:)

caaqil 53 minutes ago | parent

> what do I do?

Precisely what all NLP researchers and the ML community at large did in the last few years: embrace the frontier and realize that attention is all you need.

aaraujo002 53 minutes ago | parent

This happens all the time, even without AI. Other researchers or PhD students can publish the same results before you. I say that based on my experience during my PhD.

dcl 52 minutes ago | parent

This has always been a challenge for PhD students and researchers, it's just far more likely to occur now it seems. Getting scooped doesn't feel good, but it's a signal you've been thinking about things other people care about.

dekhn 50 minutes ago | parent

Let me give you some perspective: my entire phd was made obsolete by CRISPR. It was a wonderful thing.

thimotedupuch 39 minutes ago | parent

Interesting. If you don't mind, could you please share a little bit about that ? You already finished your dissertation ? It was about the works of Doudna and Charpentier ?

dekhn 29 minutes ago | parent

No, back in the late 90s and early 00s, people were trying to engineer custom nucleases and transcription factors, my work was on doing molecular dynamics simulations to optimize TF sequence specificity (similar to engineered zinc fingers) for gene therapy. I wrote up my dissertation and published it in 2001, and then went off to find enough compute, IO, and smart people to make it happen (https://research.google/blog/groundbreaking-simulations-by-g...).

My approach would require custom engineering for every different sequence we'd want to target. With CRISPR, you just "program" the system with a guide sequence, you don't need to do massive engineering to solve a protein design problem.

vinyl7 47 minutes ago | parent

Look forward to being obsolete I guess

bobmarleybiceps 44 minutes ago | parent

I think eventually companies won't get as much stuff that's usable for marketing, so they'll stop investing so much into ai for math, so eventually cheap and poor graduate students will be able to do relevant work again without worrying about getting scooped by a company with a million GPUs :-/

moralestapia 25 minutes ago | parent

That would be unfortunate but the world does not owe you anything and is not going to stop for you. Which is also a valuable thing to learn in your 20s (ideally earlier).

hgoel 23 minutes ago | parent

It could still be interesting if your approach to the problem was different to theirs.

claaams 19 minutes ago | parent

Don't worry, if you use openAI and get lucky they might offer to share credit with you for your work.

yieldcrv 16 minutes ago | parent

Yes, and?

glitchc 16 minutes ago | parent

Perhaps consider switching to a more applied field. Experiments in the physical realm hold value, especially if you document the process.

ks2048 56 minutes ago | parent

I think they should put human names on the papers as someone who has reviewed the result, even if just a preliminary review. (I’m assuming they didn’t just pipe their model output directly to the internet and these had some amount of review?)

xpct 44 minutes ago | parent

Presumably they don't because they're training the audience (us) to trust the machine, not its verifiers, even if they were included.

alexgoodhart 19 minutes ago | parent

I appreciate you acknowledging the politics behind this. OpenAI does not intend to be a software company for long, they intend to be scientific infrastructure. They'll want to be faucet from which pours embryos, orbital calculation, geothermal/substructural rating, and etc.

agnosticmantis 17 minutes ago | parent

Long term this will be the only reasonable author list: Chad G. Peter {1}, Mat H. Lean {2}.

1: Author 2: Verifier

/s

aaraujo002 55 minutes ago | parent

The Advisory Group states in its recommendations [1]:

"We want to state clearly from the start: we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models."

To me, this is a take against progress so that mathematicians can keep their jobs. What would we do if, instead of math, we were talking about diseases? Are we going to keep diseases around so that doctors can keep their jobs too?

[1] https://agmai.org/general-sep29/

osiris970 53 minutes ago | parent

Comical ask

medler 51 minutes ago | parent

The rest of that document makes a pretty compelling case for why this is a bad practice

esafak 44 minutes ago | parent

I fear that professional mathematics will wither, and there will be nobody left to digest the AI results of the future, leaving us unable to challenge the AI.

warkdarrior 50 minutes ago | parent

The latest posts from Terry Tao on Mastodon effectively ask for an AI to explain its results to human mathematicians.

> "I believe that AI can contribute positively in all of these directions [NB: exposition, community building, new directions of study]"

https://mathstodon.xyz/@tao/117395269325940185

jhrmnn 48 minutes ago | parent

It all hinges on the definition of “progress”. The debate of the past month is all about questioning whether formally proving outstanding unproven theorems without human understanding constitutes progress. This is quite different from solving diseases.

mattr03 48 minutes ago | parent

I don't think this is a reasonable take at all. Most work on maths has no real benefit other than to further human understanding of maths - it's more like an art. Nothing is gained from OpenAI solving all these problems but taking jobs from mathematicians. Other than advertising for OpenAI at least. It could not be more different from having AI work on disease research etc.

bravoetch 29 minutes ago | parent

> Most work on maths has no real benefit other than to further human understanding of maths - it's more like an art.

It's been a while since I was reminded of this xkcd: https://xkcd.com/435/

fph 48 minutes ago | parent

...but we're not talking about diseases. Publishing an AI-generated Navier-Stokes solution does not save lives. (And, in fact, it harms some.)

tchalla 47 minutes ago | parent

Why did you leave out the entire quote?

> At present, some frontier AI labs are testing advanced mathematical problems on proprietary models that remain inaccessible to the broader scientific community. Our recommendations are formulated with this practical context in mind. However, ideally, they would not do so. We want to state clearly from the start: we do not endorse this practice, and we ask them to stop testing advanced mathematical problems on proprietary models.

To me, the issue is that the models are proprietary which are only accessible to a few people in 2 digits. It's not about progress but access.

aaraujo002 42 minutes ago | parent

Maybe, but it still seems like an excuse. OpenAI has a proprietary model capable of solving these problems and is willing to share the results with the mathematical community. So basically, the ask is to just not use the model and leave the problems unsolved?

adrian_m 20 minutes ago | parent

The ask is to let mathematicians outside of OpenAI use it, ie. at least wait until the model is released.

agnosticmantis 2 minutes ago | parent

Which mathematicians though? Only fields medalists? Grad students? Any hobbyist wanting access?

perching_aix 45 minutes ago | parent

The trope you're drawing a parallel with has a (to me) compelling counter though: there being a cure for every disease wouldn't stop people from getting sick.

Not so for maths.

bmitc 22 minutes ago | parent

Advocating purely for progress and not humanitarian value is how we'll all get enslaved.

pavitheran 54 minutes ago | parent

From the GitHub description: “On average, each result used 3 hours of ChatGPT Pro thinking compute”

password54321 46 minutes ago | parent

Oh cool, we will all now have a math genius on our computer.

an0malous 27 minutes ago | parent

Well, on their computers. But you can rent them for a price.

jrflo 15 minutes ago | parent

It was using their internal math model, so not yet for us

password54321 12 minutes ago | parent

I used future tense. It was implied this will be available.

scrlk 39 minutes ago | parent

Does this imply that it was a one shot prompt with ChatGPT Pro style models (i.e. best-of-N), rather than the agent swarm approach that was used for Navier-Stokes?

inferencecoder 2 minutes ago | parent

It doesn't imply that, it's just measuring the amount of compute.

orlp 25 minutes ago | parent

I'd really like some clarity on what that means. E.g. DeepMind has 'cheated' with this in the past, claiming that AlphaZero only took 4 hours to reach super-human chess levels while conveniently leaving out the fact that it was 4 hours x 5000+ TPUs. Sure it's impressive that it only took 4 hours wall-clock but it's very misleading as to cost.

Can we get a number in Blackwell GPU-hours, kWh, or some other compute-scaled metric?

timjver 21 minutes ago | parent

>OpenAI has 'cheated' with this in the past, claiming that AlphaZero [...]

That doesn't sound right

orlp 19 minutes ago | parent

Oops, edited.

machomaster 10 minutes ago | parent

They did say that. "3 hours of ChatGPT Pro thinking compute"

Jtarii 4 minutes ago | parent

That estimate is obviously going to conveniently ignore all the failed runs.

mathisfun123 53 minutes ago | parent

With so many results in so many different areas no way they even remotely spot checked well enough.

Prediction: one of these is wrong and this (publicity stunt) will backfire.

Edit: don't tell me about lean. For lean to function as a proof certificate you need to represent the theorem correctly. Again: good luck doing that across such a broad swath of problems.

bravoetch 50 minutes ago | parent

What does a backfire look like? It's ok to be wrong in the science/math world.

mathisfun123 46 minutes ago | parent

of course in science/math it is but it's not okay if you're a business selling supercalifragilisticexpialidocious infallible intelligence.

bravoetch 27 minutes ago | parent

Do they claim that's the case? I don't think they do.

mathisfun123 20 minutes ago | parent

does company A making product B claim that the product is robust and consistent? is this a serious question?

jojva 31 minutes ago | parent

You have not read their readme:

> Some of the unformalized results could have issues. We will endeavor to fix any such issues quickly. We are also exploring community-hosted repositories for these materials.

mathisfun123 29 minutes ago | parent

i have and i'm exactly saying that if it comes to pass one of them is wrong it's going to backfire. ie yes that's my exact point/bet.

dekhn 51 minutes ago | parent

I'm a software engineering/biology/ML guy who loves when clever math ideas get turned into real solutions (https://en.wikipedia.org/wiki/Compressed_sensing). I am curious if any of the results have immediate applications in any kind of engineering or science.

It's fine if not, but it'd be great if even just one of these helped us solve a long-running problem.

kevinwang 46 minutes ago | parent

wow

prideout 45 minutes ago | parent

This includes a proof of Barnette's Conjecture, which is one of the graph theory conjectures that I tried attacking with SOTA models a few months ago. I like it because it is easy to understand with a basic knowledge of graph theory. I spent quite a bit of time on it and failed. Their proof looks approachable at first glance.

https://github.com/openai/math/blob/main/preprints/Paired-st...

kingstnap 45 minutes ago | parent

Some of these are interesting ngl.

109. Integer multiplication below n log n

Surprising that this is possible.

158. The Euclidean plane cannot be colored with five colors.

Only 6 and 7 remain!

376. Universal computation in forced Navier–Stokes flows.

Morning coffee proven turing complete

mFixman 37 minutes ago | parent

> We give a deterministic algorithm that multiplies two n-bit integers in O(n (log n)^(1−κ)) worst- case time, with κ = 2^(−182).

LMAO, I don't think I ever saw such a small number in a CS result.

sobellian 34 minutes ago | parent

I am fully braced for it to be a https://en.wikipedia.org/wiki/Galactic_algorithm

Very surprising result though! Multiplication is easier than sorting.

kingstnap 30 minutes ago | parent

Yeah its ridiculously small, but any improvement on n log n is wild.

Like there is somehow redundancy in a fourier transform that makes it sub Linearithmic?

Which low and behold ->

130. Fourier transforms below n log n.

xyzzyz 26 minutes ago | parent

They also separately give algorithm for Fourier transform over complex number faster than O(n log n)

mi_lk 45 minutes ago | parent

Curious if Sébastien Bubeck still work at OpenAI? He came out quite dirty after Navier-Stokes drama

yewenjie 43 minutes ago | parent

A lot of these seem to be proving conjectures rather than finding counterexamples, a lot of people used that to claim that these models are not really smart/creative etc.

That copium didn't last for what, three months?

redox99 36 minutes ago | parent

The stochastic parrots have predicted the next token once again.

connor11528 32 minutes ago | parent

will this make the math for building data centers work?

foota 26 minutes ago | parent

From their github: "The average result used the equivalent compute of roughly three hours of ChatGPT Pro thinking." That's pretty crazy.

zone411 24 minutes ago | parent

A quick check shows that this list claims to fully solve 90 of the top 500 open problems in math (https://proofatlas.ai/open-problems/).

The highest ranked would be:

| 22 | Hilbert’s tenth problem over ℚ |

| 29 | Unique Games |

| 31 | Anderson-model extended states |

| 37 | Spacetime Penrose inequality |

| 48 | Nonexistence of Landau–Siegel zeros |

| 52 | Baum–Connes |

| 78 | Abundance |

| 80 | Hadwiger |

| 87 | Bose–Einstein condensation |

| 92 | Two-dimensional entanglement area law |

applicative 18 minutes ago | parent

Why didn't they just give mathematicians access, so they could at least understand and write up the results in publishable form?

stevenhuang 3 minutes ago | parent

They're all here https://github.com/openai/math/tree/main/preprints

anematode 14 minutes ago | parent

Dear lord that website is laggy

nautilus12 19 minutes ago | parent

Have any real mathematicians working on these problems reviewed any of these and determined if they are just gobbledegook or not?

The ones with lean proofs could still be formulated incorrectly

NotOscarWilde 15 minutes ago | parent

As a TCS/scheduling person, this one is definitely of lesser importance than UGC, but it has been an open problem since the book of Garey and Johnson in 1979:

A Polynomial-Time Algorithm for Three-Machine Unit-Job Scheduling [1]

Since some people talk about small numbers that pop up in integer multiplication results, here a completely different number appears:

Theorem 1.1. Let an explicitly listed finite directed acyclic graph specify the precedence constraints on n >= 1 nonpreemptive unit-length jobs on three identical machines. There is a uniform deterministic algorithm that constructs a feasible schedule of minimum makespan. Given also an integer deadline 1 <= T <= n, it decides feasibility exactly and returns a schedule whenever the answer is affirmative. Both tasks can be performed in O((L + 2)^150020) steps on a deterministic multitape Turing machine, where L is the total binary input length.

That is some crazy exponent -- plus an interestingly old computational model to boot; not something that is natural to most of us. I have no capacity to check its correctness today, but I hope it is true purely for the exponent.

[1]: https://github.com/openai/math/blob/main/preprints/A-polynom...

jrflo 14 minutes ago | parent

Glad to seem them changing their tact with the whole NS debacle. Hopefully we can all focus on the results now rather than the surrounding drama.

curtis-jm 13 minutes ago | parent

You can read the papers here: https://hub.valency.io/collections/openai-math

againstapples 8 minutes ago | parent

As an AI "doomer" can I ask the non-doomer people here how you interpret the significance of results like these, and what kind of progress you expect to see in the next 1-5 years?

Like do you see the technology plateauing at the current level, do you expect progress will continue but only in mathematics, I'm interested to know why others are not concerned?

never_giveup 3 minutes ago | parent

Try using AI for your work, whatever you do. You will quickly understand the limitations.

schleck8 3 minutes ago | parent

This is the biggest ever breakthrough in mathematics and from a few papers I've checked, not reliant on just extrapolating existing theories but actually shows novel/surprising approaches. Very few people globally could come up with something like this, even when given time and ressources.

So in other words, since deep learning is algorithmic research, we are now in the RSI era.

applicative 8 minutes ago | parent

I wonder if the Lean compiler can change it's license so that a for-profit corporation can only use it if it pays, say, a few hundred billion dollars. This is the correct path.

xanderlewis 3 minutes ago | parent

As Kevin Buzzard recently said:

> In a 2020 piece in the Notices of the AMS, I asked the following question: “If one human had an understanding of all of modern pure mathematics simultaneously, how much further would they immediately be able to see?” Six years later we are beginning to understand the answer to this question.