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.
My memories of theoretical computer science are quite rusty, but I seem to see an issue with your argument: if you need enumeration you meet semidecidability. In other words, if you start generating the proofs and you find the one you were looking for, then problem solved. But if you can't find the proof, you would need to keep generating them at infinity to find the one you need. You can't conclude the result in this way without enumerating all possible proofs. Unless, you have a way of limiting the number of proofs that need to be generated?
You are bounded by the fact that the statement is provable. Let a statement M be provable with a proof length K. By contradiction, if K is non finite, the statement must not be provable. Thus, there must be some positive integer K s.t. the proof length < K. Thus, it suffices to enumerate all proofs of length < K.
Insofar as we are given provability, we can solve halting.
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).
Tangential, but fun fact about Zeckendorf: In addition to Zeckendorf representation, there's also dual Zeckendorf (sometimes also called lazy Fibonacci), where instead of requiring no two consecutive ones, you require no two consecutive zeroes. (Not counting the implicit zeroes at the big end, of course.) It was surprising to me that this also works, but it does!
Actually, just as you can do bijective base-b [0], you can also do bijective Zeckendorf (using 1 and 2 with no two consecutive 1s). Although, as happens with bijective binary, bijective Zeckendorf is closely tied to ordinary Zeckendorf, so it doesn't offer much new. But bijective dual Zeckendorf doesn't work -- lots of numbers can't be represented!
One more fun fact about Zeckendorf and dual Zeckendorf: Write n>0 in Zeckendorf, and count how many zeroes it ends in. This will be even if the dual Zeckendorf representation of n ends in a 1, and odd if it ends in a 0. Similarly, if you write n in dual Zeckendorf and count how many 1s it ends in, this will be even if the (ordinary) Zeckendorf representation ends in a 0 and odd if it ends in a 1.
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.
That's fine, but the citation shouldn't be in the form of a Discord link, or at least not exclusively in that form. Make a copy of the relevant messages, host them elsewhere, and include that copy in the citation. Discord has been pretty good so far but being a durable archive has never been their core selling point so I don't trust that to continue indefinitely.
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.
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.)
Yup, you got it, the content itself will remain only in the device, the hashing is done in-browser, and the only part of the original content that makes it into the system is the hashes. Once a platform that is part of the program downloads those hashes and is able to match content, you need to apply some amount of verification. It’s on the participating companies themselves to review the content that matches the hash, to see if it actually violates their policies on NCII.
I think that depends on context. Sometimes, in a technical setting correlation just means dependence as an abstract concept, and this includes non-linear dependence. Similar how in financial circles, volatility doesn't mean standard deviation, but in colloquial settings it does.
Correlation, in general, just means some sort of statistical dependence: knowing x tells you something about y. It's often "operationalized" by computing Pearson's r: it's easy to do and there's lots of associated theory.
However, I would find it absolutely bizarre if someone showed a plot with obvious non-linear dependence and described it as "uncorrelated". In that case, the low r reflects a failure of the measuring tool rather than something being measured.
Right, but you can't ensure that the only models of 'bijective functions' are actually bijective functions. To switch to a slightly simpler example, you can translate statements such as "x is finite" into a first order language (for example, set theory), but you can't ensure that x actually is finite in the models of this statement.
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 :).
