housecarpenter

I don't know much about this controversy, but looking at the Wikipedia page for the Four Color Theorem, it looks like since the initial Appel-Haken result, mathematicians have continued to work on the Four Color Theorem to try to find a simpler proof. So did they really accept it?

Why is asking 'can machines think?' assuming our thinking could be modeled as a machine? It's raising the possibility that our thinking could be modeled as a machine. Given that, as you acknowledge, we don't have a clue how our mind works, it seems premature to rule out this possibility. Rather, I would say that ruling it out betrays an assumption that we understand how the mind works enough that we can say that it is definitely not replicable by a machine, and that assumption seems unjustified.

Why would it serve the interests of AI companies to promote materialism? It seems to me that idealism would be more in the interest of AI companies to promote, since my impression is idealists are more likely than materialists to believe that AI will never be conscious, and AI being perceived as conscious would be problematic for companies that want to provide AI as a product.

I don't think that's necessarily the case. I understand that there's a continuum in reality, but psychologically, I still tend to perceive each shade as discretely either blue or green, especially when the shade is presented in isolation. Words like "teal", "cyan", etc. aren't really part of my normal vocabulary and to the extent that they are, I would think of them as subsets of blue or green, not disjoint sets.

I think the test can be fairly criticised on the basis that it is assuming everyone's psychological colour space has a discrete boundary between blue and green, which clearly isn't the case for some people (like you), but it is for others (like me).

Isabelle/HOL haven't been solving open problems, as far as I'm aware. They've been used for making fully-formal proofs of problems that were already considered proved to a satisfactory level by the mathematical community. I believe mathematicians generally consider proving something to the mathematical community the "hard part", while making it fully formal is just a kind of tedious bookkeeping thing.

The reason I don't spend the majority of my time in code review is that when I'm reviewing my teammates' code I trust that the code has already been substantially verified already by that teammate in the process of writing it and testing it. Like 90% verified already. I see code review as just one small stage in the verification process, not the whole of it.

The way I approach it, it's really more about checking for failures, rather than verifying success. Like a smoke test. I scan over the code and if anything stands out to me as wrong, I point it out. I don't expect to catch everything that's wrong, and indeed I don't (as demonstrated by the fact that other members of the team will review the code and find issues I didn't notice). When the code has failed review, that means there's definitely an issue, but when the code has passed review, my confidence that there are no issues is still basically the same as it was before, only a little bit higher. Maybe I'm doing it wrong, I don't know.

If I had to fully verify that the code was correct when reviewing, applying the same level of scrutiny that I apply to my own code when I'm writing, I feel like I'd spend much longer on it---a similar time to what I'd spend writing on it.

Now with LLM coding, I guess opinions will differ as to how far one needs to fully verify LLM-generated code. If you see LLMs as stochastic parrots without any "real" intelligence, you'll probably have no trust in them and you'll see the code generated by the LLM as being 0% verified, and so as the user of the LLM you then have to do a "review" which is really going from 0% to 100%, not 90% to 100% and so is a much more challenging task. On the other hand, if you see LLMs as genuine intelligences you'd expect that LLMs are verifying the code to some extent as they write it, since after all it's pretty dumb to write a bunch of code for somebody without checking that it works. So in that case, you might see the LLM-generated code as 90% verified already, just as if it was generated by a trusted teammate, and then you can just do your normal review process.

It's true that onomatopoeia isn't always a word, but in the particular case of "aah", I think that particular choice of letters is conventionalized enough that it is a word.

From Wikipedia:

"The exact location of Hyperion is nominally secret but is available via internet search.[12] However, in July 2022, the Redwood Park superintendent closed the entire area around the tree, citing "devastation of the habitat surrounding Hyperion" caused by visitors. Its base was trampled by the overuse and as a result ferns no longer grow around the tree.[13]

Measures to protect the Hyperion tree were officially implemented in 2022 when the National Park Service (NPS) closed public access to its location in Redwood National Park.[14][15] Anyone who gets too close could face up to six months in jail and a $5,000 maximum fine.[13][16][17]"

My impression (as a dilettante programmer without relevant credentials) is that there isn't really any question about whether mathematical structures can be rooted in set theory, or can be expressed as extensions of set theory. Disputes about foundations of mathematics are more about how easy or elegant it is to do so. (And in fact my impression is they're mostly about subjective, aesthetic considerations of elegance rather than practical considerations of how hard it is to do something in practice, even though the discussion tends to be nominally about the practical side. Quite similar to disputes about programming languages in that respect.)

Defining first-order logic doesn't really require set theory, but it does require some conception of natural numbers. Instead of saying there's an infinite set of variables, you can have a single symbol x and a mark *, and then you can say a variable is any string consisting of x followed by any number of marks. You can do the same thing with constants, relation symbols and function symbols. This does mean there can only be countably many of each type of symbol but for foundational purposes that's fine since each proof will only mention finitely many variables.

Allowing uncountably many symbols can be more convenient when you apply logic in other ways, e.g. when doing model theory, but from a foundational perspective when you're doing stuff like that you're not using the "base" logic but rather using the formalized version of logic that you can define within the set theory that you defined using the base logic.

My first thought on reading your comment was to disagree and say no, we can have the exact value of 1, because we can choose our system of units and so we can make the square a unit square by fiat.

A better way to dispute the unit square diagonal argument for the existence of sqrt(2) would be to argue that squares themselves are unphysical, since all measurements are imprecise and so we can't be sure that any two physical lengths or angles are exactly the same.

But actually, this argument can also be applied to 1 and other discrete quantities. Sure, if I choose the length of some specific ruler as my unit length, then I can be sure that ruler has length 1. But if I look at any other object in the world, I can never say that other object has length exactly 1, due to the imprecision of measurements. Which makes this concept of "length exactly 1" rather limited in usefulness---in that sense, it would be fair to say the exact value of 1 doesn't exist.

Overall I think 1, and the other integers, and even rational numbers via the argument of AIPendant about egg cartons, are straightforwardly physically real as measurements of discrete quantities, but for measurements of continuous quantities I think the argument about the unit square diagonal works to show that rational numbers are no more and no less physically real than sqrt(2).

Consider the identity function f, which just takes an argument and returns it unchanged, and has the polymorphic type a -> a, where a is a type variable. What's the type of f(f)?

Obviously, since f(f) = f it should be a -> a as well. But to infer it without actually evaluating it, using the standard Hindley-Milner algorithm, we reason as follows: the two f's can have different specific types, so we introduce a new type variable b. The type of the first f will be a substitution instance of a -> a, the type of the second f will be a substitution instance of b -> b. We introduce a new type variable c for the return type, and solve the equation (a -> a) = ((b -> b) -> c), using unification. This gives us the substitution {a = (b -> b), c = (b -> b)}, and so we see that the return type c is b -> b.

But if we use pattern matching rather than unification, the variables in one of the two sides of the equation (a -> a) = ((b -> b) -> c) are effectively treated as constants referring to atomic types, not variables. Now if we treat the variables on the left side as constants, i.e. we treat a as a constant, we have to match b -> b to the constant a, which is impossible; the type a is atomic, the type b -> b isn't. If we treat the variables on the right side as constants, i.e. we treat b and c as constants, then we have to match a to both b -> b and c, and this means our substitution will have to make b -> b and c equal, which is impossible given that c is an atomic type and b -> b isn't.

It would surprise me if most rationalists didn't know who Jaynes was. I first heard of him via rationalists. The Sequences talk about him in adulatory tones. I think Yudkowsky would acknowledge him as one of his greatest influences.

What do you find surprising---the fact that it doesn't come out red, or the fact that people are confused by this behaviour?

At least in my country (the UK), people generally do not learn abstract algebra in high school. That's a university-level topic.

I think there is a definite "step up" in complexity between the structures of abstract algebra such as monoids, rings, groups and vector spaces, and monads. All of those algebraic structures are basically just sets equipped with operations satisfying some equations. Monads are endofunctors equipped with natural transformations satisfying some equations. "Endofunctor" and "natural transformation" are considerably more advanced and abstract concepts than "set" and "operation", and they are concepts that belong to category theory (so I don't see how you can read and understand the definition of a monad without that basic level of category theory).

Your time estimates also seem wildly optimistic. A common rule of thumb is that reading a maths textbook at your level takes around an hour per page. I think the definition of a monad can be compared to one page of a textbook. So I'd say it'll take on the order of hours to read and understand the definition of a monad, and that's assuming you're already entirely comfortable with the pre-requisite concepts (natural transformations, etc.)