Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

Terence Tao on O1

mathstodon.xyz

Post reply on HN
Print view View original

291–300 of 527 posts

Re: Terence Tao on O1

#291

Post by dartos »

mkarrmann wrote: post #263
dartos wrote: post #249

Earlier quoted context omitted.

No, the first profession AI was on track to decimate was artists, but that didn’t really happen. AI just destroyed shutterstock.

Is most code being written the equivalent of high-art or Shutterstock?

I think most code being written is like a custom car made out of the most cost effective parts available.

Not pretty, but it gets the job done for the specific use cases of a given business.

Real production code doesn’t and have a shutter stock equivalent.

If you think most code is stock, then you just haven’t had enough experience in industry yet.

Re: Terence Tao on O1

#292

Post by roboboffin »

fnordpiglet wrote: post #149

Rewind your mind to 2019 and imagine reading a post that said “The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, graduate student.” With regard to interacting with the equivalent of Alexa. That’s a remarkable difference in 5 years.

[dead]

Re: Terence Tao on O1

#293

Post by williamcotton »

sweeter wrote: post #207
skydhash wrote: post #68

Earlier quoted context omitted.

> Much Much more productive world by just knuckling down and learning how to do the work. The fact everyone that say they've become more productive with LLMs won't say how exactly. I can talk about how VIM have make it more enjoyable to edit code (keybinding and motions), how Emacs is a good environment around text tooling (lisp machine), how I use technical books to further my learning (so many great books out here)…

Or people say "I've been pumping out thousands of lines of perfectly good code by writing paragraphs and paragraphs of text explaining what I want!" its like what are you programming dog? and they will never tell you, and then you look at their github and its like a dead simple starter project. I recently built a Brainfuck compiler and TUI debugger and I tested out a few LLM's just to see if I could get some useful o…

This is almost entirely written by LLMs:

https://github.com/williamcotton/guish

I was the driver. I told it to parse and operate on the AST, to use a plugin pattern to reduce coupling, etc. The machine did the tippy-taps for me and at a much faster rate than I could ever dream of typing!

It’s all in a Claude Project and can easily and reliably create new modules for bash commands because it has the full scope of the system in context and a ginormous amount of bash commands and TypeScript in the training corpus.

Re: Terence Tao on O1

#294

Post by ken47 »

JumpCrisscross wrote: post #246
fnordpiglet wrote: post #149

Rewind your mind to 2019 and imagine reading a post that said “The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, graduate student.” With regard to interacting with the equivalent of Alexa. That’s a remarkable difference in 5 years.

The first profession AI seems on track to decimate is programming. In particular, the brilliant but remote and individual contributor. There is an obvious conflict of interest in this forum.

The conflict of interest might have something to do with the fact that OpenAI's CEO/founder was once a major figure in Y Combinator. But I think you wanted to insinuate that the conflict of interest ran in the other direction.

Once ChatGPT can even come close to replacing a junior engineer, you can retry your claim. The progression of the tech underlying ChatGPT will be sub-linear.

Re: Terence Tao on O1

#295

Post by markusde »

sn9 wrote: post #236
nybsjytm wrote: post #181

Earlier quoted context omitted.

To code proofs in lean, you have to understand the proof very well. It doesn't seem to be very reasonable for someone learning material for the first time.

That's not true at all. You can literally learn how to write proofs using Lean: https://djvelleman.github.io/HTPIwL/

The examples in this book are extraordinarily simple, and covers material that many proof assistants were designed to be extremely good at expressing. I wouldn't be surprised if a LLM could automate the exercises in this book completely.

Writing nontrivial proofs in a theorem prover is a different beast. In my experience (as someone who writes mechanized mathematical proofs for a living) you need to not only know the proof very well beforehand, but you also need to know the design considerations for all of the steps you are going to use beforehand, and you also need to think about all of the ways your proof is going to be used beforehand. Getting these wrong frequently means redoing a ton of work, because design errors in proof systems are subtle and can remain latent for a long time.

Re: Terence Tao on O1

#296

Post by lanstin »

wenc wrote: post #5

Once GPT is tuned more heavily on Lean (proof assistant) -- the way it is on Python -- I expect its usefulness for research level math to increase. I work in a field related to operations research (OR), and ChatGPT 4o has ingested enough of the OR literature that it's able to spit out very useful Mixed Integer Programming (MIP) formulations for many "problem shapes". For instance, I can give it a logic problem like "…

Yeah I have been using them to help with learning graduate maths as a grad student. Claude Sonnet 3.5 was unparalleled and the first quite useful one. GPT4o preview seems about equal (based on cutting and pasting the past six months of prompts into it).

Re: Terence Tao on O1

#297

Post by bamboozled »

fnordpiglet wrote: post #149

Rewind your mind to 2019 and imagine reading a post that said “The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, graduate student.” With regard to interacting with the equivalent of Alexa. That’s a remarkable difference in 5 years.

Remind your mind to 1850, imagine seeing a lightbulb.

Re: Terence Tao on O1

#298

Post by perching_aix »

WhatIsDukkha wrote: post #26
wenc wrote: post #5

Once GPT is tuned more heavily on Lean (proof assistant) -- the way it is on Python -- I expect its usefulness for research level math to increase. I work in a field related to operations research (OR), and ChatGPT 4o has ingested enough of the OR literature that it's able to spit out very useful Mixed Integer Programming (MIP) formulations for many "problem shapes". For instance, I can give it a logic problem like "…

I entirely agree about their utility. HN, and the internet in general, have become just an ocean of reactionary sandbagging and blather about how "useless" LLMs are. Meanwhile, in the real world, I've found that I haven't written a line of code in weeks. Just paragraphs of text that specify what I want and then guidance through and around pitfalls in a simple iterative loop of useful working code. It's entirely a lea…

> HN, and the internet in general, have become just an ocean of reactionary sandbagging and blather about how "useless" LLMs are.

Now imagine how profoundly depressing it is to visit a HN post like this one, and be immediately met with blatant tribalism like this at the very top.

Do you genuinely think that going on a performative tirade like this is what's going to spark a more nuanced conversation? Or would you rather just the common sentiment be the same as yours? How many rounds of intellectual dishonesty do we need to figure this out?

Re: Terence Tao on O1

#299

Post by vessenes »

JumpCrisscross wrote: post #246
fnordpiglet wrote: post #149

Rewind your mind to 2019 and imagine reading a post that said “The experience seemed roughly on par with trying to advise a mediocre, but not completely incompetent, graduate student.” With regard to interacting with the equivalent of Alexa. That’s a remarkable difference in 5 years.

The first profession AI seems on track to decimate is programming. In particular, the brilliant but remote and individual contributor. There is an obvious conflict of interest in this forum.

I see this theory a lot but mostly from people who haven’t tried pair coding with a quality llm. In fact these llms give experienced developers super powers; you can be crazy productive with them.

If you think we are close to the maximum useful software in the world already, then maybe. I do not believe that. Seeing software production and time costs drop one to two orders of magnitude means we will have very different viable software production processes. I don’t believe for a second that it disenfranchises quality thinkers; it empowers them.

Re: Terence Tao on O1

#300

Post by sandspar »

asdasjhG wrote: post #202
teaearlgraycold wrote: post #188

Earlier quoted context omitted.

Or can everyone now lead research projects and build businesses?

No, almost everyone who gets funding for a business already belongs to the monied royalty and gets it either directly from his family, via friends of the family or laundered through a VC. There are exceptions of course, but that's how the bulk of businesses, especially those with stupid ideas are funded. In the latter category success does not even matter, the trust fund baby just has to have the appearance of a lead…

Are you kidding or being serious? Most business owners are just regular people. Have you ever worked in a small business before?
Post reply on HN