Eliezer Yudkowsky is a research fellow of the Machine Intelligence Research Institute, which he co-founded in 2001. He is mainly concerned with the obstacles and importance of developing a Friendly AI, such as a reflective decision theory that would lay a foundation for describing fully recursive self modifying agents that retain stable preferences while rewriting their source code. He also co-founded LessWrong, writing the Sequences, long sequences of posts dealing with epistemology, AGI, metaethics, rationality and so on... (read more)
Someone is well-calibrated if the things they predict with X% chance of happening in fact occur X% of the time. Importantly, calibration is not the same as accuracy. Calibration is about accurately assessing how good your predictions are, not making good predictions. Person A, whose predictions are marginally better than chance (60% of them come true when choosing from two options) and who is precisely 60% confident in their choices, is perfectly calibrated. In contrast, Person B, who is 99% confident in their predictions, and right 90% of the time, is more accurate than Person A, but less well-calibrated... (read more)
AI Risk is analysis of the risks associated with building powerful AI systems... (read more)
| User | Post Title | Wikitag | Pow | When | Vote |
Lean is a programming language designed as a proof assistant, for formally verifying software and mathematical theorems. It uses a dependent type system based on the Calculus of Inductive Constructions, similar to the older Rocq Prover.
Lean was first developed by Leonardo de Moura at Microsoft Research, where he released Lean1 in 2013. The current version is Lean4 (released in 2021 and backwards-incompatible with Lean3). It has gained substantial traction, first with the mathematics community, who have worked to encode much of modern mathematics into the library Mathlib, and then as a tool for use with LLMs. In 2023 work on the Lean project was moved into its own organization.
,
, and if there are two sets, each of which contains exactly one subset of each set in this set of sets, such as :
The Generalized Continuum HypthosisHypothesis (GCH) is, well, a generalized version of the Continuum Hypothesis, stating that not only are there no sets of size lying strictly between the natural numbers and the reals , but that for any set , there is no set of size lying strictly between the sizes of and the power set . In particular, note that the reals is of the same size as the power set of the naturals, so that GCH implies CH. It is also strictly stronger than CH (it is not implied by CH).
"There "The Axiom of Choice is necessary to select a set from an infinite number of pairs of socks, but not an infinite number of pairs of shoes." — Bertrand Russell, Introduction to mathematical philosophy
In other words, it is possible to form these models in some weaker theory on which we have "more of a grip". The entirityentirety of set theory are then special objects satisfying the axioms of this weaker theory. Is it possible to repeat this process ad infinitum? No. But if we want, we could even deal with just a finite fragment of set theory: We assume that any mathematics we want to do only needs a finite number of the (infinitely many) axioms of set theory. We then prove what we want about this finite fragment. But we may as well have proved it about the whole theory.
Zorn's Lemma can be proven by using the axiom of choiceChoice to choose the elements in a particular such chain which is so long that it cannot be extended in the 'upwards' direction by adding a further element to it; the existence of this chain combined with the fact that each one has an upper bound implies that there is a maximal element, namely that chain's upper bound.
In other words, the set of natural numbers has the smallest infinite(i.e. unending as the definition explicates) ordinal number of elements. That such a set exists is guaranteed by the axiomAxiom of infinity.Infinity.
The final task is to prove that the set it delineates really is a chain. To this end we demonstrate that each element chosen by the axiomAxiom of choiceChoice follows its unbroken chain in the same way ω succeeds all the natural numbers. To achieve this, we will prove an equivalent statement about these 'anchored unbroken chains' or 'antechains' as we call them: that none of them 'gives rise to' anything beyond any element beyond any of its elements. This is to say that it does not include any antechains (including itself) whose chosen element is greater than any element which strictly exceeds all of its elements. That this is true of all such chains less than a given element is a statement about said element, the induction hypothesis.
We have not yet shown that the set is a chain; to do so, we nest one application of the principle of transfinite induction inside another in a process called double induction. To initiate the first layer, we note that its least element is comparable to each of the others by definition, and again assume that there exists an antechain each of the elements of which is also comparable to each of the others in our set. To demonstrate that the same...
Yet, mathematicians do disagree about this axiom, and whether it applies to our world as well. Some mathematicians take a Platonic view of mathematics, in which mathematical objects such as sets actually exist in some abstract realm, and for which the axiom of choice is either true or false, but we do not know which. Others take a highly constructive view (in many cases motivated by realism and the ability of the mathematics to model the world) in which either the axiom of choice is false, or infinite sets do not exist in which case the axiom of choice is provable and hence superfluous. Others take the view that the axiom is not true or false, but merely useless, and that anything provable from it is meaningless. Many seem not to care: the axiom is convenient for the mathematics they wish to do (whose application they are not much concerned about in any case) and hence they assume it without qualm. Another interpretation of the axiom is as analogous to Euclid's parallel postulate, delineating one region of the mathematical universe in which it itis true from others where it might be replaced with alternatives.
Zorn's Lemma can be proven by using the axiom of choice to choose the elements in a particular such chain which is so long that it cannot be extended in the 'upwards' direction by adding a further element to it; the existence of this chain combined with the fact that each one has an upper bound implies that there is a maximal element, namely that chain's upper bound.
Consider that if Zorn's lemma were false, then it would not be possible to extend the chain that far, in which case it would have an upper bound, by the chain hypothesis. But this upper bound would need to be less than some element in the partially ordered set, otherwise it would be maximal, and that even larger element could then be appended to lengthen the chain, contradicting the assumption that it couldn't be extended.
How can this chain be 'constructed' 'chosen'? Clearly, the partially ordered set contains at least one element. This element can be designated the least or first in the chain. We can then define a set to be the minimal subset of the partially ordered set which satisfies certain criteria:
While this may seem like a strange or convoluted definition, it's actually very similar to the principle of mathematical induction. The (Von-Neumann ordinal) set of all natural numbers (ω) is defined to be the smallest set which:
This definition ensures the existence of the whole set of natural numbers, but it does it in a way which doesn't require an infinite number of symbols, namely by a kind of self reference: the set contains the successor of any element it contains. It also ensures that if you have a statement which is true of 0, and you know that it's also true of the successor of any natural number of which it's true, then the set of all natural numbers of which it's true satisfies the above criteria and therefore contains all the natural numbers. This is because it is the minimal set with this property, so any other set with it must, by definition, include it.
In other words,...
Zorn's Lemma can be proven by using the axiom of choice to choose the elements in a particular such chain which is so long that it cannot be extended in the 'upwards' direction by adding a further element to it; the existence of this chain combined with the fact that each one has an upper bound implies that there is a maximal element, namely that chain's upper bound.
Consider that if Zorn's lemma were false, then it would not be possible to extend the chain that far, in which case it would have an upper bound, by the chain hypothesis. But this upper bound would need to be less than some element in the partially ordered set, otherwise it would be maximal, and that even larger element could then be appended to lengthen the chain, contradicting the assumption that it couldn't be extended.
How can this chain be 'constructed' 'chosen'? Clearly, the partially ordered set contains at least one element. This element can be designated the least or first in the chain. We can then define a set to be the minimal subset of the partially ordered set which satisfies certain criteria:
While this may seem like a strange or convoluted definition, it's actually very similar to the principle of mathematical induction. The (Von-Neumann ordinal) set of all natural numbers (ω) is defined to be the smallest set which:
This definition ensures the existence of the whole set of natural numbers, but it does it in a way which doesn't require an infinite number of symbols, namely by a kind of self reference: the set contains the successor of any element it contains. It also ensures that if you have a statement which is true of 0, and you know that it's also true of the successor of any natural number of which it's true, then the set of all natural numbers of which it's true satisfies the above criteria and therefore contains all the natural numbers. This is because it is the minimal set with this property, so any other set with it must, by definition, include...
An exfohazard is a piece of information that can cause harm if shared, for instance, the genetic code for a deadly virus. Exfohazards are often considered a type of infohazard, and as of 2026, the words are used somewhat interchangeably. In this post, Yudkowsky suggests that we only use "exfohazard" to refer to information that causes harm when shared, and reserve the word "infohazard" for information that is directly harmful to the bearer, i.e. information that you as an individual would not want to hear.
One should be cautious when discussing these.
Examples and discussion:
See also:
and
then we can consider the latter to be smaller than the former because of this inclusion, and both of them to be members of a partially ordered set of subsets of the original set. We can see that any chain of these sets ordered in this way has an upper bound which can be obtained simply by taking the intersections of their elements, which in this case yields again. Zorn's Lemma ensures the existence of a maximal element of the partially ordered set, which must be a set such that it cannot possibly be reduced by removing elements from its elements in this way. Clearly, each element of this maximal set contains exactly one element from each set in the original set of sets itself, and its existence, or that of its union is the consequence of the Axiom of Choice as it applies to the original set of sets. As this set of sets was arbitrary, we can conclude that the Axiom of Choice is true.
More formally, given a set X whose elements are only non-empty sets, there is a function
from X to the union of all the elements of X such that, for each Y∈X, the image of Y under f is an element of Y, i.e., f(Y)∈Y.
For a finite set X containing only finite non-empty sets, the axiom is actually provable (from the Zermelo-Fraenkel axioms of set theory ZF), and hence does not need to be given as an axiom. In fact, even for a finite collection of possibly infinite non-empty sets, the axiom of choice is provable (from ZF), using the axiom of induction. In this case, the function can be explicitly described. For example, if the set X contains only three, potentially infinite, non-empty sets Y1,Y2,Y3, then the fact that they are non-empty means they each contain at least one element, say y1∈Y1,y2∈Y2,y3∈Y3. Then define f by f(Y1)=y1, f(Y2)=y2 and f(Y3)=y3. This construction is permitted by the axioms ZF.
The problem comes in if X contains an infinite number of non-empty sets. Let's assume X contains a countable number of sets Y1,Y2,Y3,…. Then, again intuitively speaking, we can explicitly describe how f might act on finitely many of the Ys (say the first n for any natural number n), but we cannot describe it on all of them at once.
To understand this properly, one must understand what it means to be able to 'describe' or 'construct' a function f. This is described in more detail in the sections which follow. But first, a bit of background on why the axiom of choice is interesting to mathematicians.
This is the statment that taking the mathematical product of non-empty sets will always yield a non-empty set. Consider infinitely many sets X1,X2,X3,… indexed by the natural numbers. Then an element of the product ∏i∈NXi is a family (essentially an infinite tuple) of the form (x1,x2,x3,…) where x1∈X1, x2∈X2 and so on. However, to select such a tuple in the product amounts to selecting a single element from each of the sets. Hence, without the axiom of choice, it is not provable that there are any elements in this product.
However, it does seem somewhat counterintuitive that such a product be non-empty. In general, given two non-empty sets, X1 and X2, the product is at least as large as either of the sets. Adding another non-empty set X3 usually makes the product larger still. It may seem strange, then, that taking the limit of this procedure could result in an empty structure.
Any continuous functions f:C→C from a closed_disk C onto itself has a fixed_point x0. (In full generality, C may be any convex compact set).
In other words, there is at least one point x0∈C such that f(x0)=x0.
Lean is a programming language designed as a proof assistant, for formally verifying software and mathematical theorems. It uses a dependent type system based on the Calculus of Inductive Constructions, similar to the older Rocq Prover.
Lean was first developed by Leonardo de Moura at Microsoft Research, where he released Lean1 in 2013. The current version is Lean4 (released in 2021 and backwards-incompatible with Lean3). It has gained substantial traction, first with the mathematics community, who have worked to encode much of modern mathematics into the library Mathlib, and then as a tool for use with LLMs. In 2023 work on the Lean project was moved into its own organization.
Ursula von der Leyen
Mark Carney: p(doom) is "above zero"
Barack Obama: "Nonzero chance" of being wiped out by "killer robots"
António Guterres
Rishi Sunak
Prince Albert II
Naftali Bennett
Ted Lieu (CAIS Signatory)
Audrey Tang (CAIS Signatory)
Bernie Sanders: Bernie Sanders Reveals the AI ‘Doomsday Scenario’ That Worries Top Experts
David Chalmers (CAIS Signatory)
Toby Ord (CAIS Signatory)
Will MacAskill (CAIS(CAIS Signatory)
Others:
Chris Anderson - Dramer-in-Chief, TED (CAIS Signatory)
Lex Fridman (CAIS Signatory)
Grimes (CAIS Signatory)
Stephen Fry (endorsed "If Anyone Builds It, Everyone Dies")
Cenk Uygur: AI's Disturbing Behaviors Will Keep You Up At Night
Paul Tudor Jones: AI poses an imminent threat to humanity in our lifetime
Nate Silver
Steve Bannon
Bill Gates
Interestingly, we can see that any subset containing elements of the 'chosen' chain either contains the initial element, or contains only elements which are greater than those of some subset of this chain(atchain (at the very least, that containing the initial element alone). The union of all of the subsets of the chain whose elements are smaller than the subset in question is clearly an unbroken anchored chain. This means that the element chosen by the choice function to be greater than this chain is the least element of the subset in question, and we can infer that this is true of all of the non empty subsets of the maximal chain, a property known as being well ordered.
Yet, mathematicians do disagree about this axiom, and whether it applies to our world as well. Some mathematicians take a Platonic view of mathematics, in which mathematical objects such as sets actually exist in some abstract realm, and for which the axiom of choice is either true or false, but we do not know which. Others take a highly constructive view (in many cases motivated by realism and the ability of the mathematics to model the world) in which either the axiom of choice is false, or infinite sets do not exist in which case the axiom of choice is provable and hence superfluous. Others take the view that the axiom is not true or false, but merely useless, and that anything provable from it is meaningless. Many seem not to care: the axiom is convenient for the mathematics they wish to do (whose application they are not much concerned about in any case) and hence they assume it without qualm. Another interpretation of the axiom is as analogous to Euclid's parallel postulate, delineating one region of the mathematical universe in which it it true from others where it might replaced with alternatives.
Interestingly, we can see that any subset of the 'chosen' chain either contains the initial element, or contains only elements which are greater than those of some subset of this chain(at the very least, that containing the initial element alone) . The union of all of the subsets of the chain whose elements are smaller than the subset in question is clearly an unbroken anchored chain. This means that the element chosen by the choice function to be greater than this chain is the least element of the subset in question, and we can infer that this is true of all of the subsets of the maximal chain, a property known as being well ordering.ordered.
Note that it may also be possible for a maximal element to exist without there being an upper bound. Consider for example the natural numbers with an 'extra' element which is not comparable to any of the numbers. Then this is a perfectly acceptable poset. Since this extra element is incomparable, then in particular there is no element larger than all n.
All well ordered sets are susceptible to transfinite induction. This means that if we can prove that any statement which is true of all elements smaller than a given element in the well-ordered set is also true of that element, it follows that it is true of every element in the well ordered set. This extends the principle of mathematical induction to apply to sets of vastly larger cardinality than the set of natural numbers.
, and if there are two sets, each of which contains exactly one subset of each set in athis set of sets:sets, such as :
Is there a way of finding a list of guarded definitions on which the lesswrong community has settled on a meaning? I know https://www.lesswrong.com/w/pivotal-act is labeled as such. It would be helpful for me if this page would contain a short description how to find guarded definitions on this website.