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

331–340 of 527 posts

Re: Terence Tao on O1

#331

Post by nybsjytm »

cma wrote: post #229
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.

Tao says that isn't the case for all of it and that on massive collaborative projects he's done many nonmathemeticians did sections of them. He says someone who understands it well needs to do the initial proof sketch and key parts but that lots of parts of the proof can be worked on by nonmathemeticians.

If Tao says he's interested in something being coded in lean, there are literal teams of people who will throw themselves at him. Those projects are very well organized from the top down by people who know what they're doing, it's no surprise that they are able to create some space for people who don't understand the whole scope.

This is also the case for other top-profile mathematicians like Peter Scholze. Good luck to someone who wants to put chatgpt answers to random hypotheticals into lean to see if they're right, I don't think they'll have so easy a time of it.

Re: Terence Tao on O1

#332

Post by nybsjytm »

JonChesterfield wrote: post #231
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.

The premise is to have the LLM put up something that might be true, then have lean tell you whether it is true. If you trust lean, you don't need to understand the proof yourself to trust it.

The issue is that a hypothetical answer from a LLM is not even remotely easy to directly put into lean. You might ask the LLM to give you an answer together with a lean formalization, but the issue is that this kind of 'autoformalization' is at present not at at all reliable.

Re: Terence Tao on O1

#333

Post by charlieyu1 »

ken47 wrote: post #294
JumpCrisscross wrote: post #246

Earlier quoted context omitted.

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.

The current driving force of AI is the desire to cut costs. Jobs will be cut even if ChatGPT is nowhere near a junior engineer and that's the problem.

Re: Terence Tao on O1

#334

Post by remoroid »

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…

Really? Come on. You think trying to make it solve "niche and complicated issues" for a Brainfuck compiler is reasonable? I can't take this seriously. Do you know what most developer jobs entail?

I never need to type paragraphs to get the output I want. I don't even bother with correct grammar or spelling. If I need code for x crud web app who is going to type it faster, me or the LLM? This is really not hard to understand.

Re: Terence Tao on O1

#335

Post by CJefferson »

wenc wrote: post #327
CJefferson wrote: post #325

Earlier quoted context omitted.

OK, but at that point you've told it basically everything, and this is a really basic book problem! As another example I just gave it a network flow problem, and asked it to convert to maximum flow (I'm using the API, not chatGPT). Despite numerous promptings, it never got it right -- it would not stop putting a limit on the source and sink (usually 1), which mean the flow was always exactly 1, here's the bit of wron…

Sure, but that is nature of LLM prompting. It does take some doing to set up the right guardrails. It's still a good starting point. Also a trick when the LLM fights you: start from scratch, and put guardrails in your initial prompt. LLM prompting is a bit like gradient descent in a bumpy nonconvex landscape with lots of spurious optima and saddle points -- if you constrain it to the right locality, it does a better…

I think this is just a case of different people wanting to work differently (and that's fine).

I can only tell this is wrong because I fully understand it -- and if I fully understand it, why not just write it myself rather than fight against an LLM. If I was trying to solve something I didn't know how to do, then I wouldn't know it was wrong, and where the bug was.

Re: Terence Tao on O1

#336

Post by zeroonetwothree »

JumpCrisscross wrote: post #303
IncreasePosts wrote: post #280

Earlier quoted context omitted.

Before it can replace the brilliant programmer, it needs to be able to replace the mediocre programmer. There is so much programming and other tech/it related work that businesses or people want, but can't justify paying even low tech salaries in America for. So far, there is little chance of a non-technical person developing a technical solution to their problems using AI.

> Before it can replace the brilliant programmer, it needs to be able to replace the mediocre programmer Nope. Compensation is exponential. Being able to replace a top performer with a fee mediocre devs pair coding with an LLM is more than fine for 90% of use cases.

This makes no sense, there are problems that 'brilliant' programmers can solve and no number of mediocre ones ones. Just like you can't substitute Mozart with 100 mediocre composers.

Re: Terence Tao on O1

#337

Post by zeroonetwothree »

energy123 wrote: post #276
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.

The large majority of professional writers and artists produce thankless commodity output for things like TV advertisements, games, SEO content. These jobs should be threatened.

They get paid pretty low wages so it's not even clear that AIs will be cheaper. Consider also that you still need a human to evaluate their output, make adjustments, etc.

Re: Terence Tao on O1

#338

Post by zeroonetwothree »

dartos wrote: post #254
a_wild_dandan wrote: post #232

Earlier quoted context omitted.

My sheer productivity boost from these models is miraculous. It's like upgrading from a text editor to a powerful IDE. I've saved a mountain of hours just by removing tedious time sinks -- one-off language syntax, remembering patterns for some framework, migrating code, etc. And this boost applies to nearly all of my knowledge work. Then I see contrarians claiming that LLMs are literally never useful for anyone, and…

> At this point, such sentiments feel either willfully ignorant, or said in bad faith. I feel exactly the same, but in the opposite direction. As someone who’s been programming for 17 years and working professionally for 10, I’m unable to get any huge productivity boosts from AI tools. They’re better than Google+stack overflow for asking random questions, but in a specific context and they’re good for repetitive, but…

Right, in my experience the time it takes to verify that the code it wrote for you is correct is more than just to write it in the first place. A big exception is if you're working in a new domain (e.g., new language or framework). Then it's obviously much faster, and I do derive value from it. But I don't spend a very large % of my time doing that.

I would speculate it's a productivity boost for programmers specifically working in areas that they are new to (or haven't really mastered yet). One question I have is whether overly relying on LLMs will reduce the ability to master a domain, and thus hurt your long-term skill. It might seem silly, like complaining that no one knows assembly anymore because of compilers, but I think it's different than just another layer of abstraction.

Re: Terence Tao on O1

#339

Post by kevinventullo »

benreesman wrote: post #168

Reading anything Terrence Tao writes is thought provoking and I doubt I’m seeing anything others haven’t. There’s at least a “complexity” if not a “problem” in terms of judging models that to a first approximation have been trained on “everything”. Have people tried putting these things up against serious mathematical problems that are well studied? With or with Lean hinting has anyone gotten like, the Shimura-Taniya…

I believe this is the farthest anyone has gotten: https://deepmind.google/discover/blog/ai-solves-imo-problems...

No FLT yet, but as someone who was initially quite skeptical, I’m starting to be convinced!

Re: Terence Tao on O1

#340

Post by zeroonetwothree »

reverseblade2 wrote: post #108

Here's a little test I try on LLMs. So far only O1 and Microsoft Copilot (bing chat) was able to solve it: Find a, b, c distinct positive integers satisfying a^3 + b^3 = c^4. Hint: try dividing all sides by c^3, then giving values to (a/c) and (b/c).

Any integer that is a sum of 2 cubes produces a solution. Since if x^3 + y^3 = z then we have (xz)^3 + (yz)^3 = z^4. So this doesn't seem super interesting?
Post reply on HN