Comment by anonymous908213 | Hacker News Reader

Comment by anonymous908213 | Hacker News Reader

Parent Full thread

anonymous908213

This is my hypothesis too. I work with LLMs daily. I use frontier models all the time, and I work in a startup that trains its own special-purpose models. At no point in the course of my work do I see anything resembling superhuman intelligence. I see superhuman stupidity, ie. stupidity so extreme that it exceeds what any human is capable of by orders of magnitude. So where are the superhuman math results coming from? Simple: translation. I've already thought this for a long time, that math is an obsfucated field and that programming already makes it far simpler to understand. So you train a machine to throw tons of compute at translating math into programming, and blow the field out of the water because it's effectively been deobfuscated. Math proofs had a sort of security by obscurity; they were not genuinely supremely difficult, but rather very few people worldwide worked on them and their work was heavily obscured, so the great deobfuscation machine comes along and trivialises that aspect and suddenly the facade crumbles. I think all of this could have been achieved a long time ago had humans done the deobfuscation, but there wasn't sufficient programming <--> maths cross-domain expertise or financial incentive to develop it.

This is not at all what mathematitians are saying. They say LLMs obfuscate proofs even more. Saying that mathematitians obscure proofs is nonsense. Maths requieres a big effort from the brain to be deobfuscated as you say, and deobfuscating maths requires understanding, which takes even longer. Thats why textbooks dont exist just after a new proof appears, it takes some time to digest it and identify the key parts.

Maths is a language, and learning a language takes time. Its like if I say that japanese made an effort to obfuscate their language just because i cannot read it or read it as fast as english.

LLMs are autimating some part of maths which is formal manipulation. It happens that computers are much better than humans at formal manipulation. In the same way that computers are much better at mathematical computations. That is the huge change in the field. But any working mathematitian can tell you that formal manipulation is just part of the research job.

The powerfull thing about maths is that formal manipulation has allowed humans to go further "for free": you just need to understand the foundations, and the formal system allows you to compute new results for free without needing to reunderstand them.

I am really curious how far you went in math, because you seem incredibly ill-informed.

It is certainly a 'unique' perspective.

Reading very charitably: you can say that at the moment a lot of the AI's advantages seem to come from: (a) having read approximately everything, and (b) being willing and able to try out lots and lots of approaches without tiring or getting bored. You don't need to have superhuman intelligence, yet, when superhuman persistence still yields so much low hanging fruit.

It's not unique. I for one agree. Mathematics is obfuscated because mathematicians prioritize compactness on the page over ease of understanding. This results in confusing notation (single-character variable names, implicit multiplication, implicit parentheses) and large numbers of omitted steps.

If I want to understand some mathematics, my first step is always translating it to code. Modern code (excluding array languages) no longer has a culture of minimizing character count, and omitting "obvious" steps is not possible. LLMs are based on an architecture (transformers) that was originally designed for natural language translation, so it doesn't surprise me that they're good at this.

The concise notation and omitted steps are to increase legibility. You are focused on things that the author is intentionally telling you are not important, and you are likely missing the things they're trying to say (e.g. the "shape" of an expression vs the names/super concrete meanings of variables). One of the challenges with Lean is that it requires a lot more effort to write things in a way that communicates what you're actually trying to say.

You need to think of mathematical writing as being both symbols/words and also a picture. You're meant to see patterns in what is in front of you. The short names are necessary for the picture. Without them you can't see it. It's like you've zoomed into the individual pixels; the information is all there but you'll never make sense of it that way. You're meant to read the "zoomed out" view where you have short placeholders as names.

And anyone who's tried to write or read Lean will also tell you that understanding a complicated mathematical proof doesn't necessarily get any easier when it's completely formalised.

Had the same problem with browser extension for a while. I made Explayn because of it: a browser extension that explains any highlighted word, sentence, or formula in place, so readers can understand content without leaving the page. https://chromewebstore.google.com/detail/enjakhegoldmloghmce... Figured it might save you some time.

yes, I couldn't agree more, if like to add that "the industry" drove programming and maths apart:

computer science, or "Informatik/informatique" how some Europeans call it, was a branch of mathematics, and "the industry" pushed _very_ hard to get it "practical", make colleges and universities produce programmers, not computer scientists.

so they removed all "challenging" maths requirements from the curriculum, and you can graduate with much less formal rigour, and certainly without being a matematician.

that's also how python replaced scheme as a first teaching language.

> that's also how python replaced scheme as a first teaching language.

Not so fast. There were plenty more horses in that race.

You can easily make an argument that Python is a 'worse' language than Scheme as a first teaching language (though not necessarily one I would subscribe to: they are both dynamically typed and mostly differ in syntax). But Python (and Scheme and even Basic) are a lot better than starting people off with C or Java, or, God forbid, C++.

Obviously there are people who you can lock in a dimly lit closet with just an outdated reference manual to a made up machine and they'll can't help but pick up programming; and those won't have much trouble coping with Java or C++. But those who actually need to be taught will be better off with Python (and Scheme).

This is a good thing, it was just implemented the wrong way. Should have split the degree into separate engineering and theoretical tracks with different names (CS and CE/SE). Today we get weird hybrids where the same degree is math focused in one school and more practical in another.

There is space for both but in the real world we need more engineers who know how to build systems properly than theorists who are great at formal reasoning. It's like structural engineering and physics.

While I think there is some truth to this I think the framing is very uncharitable. The obscurity in maths comes from layers upon layers of abstraction because this is a useful way for humans to work with these complex ideas. I think we see some of this with these proofs that have been translated to lean: some of the proofs are millions of lines of lean, imagine trying to wrap your head around a codebase that is millions of lines! And just for a single proof! These impenetrable abstractions that mathematicians have created are like a mental model for a massive code base.

Reply on news.ycombinator.com