Traditions are sets of practices that have survived and passed down through time from generation to generation. They usually weren't arrived at through a process of reasoning, and even if they were, that reasoning is often lost to time. And yet, the very fact that these traditions propagated through time gives us information about their utility... (read more)
AI Control in the context of AI Alignment is a category of plans that aim to ensure safety and benefit from AI systems, even if they are goal-directed and are actively trying to subvert your control measures. From The case for ensuring that powerful AIs are controlled:.. (read more)
Archetypal Transfer Learning (ATL) is a proposal by @whitehatStoic for what is argued by the author to be a fine tuning approach that "uses archetypal data" to "embed Synthetic Archetypes". These Synthetic Archetypes are derived from patterns that models assimilate from archetypal data, such as artificial stories. The method yielded a shutdown activation rate of 57.33% in the GPT-2-XL model after fine-tuning. .. (read more)
If you are new to LessWrong, the current iteration of this, is the place to introduce yourself... (read more)
Repositories are pages that are meant to collect information and advice of a specific type or area from the LW community. .. (read more)
A threat model is a story of how a particular risk (e.g. AI) plays out... (read more)
A Self Fulfilling Prophecy is a prophecy that, when made, affects the environment such that it becomes more likely. similarly, a Self Refuting Prophecy is a prophecy that when made makes itself less likely. This is also relevant for beliefs that can affect reality directly without being voiced, for example, the belief "I'm confident" can increase a person confidence, thus making it true, while the opposite belief can reduce a person's confidence, thus also making it true... (read more)
A project announcement is what you might expect - an announcement of a project.
Posts that are about a project's announcement, but do not themselves announce anything, should not have this tag... (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.
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:
In addition, the Axiom of Choice precludes the possibility of any infinite well ordered chain which includes no subsets without a greatest element (well ordered in both ascending and descending order).
, and if there are two sets, each of which contains exactly one subset of each set in athis set of sets:sets, such as :
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...
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
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.
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,...
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.
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.
,
, 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).
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.
"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...
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.
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.