UncombedCoconut

Joined 12 years ago

Karma

Submissions

Member since

May 11

Recent submissions

Sadly, we can't, for such a test would already be enough to solve the halting problem: if a TM's status is provable, enumerate possible proofs (of halting and non-halting) until we find one and know the result; if the status is not provable, then the machine certainly cannot halt.

Comment · 2 years ago

Mostly no: we did find some non-halting TMs that required new proofs, but none of those had the flavor of new math, per se. Indeed, we found that all but 30 of them could be proved by finite automata methods, meaning the TM's state/tape at any step could be reduced to one of finitely many states and we'd still know all we needed to know about future steps. I would argue that such a non-halting proof can't have much mathematical content. (Maybe a bit, in about the same way that an integer equation is sometimes proved unsolvable by considering it modulo n and checking every case.) Also, I learned some math I wasn't personally familiar with from the analysis of a particular machine: https://www.sligocki.com/2023/03/14/skelet-10.html (Zeckendorf's Theorem).

Comment · 2 years ago

As a member of these chats: it's often like hitting on an idea on a break-room blackboard and working it out, except the interaction can be cited. That's a positive change, if we can follow through and add to the literature in due time. Here's hoping.

Comment · 3 years ago

This program is at least related to what you want: https://googology.fandom.com/wiki/Hypercalc -- and the community there has devised other systems for representing huge numbers with compact notations.

Comment · 3 years ago

Great news: this article does discuss it. It links to that exact Science paper.

Comment · 4 years ago

FWIW: A pattern along these lines is in B of A's Quartz, allowing the construction of table filters like "Where('colname') <<inlist>> ['cat', 'dog']".

Comment · 4 years ago

https://stopncii.org/how-it-works/ explains that "Your content will not be uploaded, it will remain on your device", and "Participating companies will look for matches to the hash and remove any matches within their system(s) if it violates their intimate image abuse policy."

In principle, both promises can be kept, with humans checking the matches (if any) against their rules. (In practice, I have no idea how it will work out.)

Comment · 4 years ago

Hello, see here for an explanation: https://en.wikipedia.org/wiki/Pearson_correlation_coefficien... It's widely understood that the words "correlation" and "uncorrelated", when used in the context of statistics and not otherwise qualified, are shorthand for this definition in particular. By "otherwise qualified" I mean, for example, saying "Spearman's correlation" (in in the OP's abstract) to specify this one: https://en.wikipedia.org/wiki/Spearman%27s_rank_correlation_...

Comment · 6 years ago

Display Options, [ ] Rotate globe

Comment · 10 years ago

To your first point: yeah, some discomfort around it is valid, but I see it as a non-issue. Informally/philosophically, because a model's job is to capture everything a first-order theory can see about your object of study - so it's fine for (say) an "actually" countable set to model the reals, and not be up to the task of "actually being" the reals. Formally, you differentiate between internal and external statements and don't expect them to be the same (a rigorous version of my pretentious use of scare quotes above :).

Comment · 10 years ago

You can, as long as your first-order statement is in the language of set theory, by translating "there does not exist a bijective function f: N->R".

Comment · 11 years ago

I love it! Quick idea -- though I'm not sure if this would further the goal of having fun, even as a PR -- there's a documented way to make Birdseed subclass random.Random (https://hg.python.org/cpython/file/2.7/Lib/random.py#l72) and inherit the familiar interface and fancy methods.

Comment · 11 years ago

I think you're misunderstanding the example.

An anti-derivative of 1/x is ln |x| (very different from |ln x|) when the domain excludes x=0. By the fundamental theorem of calculus, you can use it to integrate over intervals that exclude x=0. (On positive-real intervals F(x)=ln(x) works, and on negative-real intervals F(x)=ln(-x) works. In either case, F(x)=ln|x| is an equivalent formula. If you try a domain that includes x=0, you risk not just a problem with technicalities but also the practical problem that F(x)=ln|x| and G(x)=ln|x|+sgn(x) look no different...)