I really like Julia, but I wind up not using it as much as I might otherwise because the startup time kills it for many use cases (though of course it's easily amortized in others).
When I was a lad we walked out to the car and did that with the key. In the snow. It wasn't that bad and, despite what you may have heard, was not in fact uphill both ways.
LLMs write like some people cook, adding bespoke artisanal Belgian sea salt, truffle oil and weirdly specific cheese without any thought given to how the result will taste.
It would have been interesting to try something closer to the movie poster example; say have the AI rewrite the passage with the room toggling between the initial light-mode decor and a dark-mode decor, then back, repeatedly. Or even change the woman's name to "Mrs. Smythe" and back.
As the article explains: “[…] In other words, if you instruct a model to change a single word in a paragraph of text, it can almost always handle the task with no collateral damage.“
Right, but if you ask it to make a systematic change (the room decor for light to dark and back) or something with subtle implications that would require other changes to fit in?
Changing the title in the movie example is this sort of change; the "change a single word" isn't analogous.
The point was that a textbook (where the 40hr/page estimate comes from) is cumulative/linear -- what you need for page n was defined / established on the preceding pages. But in a proof such as this you can call on any other published result (and those can do the same) so the dependency graph is (potentially) much bushier. Thus later pages of the proof should take far more than 40 hours to manually formalize.
The point of these problems is the understanding / tooling gained in solving them. We're getting none of that. At best they are like a modern oracles, correctly answering your questions in a way that's doesn't help you any. (At worst,...)
"an LLM AI [company] just [claimed that a team of mathematicians they hired, using their AI] [may have] solved [part of] Navier Stokes[, definitely prompted by (and possibly by looking at) the work of human mathematicians."
reply