Modern ascendant calculations are "correct", in the sense that they'll match what you see in the sky. Apps like AstroMatrix work from NASA data.

As you rightly observed, it doesn't make a difference when it comes to foretelling the future. But it does make a difference if your aim is to make money selling it. The big spenders on these applications often care a great deal about getting the particulars just so.

The average Visual Basic programmer and the world's best mathematician are going to be about equally good at writing the fortune-telling part, but the mathematician will have a much easier time getting the factual part right.

You won't (write software to) do that without knowing a whole bunch of linear algebra and ODEs.

The fortune-telling part is not what needs the math degree.

The "whale" users who account for a disproportionately large percentage of an astrologer's revenue tend to know the factual information surrounding their birth fairly well. An app/astrologer who doesn't get these facts right, even for a handful of clients, will get a bad reputation fairly quickly.

I reckon the same principle would hold in cultural bubbles where reading tea leaves is a customary means of divination. If the client recognizes recognize black tea, but the fortuneteller insists it is rooibos, there won't be much trust in the rest of the prophecy.

Advertising that the horoscope shop uses Haskell is actually a solid business idea. It pre-filters for the sort of dev who will be able to do the math.

Fwiw, I am in full agreement, and it's commendable when people do have at least a basic understanding of intuitionistic logic.

My remark was simply that the majority in the field don't make this (barely 16 years old) distinction between "proof of negation" and "proof by contradiction", and it has come to be associated with a more introductory or superficial understanding. This is not to suggest that everyone who uses Bauer's terms has a superficial understanding, e.g. Bauer and Escardo are top tier and certainly use it a lot.

I also don't say that this distinction is unique to Bauer. I'm saying he invented and popularized it (I was in fact there in the 2010 thread where it was invented).

With that out of the way:

> It's simply a way to square two widely-held beliefs, even amongst professional mathematicians [...] > > I assume you would prefer to correct the first "misconception", by clarifying that only proofs of positive statements that assume the negative are non-constructive.

Well, yes, one should correct the first widely held belief, because it is a baseless misconception (or rather, was a baseless misconception under the reading of everyone before 2010).

There is no necessity to divide it into “two kinds,” or to speak of positive and negative statements though. If one assumes not-X and thereby arrives at a contradiction, then one has indeed established that not-X is not the case. This works the same way in both classical and intuitionistic logic, in both classical and constructive mathematics.

If you have some way of going from not-not-X to X, then you also proved X. The difference between classical logic and intuitionistic logic is that the latter does not admit any general way of going from not-not-X to X.

This is what's actually going on, and it's entirely orthogonal to proofs by contradictions. Redefining "proof by contradiction" to make a common misconception come out right does not help communicate this in any way, since the end of a proof by contradiction is not the only place where double negations are eliminated in classical mathematics.

If anything, it obscures what is going on: mathematicians usually come away with more misconceptions, like "in constructive mathematics you are not allowed to assume a negative". And it makes it a fair bit harder for constructive mathematicians to converse clearly with the rest of the mathematical world.

Indeed, long before 2010, they already had perfectly serviceable language for this sort of thing: they said "this proof uses DNE". They do not need a separate, additional term for "this proof of this particular form uses DNE at a very specific place".

> One may scoff at these questions (and many of my colleagues do) but I have personally found them helpful to think about, and also relevant now that logic-based computer proof systems are becoming more important to mathematicians.

Bridges, cited above, coauthored with Bishop the main monograph on constructive analysis. Birkedal, for his part, might fairly be said to have done as much as anyone to shape what we now call modern realizability.

They don't scoff at these questions, they take them rather seriously. Yet like almost all mathematicians AND most other logicians, they chose not to use Bauer's terminology.

> Would you care to enlighten us about any of the subtleties of intuitionistic logic that make this a shibboleth?

It's something of a shibboleth because it reveals the speaker first encountered the field through pop literature like blog posts (there is nothing wrong with that), and has not then spent sufficient time with the primary literature to realize that this is not, in fact, customary terminology used by most of those who work in the discipline proper. So it marks the speaker as somebody likely to have somewhat superficial knowledge of the field.

Most mathematicians have never heard of it. Those who have tend to scoff, even in CS and constructive mathematics, and call any proof that "supposes for a contradiction that X" a proof by contradiction.

Take a look at Douglas Bridges calling the sqrt 2 proof a standard proof by contradiction [1], or Lars Birkedal in the proof of Lemma 6.6 here [2].

Bauer is a very productive mathematician who maintains a well-read blog, and it was through that blog that the phrase began to circulate, eventually becoming something of a shibboleth, signaling, perhaps a rather superficial acquaintance with the subtleties of intuitionistic logic.

[1] https://www.dsbridges.com/myths-about-constructive-mathemati...

[2] https://cs.au.dk/~birke/papers/locrcg.pdf

But they need to improve their humanizer dataset. Right now, most models can be given system prompts which cause them to emit text classified as 100% human. It looks like their automated humanizers do worse than these system prompts. Or (alarming if so) they chose not to include ones that would make their product look unreliable.

If I got you to be skeptical of AI takes, though, mission accomplished. Exercise your skepticism especially when the takes come from somebody who is trying to sell something.

It claims to be an evidence-based investigation, but basically invents the contents of the documents they supposedly investigated, such as the Anthropic Frontier Red Team writeup, from whole cloth.

I don't think deeper engagement with it would promote good discussion.

Anthropic tries to create marketing hype around Mythos using two psychological tricks.

1. Put large numbers in the headlines.

"Mythos discovered 271 vulnerabilities in Firefox" makes the model seem extremely capable to the uninitiated.

But it's actually meaningless as a measure of capability _improvement_.

Anthropic gave away $100mil specifically as Mythos credits to these projects and companies (that's $2.5mil per project). Spending the same exorbitant amount of compute analyzing the same codebases in an older model like GPT 5.x Pro would have turned up 260 of these vulnerabilities, or could even have turned up more than 271 ones.

No need to speculate, since this is exactly what we saw in the few code bases where we have such comparisons (like in the curl codebase). Supposedly weaker models, working with a much lower budget, turned up dozens of vulnerabilities. Mythos turned up only one, which ended up as a low severity CVE.

2. Do the whole "too dangerous to release" shtick. This is one of Dario Amodei's favorite moves. When he was vice president of research at OpenAI, he declared GPT-3 (which wasn't able to produce coherent text beyond 3-4 sentences at the time) too dangerous [1] as well.

Long story short, it's the ChatGPT 4.5 situation again: a company trained a model that's too slow and expensive, but not much more capable than what came before. It therefore requires these marketing stunts.

[1] https://www.itpro.com/technology/artificial-intelligence-ai/...

You can find thousands of such questions on Math StackExchange. Take e.g. [1]: never been asked anywhere else, interesting enough, yet answered pretty much immediately by two separate mathematicians.

"Is there a single constant and function with connected domain that can express all of $\log, \exp, \sin, \dots$?" would have made a fine question there too, the type that gets a thorough answer very quickly if anyone bothers to ask it.

> the burden of proof should not lay with the reader

You were the one who made the claim that "this is one of the most significant discoveries in years". Feel free to substantiate that claim first, according to the same standards. Are there any authors who ask this question, and/or suggest that they don't know an answer?

[1] https://math.stackexchange.com/questions/2308587/is-the-set-...

These classes can always safely include all single-valued continuous functions (you cannot even write the _quadratic_ formula in terms of arithmetic and single-valued continuous functions!), but also plenty of non-single-valued functions (e.g. the +-sqrt function which appears in the well-known quadratic formula).

Applying Arnold's proof to the class given by arithmetic and all complex nth root functions (also multivalued) gives the usual Abel-Ruffini theorem. But Arnold's proof applies to the class "all elm-expressible functions" without modification.

Some of my favorites:

DoctorOetker: "I'm still reading this, but if this checks out, this is one of the most significant discoveries in years."

cryptonektor: "Given this amazing work, an efficient EML operator HW implementation could revolutionize a bunch of things."

zephen: "This is about continuous math, not ones and zeroes. Assuming peer review proves it out, this is outstanding."

[1] https://news.ycombinator.com/item?id=47746610

[2] https://www.reddit.com/r/math/comments/1sk63n5/all_elementar...

Neither the present article, nor the original one has much mathematical originality, though: Odrzywolek's result is immediately obvious, while this blog post is a rehash of Arnold's proof of the unsolvability of the quintic.

Yes, and that would be relevant if this was a verified software system. But it wasn't: the system consisted of a verified X and unverified Y, and there were issues in the unverified Y.

The article explicitly acknowledges this: "The two bugs that were found both sat outside the boundary of what the proofs cover."

Anti-griefing works by keeping the barriers to entry very high, so chances are you won't try VATSIM, even though MSFS is technically available on Steam.

[1] https://vatsim.net/docs/basics/becoming-a-controller