QuesnayJr

I don't know how Polymarket works. Were people betting against Polymarket, or was Polymarket just making book and someone else is on the other side of the bets.

It's hard to explain, but immediately clear to enough people that it explains why so many people aren't sad to see SO fall on hard times.

I get that there have to be some rules, but it comes across like you derive some sort of satisfaction in enforcing rules. Successful sites with user moderation start out with a big population of people who will tolerate the rules in order to participate in the goal of the site, but eventually they end up dominated by people who feel that the very act of enforcing rules is an important contribution. All of the talk of "community" comes across as a thinly veiled version of Cartman's "Respect my authority" from South Park.

The tone of this answer explains everything why people fled SO as soon as they possibly could.

I actively hated interacting with the power users on SO, and I feel nothing about an LLM, so it's a definite improvement in QoL for me.

It was sad to read that the store has closed (though they still managed to do some seasonal events with the organ).

There's a couple of problems that were solved that way a while ago, and they have been formalized, but not in Lean:

https://en.wikipedia.org/wiki/Four_color_theorem

https://en.wikipedia.org/wiki/Kepler_conjecture

It's not that obscure, even in the US. Anyone who takes French in US high school has probably read it in French (it's very easy to read), and even in English it's one of the most common classic children's books.

I remember it being for both Unix and DOS.

Thanks for the links. I couldn't quite tell if that was a text game like bsdgames trek, or a curses game like Rogue.

If you like that kind of thing, you might like looking at the Angband Plus github repository: https://github.com/NickMcConnell/AngbandPlus

Angband is a roguelike that had many variants over the years, and Nick combined all of these variants into one big git repository where each variant is a branch.

There was a Curses version of Trek called "universe" that I was obsessed with, back in the day, but I've never been able to find it again.

I found the claim that Peirce rejected bivalent logic strange, simply because he was one of the key figures in actually creating bivalent logic, in his paper "On the Algebra of Logic". He even proposed one of the classic forms of the law of excluded middle known as Peirce's law.

I think you are misjudging which side of the religion/non-religion divide you are on.

The article was interesting, but it convinced me of the opposite of its thesis. The books mentioned are 1) a standard school textbook, 2) a standard book for navigators, and 3) a chart of whale hunting grounds that someone created (that Melville anticipated). It all seems like the kind of books a ship's captain would own.

Still, it was interesting to read about the things themselves. I had no idea that the US Navy put out a mathematics reference book. (It's easy to find online, too. The most recent edition came out in 2021.)

And Kevin Buzzard (who is an established algebraic number theorist) is making the claim that this no longer applies in a world where people are depending on 1000-page proofs that maybe two people have ever checked. In the case of Jim Arthur's work, zero people have checked it, because Arthur hasn't even finished writing it down, yet people are publishing results that depend on it.

There isn't really anything better. The Notices of the AMS has one feature article each issue, but those are sometimes too technical.

Anyway, this article seems fine to me. The "exponentiation" comment seems like a bizarre misreading. The article is just trying to explain how big BB(6) is. Before that, it explains what BB(n) is. To think it's solely about exponentiation you have to skip that entire section.

The specific example of Fermat's Last Theorem is probably true simply because so much work has been done on the modularity of elliptic curves since then, but the probability of false results being proven is much higher than 0%.

In fact, Buzzard has an "existence theorem" of this exact thing. Annals of Mathematics (one of the top mathematics journals) has published one paper proving a theorem, and another paper proving the opposite result of a theorem: https://www.andrew.cmu.edu/user/avigad/meetings/fomm2020/sli...

The Wikipedia article on helium hydride has the most hardcore sentence I've ever seen on the site: "Since HeH+ reacts with every substance, it cannot be stored in any container." It sounds like something out of a comic book.

LLMs understand LaTeX extraordinarily well.

It's striking how complicated quadratic forms are, given how simple they sound. You could probably explain the idea of a quadratic form over a ring to a good high school class, while explaining the proof of the Milnor conjecture would be tough even for graduate students in math.

Seeing the culture of StackOverflow, I would choose to be dead in the ground rather than ask a question there, even a question that can't be easily answered elsewhere. Volunteer-run sites need a mix of enthusiasts who do the real work of the site and janitors who keep things from being too chaotic, but enthusiasm dims while the desire to impose order never does, so eventually the janitors take over.

MathOverflow has a much better culture, so I ask (and answer) questions there. I'm not quite sure why it's worked out better there, though I suppose it's something to do with the population.

Algol 58 had "for i:=0(1)9". C's for loop is a more general variant.

Full $L_2$ also has a countable orthonormal basis. Hermite functions are one example.

The solution to the puzzle is that "the bitter lesson" is about AI software systems, not arbitrary software systems. If you're writing a compiler, you're better off worrying about algorithms, etc. AI problems have an inherent vagueness to them that makes it hard to write explicit rules, and any explicit rules you write will end up being obsolete as soon as we have more compute.

This is all explained in the original essay: http://www.incompleteideas.net/IncIdeas/BitterLesson.html

I'm starting to think that half the commenters here don't actually know what "The Bitter Lesson" is. It's purely a statement about the history of AI research, in a very short essay by Rich Sutton: http://www.incompleteideas.net/IncIdeas/BitterLesson.html It's not some general statement about software engineering for all domains, but a very specific statement about AI applications. It's an observation that the previous generation's careful algorithmic work to solve an AI problem ends up being obsoleted by this generation's brute force approach using more computing power. It's something that's happened over and over again in AI, and has happened several times even since 2019 when Sutton wrote the essay.

This isn't really how it went down, historically. They considered lots of different large cardinals, and then they turned out to be linearly orderable by consistency strength. And then it's natural to wonder if it's a general rule.

I think of the line "I want some answers that Ja Rule might not have right now" pretty often.

I have the exact opposite reaction, that if someone told me the answer is "no" because it requires an unbounded number of coin flips that they were the ones trying to bullshit me. In antic's formulation, nothing is said about requiring a bounded number of flips.

This is the coolest thing I've seen in years.

It preserves angles, which is what makes it useful in navigation. Mercator is bad at relative sizes for places far apart, but when you look at a small patch shapes are less distorted. For that reason, online maps use a version of Mercator.

I think they're imitating Eliza.