scapp

That's a different meaning of the word "undecidable". You're talking about undecidable problems [1]. The meaning in Gödel's incompleteness theorem is different and is a synonym with independent [2].

[1] https://en.wikipedia.org/wiki/Undecidable_problem

[2] https://en.wikipedia.org/wiki/Independence_(mathematical_log...

Hmmm, it could definitely be clearer. It looks like it's using the bulk density for "sugar" (so including the air between the crystals) and the actual density for "sucrose".

It's somewhat a coincidence. In the paper, the dimension has to be larger than this constant K which is shown to be no larger than 1728. This is a fairly crude estimate that comes from multiplying a bunch of small numbers together, so the fact that it ends up being 12³ is not unimaginable. Then taking the dimension to be one larger than this estimate on K, we get 1729 = 12³ + 1³ (= 9³ + 10³).

However, 1728 isn't the minimum possible value for K. With more precise estimates, sketched in the paper, we can bring it down to 8 + ε. So assuming that this finer estimate works, using a 9 dimensional Fourier transform would also make the algorithm be O(n log(n)).

This is the easiest of the paradoxes mentioned in this thread to explain. I want to emphasize that this proof uses the technique of "Assume P, derive contradiction, therefore not P". This kind of proof relies on knowing what the running assumptions are at the time that the contradiction is derived, so I'm going to try to make that explicit.

Here's our first assumption: suppose that there's a set X with the property that for any set Y, Y is a member of X if and only if Y doesn't contain itself as a member. In other words, suppose that the collection of sets that don't contain themselves is a set and call it X.

Here's another assumption: Suppose X contains itself. Then by the premise, X doesn't contain itself, which is contradictory. Since the innermost assumption is that X contains itself, this proves that X doesn't contain itself (under the other assumption).

But if X doesn't contain itself, then by the premise again, X is in X, which is again contradictory. Now the only remaining assumption is that X exists, and so this proves that there cannot be a set with the stated property. In other words, the collection of all sets that don't contain themselves is not a set.

M.A. was the highest degree available in the UK at the time [1]. The closest equivalent to a PhD program might be the Prize Fellowship that Hardy had from 1900 to 1906, though it's certainly not one to one. Don't get the impression that Hardy was done with his education when he got his masters degree.

[1] https://www.economics.soton.ac.uk/staff/aldrich/Doc1.htm

[2] https://royalsocietypublishing.org/doi/10.1098/rsbm.1949.000...

Nothing wrong with starting at 1 for induction, but yes, having an additive monoid is nice (still get a multiplicative monoid with N*)

*Bill Odenkirk. Bob is his brother

Nice! I wondered if someone would beat that TAS level anyway.

It's easy to find the UUID associated to a nickname. For example, here's [0] the one for `accrual`

[0] https://namemc.com/profile/Accrual.1

It's always fun to make fun of cranks. Thanks for linking that. The author really needs to find the right statement of what they call the Nested Interval Theorem. I cracked up at the complete misuse of it in the "Interval Argument for the Rationals" section

Kind of disappointing that it doesn't have the victory screen. But man, my fingers still remember that combo you have to do for those 4 wide areas.

2 line explanation of where e comes from here: to represent a number x in base b, you need roughly log_b(x) digits. If you weight that by the number of different digits in base b, you get b * log_b(x) = b * log(x)/log(b) = b/log(b) * log(x) (where now the log is any base you care to choose).

So assuming x > 1, this is minimized precisely when b/log(b) is minimized. The derivative of b/log(b) is (log(b) - log(e))/log(b)^2, so this is zero when b = e. (The second derivative is 1/(e log(e)) > 0, so this is a minimum).

> Last time I checked there was still no formal version of Cantor's diagonalization argument.

Formalization? Like a computer checked proof?

Lean: https://leanprover-community.github.io/mathlib_docs/logic/fu...

Coq: https://github.com/bmsherman/finite/blob/63706fa4898aa05296c...

Isabelle: https://isabelle.in.tum.de/website-Isabelle2009-2/dist/libra...

Check out the replies to this comment [1] with the same attempted counterexample. Your set isn't union closed because {1}U{2} = {1, 2} isn't in it (same for {1}U{3} etc.).

[1] https://news.ycombinator.com/item?id=34236889#34240381

There's a way to make it always appear above other windows. Let me see if I can find that again...

Ah, it's in the options menu on the task manager itself (alt + O to access the menu without a mouse).

I don't see the problem. For example, if something finishes in 10 minutes, it has 6 completions per hour. If a competitor finishes in 1 minute, it has 60 completions per hour. It both finishes in 1/10 of the time (time per completion) and is 10 times faster (completions in a given amount of time).

If you don't like the unit "completions per hour", consider that you don't have to drive for an hour or even go a mile to go 60 miles per hour.

> along with the other axioms the the theory is derived from

Axioms are trivially provable in any system. Unless you mean prove them without using them, in which case you're actually talking about a system where they aren't axioms.

> the unnameable reals, which are almost every real

Is there a definition you have in mind for "unnameable"? If you mean definable [0][1], then this is independent of ZFC.

The "standard" argument for this is flawed, and indeed there are models where every real is definable. [2]

[0] "x is definable if there exists a first order formula with one free variable P such that x is the unique real number with P(x) true" [1] https://en.wikipedia.org/wiki/Definable_real_number#Definabi... [2] https://mathoverflow.net/questions/44102/is-the-analysis-as-...

It's because the cone cells connected to those variants of colorblindness have very similar sensitivities to wavelengths. Check out this diagram: https://en.wikipedia.org/wiki/Cone_cell#/media/File:Cone-fun...

With protanopia, the L cone cell is affected. For deuteranopia, it's the M cone cell.

Spaces like this (manifolds) are usually classified by which Euclidean space they look like locally. So, for example, the surface of a sphere is two-dimensional since it locally looks like a plane (whence flat-earthers). A two-dimensional torus can be visualized as the surface of a doughnut, but also as a square where going off an edge brings you to the opposite edge.

As explained in the article, the torus in question is locally three-dimensional, and you might mistake it for ordinary 3d space at first. The specific geometry we're visualizing is the 3d analogue of the square from above: it's a cube where going off an face brings you to the opposite face.

Maybe it's changed now, but the "π" in the title is unicode U+03C0 [0], which is a lowercase pi. In the font Verdana (the one that I see in the title, but not this comment as I type it[1]), U+03C0 looks like a small capital pi and looks a bit like "n").[2]

[0] https://www.compart.com/en/unicode/U+03C0

[1] EDIT: once the comment was submitted, the font changed to Verdana.

[2] https://graphicdesign.stackexchange.com/questions/74608/why-...

Does this project still exist somewhere other than Google Code? It seems everything on the website 404s.

EDIT: this might be it: https://github.com/Tipoca/intuitionistic

The better term to use here is Socratic dialogue [0].

[0] https://en.wikipedia.org/wiki/Socratic_dialogue

First, a point of terminology: uncountably infinite refers to any infinite cardinality other than countably infinite, so if the number of probability distributions is at least the cardinality of the real numbers, then it's already uncountable.

As for what uncountable cardinality they form, it's the same as the real numbers [0]. Roughly, a probability distribution is determined by the countable collection of real numbers P(X <= q) with q rational. That means the cardinality is no more than R^Q, which is isomorphic to R. (the cardinality is at least R due to, say, uniform distributions on [0, x] for x real).

[0] https://math.stackexchange.com/questions/3698864/why-does-th...

Wait, is there something wrong with the paper you linked? Theorem 1.1 says

> There is an integer multiplication algorithm achieving M(n) = O(n log n).

You don't call something a theorem if it's a conjecture.

In case anyone's curious, the SCOTUS case was Kirtsaeng v. John Wiley & Sons, Inc.

https://www.scotusblog.com/case-files/cases/kirtsaeng-v-john...

I don't know what proof is used here, but the standard proof uses univalence to upgrade the equivalence (_ + 1): Z -> Z to a path Z = Z. Then we use induction for S^1 to define the map S^1 -> U that takes the base point to Z and the loop to the path Z = Z.

Having the fundamental groupoid of the circle be the integers requires the universe to be a 1-type or higher. There are some type theories that have that without full univalence (e.g. this [0]), but it'll definitely have a HoTT flavor with non-identity paths.

[0] Two-dimensional models of type theory: https://arxiv.org/abs/0808.2122

Lean 3 introduced singleton-elimination which is inconsistent with HoTT. There's a project [0] that uses an attribute to restrict uses of that rule, but it isn't really ergonomic to use.

[0] https://github.com/gebner/hott3

I think they meant

> Thus if you assume that the function is total and thus does halt, it must run in O(1) time.

Since that's what total means.

Problem 1: 1/(2^aleph_0) isn't a real number. The real numbers don't contain infinitesimals. It's possible to formalize a number that behaves like 1/(2^aleph_0) "ought to" (surreals would be one possible approach), but the result won't be a real number.

Problem 2: There's no natural number that maps to (say) 1. Even if you do allow 1/(2^aleph_0), there's no finite number n that would make n/(2^aleph_0) = 1. With any reasonable definitions of the operations involved here, n/(2^aleph_0) would always be infinitesimal, so it would never equal a non-infinitesimal.

Problem 3: You're still skipping over infinitely many numbers. If 1/(2^aleph_0) is a number (and again, this requires going beyond the real numbers) and 1.5 is a number, then 1.5 * 1/(2^aleph_0) = 1.5/(2^aleph_0) is also a number, but no natural number gets mapped to that.