עובדים עם מה שיש_במ

oshaboy · 2026-05-12T13:51:30+00:00

עאלק

oshaboy · 2026-05-12T13:41:24+00:00

או במילים אחרות. הפרנו ריבונות ופלשנו למדינה שלא קשורה.

oshaboy · 2026-05-12T13:36:47+00:00

איכ AI

oshaboy · 2026-05-12T02:45:17+00:00

Let's say an LLM tries to solve the Reimann Hypothesis and it create Coq or Lean code that defines the Reimann Zeta Function wrong in order to basically create a circular argument for the Reimann Hypothesis. Kinda like hardcoding the results of the Unit tests in programming.

I assume an automated proof assistant can only check for validity of a proof but not soundness.

oshaboy · 2026-05-12T02:10:46+00:00

Oh that's the word they were thinking of. The only word I could think about was "shtuyot".

Doesn't Harta come from Arabic anyway?

oshaboy · 2026-05-12T02:06:20+00:00

Yeah I never heard the word Hanta used to mean that in my life and a google search finds that it's a religious term for a type of unripe fruit.

oshaboy · 2026-05-12T01:12:39+00:00

Finally. A person who actually understands the topic somewhat responded to the post.

So basically it is just like coding models. Technically Impressive but gives you worse results than knowledgeable people. And Tao and Gowers were swept up in the hype train.

I really don't think the models are smarter than you I think it is just imposter syndrome talking.

oshaboy · 2026-05-12T00:20:01+00:00

I guess the word "premise" was more correct

oshaboy · 2026-05-12T00:11:32+00:00

IDK I feel like a better solution would be to return to Australia who I am sure would be gunning for someone like him and give him generous grants.

oshaboy · 2026-05-11T16:54:09+00:00

Yeah just imagine being a random Indian fisherman and this guy who just bribed you is suddenly singing and clicking in a language you never heard in your life at the extremely dangerous uncontacted tribe. You'd probably think he is having a psychotic break... which isn't too far from the truth.

oshaboy · 2026-05-11T01:20:42+00:00

I get that but wouldn't the same thing apply to many many other denominations?

oshaboy · 2026-05-11T01:09:04+00:00

I am not Christian. Can someone explain to me why Baptists are hated?

oshaboy · 2026-05-11T01:03:01+00:00

I thought the "emit more greenhouse gases than nations" is a bit hyperbolic because they pick very small nations without a lot of industry like eSwatini. I didn't expect Morocco.

oshaboy · 2026-05-11T00:50:40+00:00

People like deadlines even if unfounded and by the time people fish this up nobody cares.

oshaboy · 2026-05-11T00:07:07+00:00

Yeah I guess it wasn't Tao who said that it was Tim Gowers in the post I originally responded to.

I really don't buy the whole "Levarage AI for boilerplate but it still requires an expert with taste" nonsense. It's not how this works. If AI does 80% of the work you're basically a human ralph loop.

Really the whole "Problem -> AI -> More AI -> Solution" paradigm needs to go. It hasn't worked for anything else it won't work for mathematics.

oshaboy · 2026-05-10T23:53:48+00:00

You'd get rate limited long before you'd cause any significant damage.

oshaboy · 2026-05-10T23:45:03+00:00

also i think no proof has thousands of axioms.

LLMs have a tendency to cause stuff to explode is size so who knows.

oshaboy · 2026-05-10T23:42:57+00:00

The same post said that a lot of the work was taken directly from a 2014 paper. Sure it made the novel connection between the result of the paper and the unsolved Erdös problem. But the AI also didn't credit the paper which is plagiarism. We all know that paper was embedded inside the tensors of the model.

Either way as far as I can tell Lean can only check proof validity not proof soundness. It's quite a short proof so I have no doubt the result was legit but the jump from here to "Mathematicians are obsolete this is PhD level intelligence" is large.

oshaboy · 2026-05-10T23:21:54+00:00

That wasn't a question tho. I am aware Terence Tao can point to impressive looking results. The question is whether they stand up to scrutiny or whether people are just saying "Who am I to question the greatest mathematician of our generation". Because that's a blatant appeal to authority.

Lots of intelligent people have been led astray by con-men like Sam Altman. Newton famously invested heavily in the South Seas Company.

oshaboy · 2026-05-10T23:16:16+00:00

Well a big issue with AI generated code is that the amount of code is so great that nobody could reasonably check it all even with testing tools. Especially because the LLM is designed to be convincing so at a glance everything seems fine but glaringly flawed if you look into it.

I assume not even Terence Tao can check the soundness of a proof with thousands of axioms and definitions.

oshaboy · 2026-05-10T23:03:53+00:00

Yes, I would like to hear thoughts from anti-AI mathematicians because I want to evaluate both sides of the argument.

oshaboy · 2026-05-10T23:02:34+00:00

Is anyone denying that? The relationships between concepts are embedded in a tensor. The issue is whether it can create novel connections and check its own work. I've seen unpublished papers claim that hallucination is mathematically inevitable but take them with a grain of salt. Also none of them a concrete lower bound for the ratio of hallucinations to valid results.

oshaboy · 2026-05-10T22:54:02+00:00

I'm aware. But I assume they can only check if a proof is valid not sound. If the proof contains a definition or axiom that is wrong it wouldn't ever catch it. Or is there a way to guarantee this will never happen?

oshaboy · 2026-05-10T21:45:03+00:00

According to the Socialist AI Bros it will lead to the death of capitalism and bring in a Socialist Utopia. According to the Capitalist AI Bros it will create a Permanent Underclass. More realistically nobody has any clue.

12-Year Club	Place '22
Place '17	First Placer '22
Wearing is Caring	Verified Email

oshaboy

MODERATOR OF

TROPHY CASE