Those who haven't read Mythical Man Month are doomed to repeat it. I don't recall anywhere in the book where it states that the problems described in its essays don't apply to you if you're working with dozens of the most intelligent engineers in the world who can produce code in hours instead of days.
I was discussing this with someone else and used the analogy of nuclear energy. Although nuclear plants are highly complex and use forces that have only been understood for the last hundred years, at the end of the day it's still boiling water to create steam to spin a turbine, and nothing about nuclear innovation can engineer away the laws of thermodynamics.
Agents have and will continue to drastically change how we develop code, but it's my belief that drastically changing our software practices to speed up development just means we're going to hit engineering limits faster, rather than being able to overcome those limits entirely.
I was telling a friend something similar last week.
Unless, or perhaps until, we figure out how to use LLMs effectively at the organization level we're still going to be limited to the "slime mold" level of organizational intelligence.
Will that happen? Most likely, but will it take a generation or ten? I suspect it'll be far harder for society to adapt at that level. We've had Mythical Man Month for decades yet software managers continue repeating the same mistakes.
Because of that the idea of OAI and Anthropic just moving to in-house product development makes sense.
And the response back will be "If you could've asked the AI, why did you ask me then?"
In some cases, it may even be the appropriate response. Interrupting somebody to ask something that could be cleared up by an AI is in the same ballpark as asking them something that could be cleared up if you read the docs.
> By now the code of frontier models works well, and the need to read it is gone.
Like anything else, it depends on what you're working on. For small personal projects I agree, but in maintaining large scale business applications with millions of lines of code, I am still having to guide the models to reuse existing code and to be more flexible with their data structures to accommodate changing business requirements in the future.
They only see a snapshot of the world the application exists in due to their ephemeral nature, and until that is overcome, they will only be able to learn general principles and not the particular nuances of your codebase that only arise from observing how the users use it on a daily basis.
Not a comment on this link in particular, but just a general observation from my experience.
One should be skeptical of the demos they initially see at model release, as there have been instances of some being called out as AI generated video or work that took days and millions of tokens and not a one shot as claimed.
The first few days Astra was out, I attempted to reproduce a few of the demos I saw on twitter, and it was clear Astra had a distinctive style and certain limitations when working in short sessions with tools like Blender that could distinguish genuine demos from bs for retweets.
People putting out these demos should share their sessions to really show what was going on, and I invite people to test models and try to replicate what they see and draw their own conclusions.
The circumstances under which they were able to get the synthesized DNA this way would not work in the general case [1]
>Multiple IGSC member companies detected the ordered sequence and determined the order to be legitimate as defined in the 2023 guidance. Specifically, the orders were placed on behalf of SecureBio, an organization known to IGSC member companies given the role played by SecureBio in the SecureDNA project, an effort to build a DNA synthesis screening system. In addition, the name on the orders was an individual who has co-published multiple times with Esvelt, an individual well known to IGSC companies to work in viral evolution and who is known to have access to laboratory facilities sufficient to work safely with the ordered material.
>In short, the system worked as designed: a legitimate individual ordered DNA sequence that, by itself, posed no risk of misuse, for delivery to a company associated with legitimate scientific contributions directly relevant to the sequence that was ordered.
This is going around due to rumors and baseless speculation on Twitter [1] right now that Anthropic has solved the Millennium problem related to Navier-Stokes [2]
This is a step beyond baseless predictions. Tao also had a "weird" "hypothetical" comment about LLMs solving complex proofs with impossible to human verify Lean.
There are theorems like that now, like de Grey's lower bound for the Hadwiger-Nelson (unit distance graph) problem. He used a SAT solver to check that a certain graph with 1581(?) vertices is not 4-colorable. There's no way for a human to check that.
Even simpler, imagine Anthropic announces Goldbach's conjecture is false and they have a billion digit counterexample. Anyone can download it (300MB compressed), but how do you check it?
Doron Zeilberger for decades has expected incomprehensible computer proofs to eventually take over mathematics.
Lol as far as I know that post was the origin of that claim and it's clearly just a guy predicting something that will happen in the future with no information about it.
Yeah, can't read anything on xitter due to the gigantic dickover they put over the content when you don't have an account. A screenshot would've been more helpful than an xitter link.
Why would they send it out for "expert review"? Every time, they have just made the AI generate a Lean proof. In fact, it seems like the most plausible direction to NS is computationally assisted detection of a blowup solution, which has fantastic automatic validation.
The surface of bugs in Lean is infinitely smaller than the human error involeved in a committee of peer reviewers. It's way more probable to say "it's proven because Lean says so" than "it's proven because a couple of reviewers said so".
Also, if a bug is found, all previosuly proven theorems can be reproven to immediately and conclusively find out if things went wrong somewhere
As the recent "proof" of the Collatz conjecture shows, that's not enough in an adversarial context. Human mathematicians don't submit proofs that take advantage of soundness bugs in Lean. AIs do.
Exactly, and the advantage is that checking that the problem is "formalized" here is essentially isolated to verifying that the final theorem statement matches the claim. If there are no 'sorry's and the program compiles, then it has been proven. That's the point of Lean.
Each word of your answer is carefully chosen. I'll add one sentence though: you let time do its job.
Of course there may be errors in lean, of course AI can take advantage of it, of course "carefully" is full of errors. So the only thing left is waiting to see if the result holds. And yes, it may take 30 years...
For a second I thought they were aiming the scary proof machine at us mortals doing PDE stuff. Fortunately the speculation is just that they happen to be aiming it at a nearby mathematician type problem. Phew.
None really. It just says if the NS equations are realistic and can really model real physics or there exist some solutions that make it blow up (infinite energy). But even if that would exist (a solution that blows up) it doesn't mean it doesn't work for 99,999999% of the stuff we're interested in.
The question is basically a pure math question about PDEs.
Maximally, a closed form solution would remove the need for Computational Fluid Dynamics. Any property could be derived from a (presumably expensive) analytic function.
Minimally. It could say that no such analytic function can ever exist. Which would be rather boring.
Turbulent fluids look awfully predictable with their spirals….
That would be surprising IMO. We have closed form solutions to Newton’s Laws plus gravity (albeit not very many of them), we have several closed form solutions to Einstein’s equation in GR, and we have a whole lot of closed form solutions to Maxwell’s equations. But we still use numerical methods to solve interesting problems in all of these fields.
Honestly, for practical engineering purposes not that much. The Navier-Stokes equations are an approximation for a mathematically ideal in-compressible fluid. Even ignoring compressibility, physical fluids in the real world are not continuous fields since they are composed of discrete molecules. However, for that small class of problems where an analytic solution can be found, then it means you can be confident in the answer (it won't blow up to infinity), and that there are no other alternate solutions to the same problem.
I have visual aphantasia but not aphantasia of any other senses, so I can assure you it's not a semantic misunderstanding. I play piano and can hear tunes in my head and use what I hear to play it out on the piano, like playing by ear but without actual sound. And I simply don't have this same ability with visualization.
However, I do visualize in my dreams, so from my own experience, I suspect that aphantasia is not a complete inability to visualize, but rather an inability to visualize intentionally. When I'm very sleep deprived or on psychedelics, my ability to conjure mental images changes, not necessarily to full visualization, but at higher levels than in normal life.
You have to pay to read the rest of the article, which says:
>In August 2024, the town of Cedar Grove held a routine city council meeting. There, they discussed raises for their crossing guards and the purchase of a new truck for the local waterworks.
>The last item on the agenda was whether to accept a donation of new automatic license plate reader (ALPR) cameras for the town’s police department.
>“We’ve received a generous donation of new ALPR cameras … a very generous donation that the police department is receiving,” the town’s manager said. “These are very heavily used tools in the law enforcement toolkit, so it’s good to add more to our belt.”
>The total monetary value of the donation was $37,004. In the approved resolution, the town detailed its provenance: an LLC based out of Encinitas, California.
>It just so happens to be the same LLC that property records list as the owner of a $9.5 million mansion in the town.
>The address for the LLC is also used for a number of other businesses, investment ventures, and a charity. All of which have the exact same manager.
I was discussing this with someone else and used the analogy of nuclear energy. Although nuclear plants are highly complex and use forces that have only been understood for the last hundred years, at the end of the day it's still boiling water to create steam to spin a turbine, and nothing about nuclear innovation can engineer away the laws of thermodynamics.
Agents have and will continue to drastically change how we develop code, but it's my belief that drastically changing our software practices to speed up development just means we're going to hit engineering limits faster, rather than being able to overcome those limits entirely.