jonlong

No, OpenAI did not solve the "wrong" Navier-Stokes problem. OpenAI did not solve the hardest version of the problem (unforced blow-up), but did give a solution to the Clay Millennium Prize Problem as written and understood, choosing the explicitly allowed forced option.

SciAm writes "in a sense, the LLM found and exploited a loophole in the framing of the question". This is pure sensationalism. Choosing option (C) (out of an explicit list of four options) is neither a "loophole" nor something "found by the LLM"; everyone involved knew this was the option they were pursuing.

With the grumbling out the way, there is some actual scientific content to the article: there's a strong argument that OpenAI's method will not extend to the unforced case, leaving our understanding of NS incomplete. This negative result is itself new and interesting (and predicated entirely on the solution found by OpenAI)!

What I would add here is that the property of left-cancellation is exactly equivalent to injectivity, i.e., f : A -> B is injective iff, for any g, h : C -> A, f o g = f o h implies g = h. If A = {} then f is injective and left-cancellative, both vacuously.

The subtlety is now that left-cancellativity is not equivalent to having a left inverse, for exactly the reason pointed out.

The value of this observation is that left-cancellativity is a useful generalization of injectivity that works in any category, where left-cancellative morphisms are called monomorphisms. If you already know about monomorphisms, it's easier to notice that there's something "off" about D&F's exercise!

It's important to know that (in the usual setting of analysis) not every function is everywhere (or even anywhere) differentiable, but this is more orthogonal to the author's point than opposed to it. A square wave is piecewise differentiable and you can compute a piecewise derivative. The Weierstrass function is defined by an infinite series, and you can compute its derivative term-by-term by the usual rules and check that the result does not converge; it is indeed straightforward to calculate its nonexistent derivative, and this is what Weierstrass did!

In general, to even ask what it means to compute a derivative we need to specify some input language which describes functions in finite terms; we are necessarily in the world of constructions rather than (say) arbitrary set-theoretical maps between infinite sets. With this in mind, the claim that differentiation is always a straightforward computation is a strong one.

Fwiw, you can use the "Modern English" language setting to banish the long s. Reproducing Byrne's original typography is a stated goal of the author. (You can certainly debate the value of that goal.)

The etymology and physical metaphor of "The Singularity" are a bit confused here, and I think it muddles the overall point.

> the singularity is a term borrowed from physics to describe a cataclysmic threshold in a black hole

In his article which popularized the idea of The Singularity, Vinge quotes Ulam paraphrasing von Neumann, and states, "Von Neumann even uses the term singularity". As von Neumann surely knew, "singularity" was a term widely used in mathematics well before the idea of black holes (etymonline dates first use to 1893). Vinge does not say anything about black holes.

> an object is pulled into the center [of] gravity of a black hole [until] it passes a point beyond which nothing about it, including information, can escape. [...] This disruption on the way to infinity is called a singular event – a singularity.

The point at which "nothing" can escape a black hole is the event horizon, not the singularity. What exactly happens to information and what exactly happens when crossing the event horizon are subjects of debate (see "black hole information paradox" and "AMPS/firewall paradox"); however, it's probably fair to say that the most orthodox/consensus views are that information is conserved through black-hole evaporation and that nothing dramatic happens to an observer passing through the event horizon.

> the singularity became a black hole, an impenetrable veil hiding our future from us. Ray Kurzweil, a legendary inventor and computer scientist, seized on this metaphor

While I'm not prepared to go into my personal views in this comment, it's worth noting that the idea that "exponential curves look the same from every point" is not foreign to, e.g., the Kurzweilian view of The Singularity; nevertheless, fitting dramatic, industrial-revolution-sized progress into the fixed scale of a (contemporary) human lifetime would surely be a big deal. This idea, (whether you believe it will happen or not), is obscured by the spurious black hole metaphor.

I suppose I erroneously assumed some familiarity with the correspondence between product types (i.e., types of pairs) and the constructive logical interpretation of "and".

Suffice it to say for now: there is an interpretation of logic that gives a tighter correspondence to programming than the set-theoretic one, under the name "Curry-Howard" or "propositions as types, proofs as programs", and which has been known and cherished by logicians, programming language theorists, and also category theorists for a long time. The logic is constructive as it must be: a program of type A tells us how to build a value of type A, a proof of proposition A tells us how to construct evidence for A. From here we get things like "a proof of A and B is a proof of A together with a proof of B" (the "BHK interpretation"), which connects "and" to product types...

I spoke up because I could not leave untouched the idea that "tagged unions are illogical". On the contrary, tagged unions (aka "disjoint unions", "sum types", "coproducts", etc.) arise forthwith from an interpretation of logic that is not the set-theoretical one, but is a more fruitful one from which programming language theory begins. You are not wrong that there is also a correspondence between (untagged) union and intersection types and a set-theoretical interpretation of propositional logic, and that union and intersection types can also be used in programming, but you are missing a much bigger and very beautiful picture (which you will find described in most any introductory course or text on PL theory).

Well, I have outlined the usual story of logic as it corresponds to programming (as has been accepted for at least some five decades now); it strains credulity to claim that logic is illogical.

Now I do see where you are coming from; under a set-theoretic interpretation with "implies" as "subset", "or" as "union", and "and" as "intersection", the fact that "A implies (A or B)" tells us that an element of the set A is also an element of the set "A union B".

However, this is not the interpretation that leads to a straightforward correspondence between logic and programming. For example, we would like "A and B" to correspond to the type of pairs of elements of A with elements of B, which is not at all the set-theoretic intersection. And while "(A and B) implies A", we do not want to say a value of type "(A, B)" also has type "A". (E.g., if a function expects an "A" and receives an "(A, A)", we are at an impasse.)

So "implies" should not be read programmatically as a subtyping relation; instead, "A implies B" tells us that there is a function taking a value of type A to a value of type B. In the case of "A implies (A or B)", that function takes its input and tags it as belonging to the left disjunct!

Another perspective I must mention: given a proof of "A or B" and another of "(A or B) implies C", how can we combine these into a simpler proof of just "C"? A proof of "(A or B) implies C" must contain both a proof a "A implies C" and a proof of "B implies C", and we could insert into one those proofs a proof of A or a proof of B. But we have to know which one we have! (This is a very short gloss of a much deeper story, where, under Curry-Howard, proof simplification corresponds to computation, and this is another way of describing a function call that does a case-analysis of a tagged union (or "sum type").)

Now "union and intersection" types with the set-theoretic properties you are hinting at have indeed been studied (see, for example, Section 15.7 of Pierce's "Types and Programming Languages"). But they do not replace the much more familiar "sum and product types", and do not play the central role of "or" and "and" in the correspondence of programming to logic.

While others have addressed the programming case for tagged unions, I want to add that, to a logician, tagged unions are the natural construct corresponding to "logical or".

In intuitionistic logic (which is the most basic kind from which to view the Curry-Howard or "propositions-as-types" correspondence), a proof of "A or B" is exactly a choice of "left" or "right" disjunct together with a corresponding proof of either A or B. The "choice tag" is part of the "constructive data" telling us how to build our proof of "A or B". Translated back into the language of code, the type "A | B" would be exactly a tagged union.

For late arrivals to this thread: note that the illustration being discussed has been updated (see the Wayback Machine for the old version). The new version probably still does not show the best second-order approximations, but the obvious qualitative errors have been corrected.

> They likely misjudged the plane due to assuming it was a large jet but it was a regional jet

Maybe this is possible, but it seems implausible given that ATC explicitly refers to the jet as a "CRJ".