2.4. Proofs in Lean
So far, we have explored the dependent type theory on which Lean is built, as well as the foundations that guarantee the correctness of its proofs. We therefore move on to a more practical approach: how do we write mathematics in Lean?
Let us remember that formalising a result in Lean does not consist only of writing its statement, but also of constructing a proof step by step, with no omissions and with total precision. Here, it is never enough to write "trivial" when we believe we should already know something: we need to convince the system that every step is valid.
This section is devoted to learning how to write proofs in Lean. We will see how to introduce new objects into our context, how to state propositions and how to build proofs by interacting with Lean. We will also present some automation tools and methods for relying on the Mathlib library.
2.4.1. Axioms, definitions and variables
Before writing proofs in any formal system, we need to describe the context in which we work: the set of objects and hypotheses available at a given moment. This context is dynamic and expands as we introduce new elements.
The same happens in Lean. The system maintains and constantly updates this context to check that each expression is well formed and has the expected type.
We can introduce new information into the context in different ways. We distinguish between axioms, definitions and variables, each with a different logical function in the system.
-
AxiomsIn Lean 3, this kind of declaration was called a constant and used the
constantcommand.
They allow us to introduce hypotheses that are assumed without proof. In particular, writing that x "has type X" is also a hypothesis, so axioms can be used to introduce new objectsIn this sense we said that defining an inductive type is analogous to writing a collection of axioms. inductive Nat can be seen as a structured version of axiom Nat : Type, axiom zero : Nat, axiom succ : Nat to Nat, etc.. For example:
axiom P : Prop
axiom h : P → P
We are declaring a proposition P and a proof that P implies P.
axiom n : Nat
axiom hn : n > 2
Here we are assuming that n is a natural number greater than 2.
Thus, axioms allow us to fix facts that we want to assume as valid throughout our proofs.
-
Definitions
They introduce new objects from already known ones. Unlike axioms, it is not enough to indicate the type of the new object; its construction must also be given. For example:
def f : Nat → Nat := fun n ↦ 2 * n
def n : Nat := 3
def es_par : Nat → Prop := fun n ↦ ∃ m, n = f m
Moreover, when the type can be inferred from the construction, it is not necessary to indicate it explicitly:
def n := 3
#check n
-
Variables
In most programming languages, we are used to defining a variable implying assigning a concrete value to it. However, in Lean variables behave more like they do in logic. When introducing a variable x, what is introduced is a universal context: whenever x appears free, Lean will interpret that what follows is universally quantified with respect to x. For exampleVariables, unlike axioms and definitions, are written between parentheses. The same happens with the arguments taken by propositions, as we will see later. This is related to the Curry–Howard correspondence: declaring a variable amounts to abstracting over it, which corresponds to quantifying universally.:
variable (x : Nat)
axiom hx : x ≥ 0
#print hx
2.4.2. Propositions
Besides introducing objects, we also want to state and prove propositions. In Lean, this is done in the same way as in other formal systems: we first write the results (as lemmas or theorems) formally, and then we provide a proof.
As we have already seen, a proposition in Lean is a term of type Prop, and a proof of p : Prop is simply a term of type p. Therefore, proving a proposition is no different from defining an object; we can use def to write mathematical results. For example:
def mi_prop : 1 > 0 := ...
Here we are saying that mi_prop is an object of type 1 > 0. If in the place of ... we provide a term of type 1 > 0, we will have proved mi_prop.
However, for greater clarity and structure, Lean provides the lemma and theorem commands. Both work exactly like def and are interchangeable with each other, but they make the code easier to read by indicating which objects are mathematical results, and the hierarchy of importance among them. The syntax is the same:
lemma my_lemma : 1 > 0 := ... theorem commutative_sum (a b : ℕ) : a + b = b + a := ...
There is also the example command, which is used to write proofs without the need to name the result:
example (a b : ℕ) : a * b = b * a := ...
This kind of expression does not extend the context or define new objects; they are simply local checks. But we will see that they can be useful to us on certain occasions.
2.4.3. Proofs: tactic mode
We arrive at the central part of this section: writing proofs in Lean. In general, there are two ways of constructing a proof in Lean:
-
By means of terms, that is, directly writing an expression of the desired type.
-
By means of tactic mode, in which a proof is built step by step using instructions called tactics.
In this work we will use tactic mode exclusively, since it is the most practical approach and the closest to the way we reason when writing mathematical proofs in natural language.
In an informal proof, we usually advance through chained logical steps: "suppose that...", "then...", "by the lemma..., we have...". Each of these steps is translated in Lean through a tactic: an instruction that modifies the state of the proof, whether by introducing hypotheses, applying known results, splitting the goal into more manageable parts, etc.
Moreover, tactic mode allows us to work interactively with Lean. If we write a statement, and immediately after := we write by, we are telling Lean that we are going to use tactic mode for the construction of this term. For example:
example (p q : Prop) (hp : p) (hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q
We are indicating that we want to construct a term of type p ∧ q from the hypotheses hp : p and hq : q, and that we are going to use tactic mode for that construction.
Internally, Lean interprets this by generating a local context (our hypotheses) and a goal (our thesis), which consists of constructing the term of the expected type. After by, we can start writing tactics, which Lean will interpret by updating the context and the goals.
This goal is reflected in the InfoView, a window that shows the current state of our proof. Lean processes line by line automatically, so at any moment we can consult the impact of having applied a tactic simply by placing the cursor on the corresponding line of code.
In fact, the InfoView also shows the results of the instructions we have already seen, such as #check, #print or #eval.
In general, while writing in Lean, we will have this window open alongside our code, so that we can watch the progress of our proof.
Under the Tactic state section, we can check:
-
The number of goals we still have to prove (in this case just one:
1 goal). -
Our context.
-
The goal (or goals), marked with the symbol
⊢.
From this point on, we can start adding the tactics that will make up our proof. Tactics are written one after another, separated by semicolons (;) or by line breaks.
When writing a tactic, the Tactic state section of the InfoView will update accordingly. When all the goals have been solved, the InfoView will show No goals.
2.4.4. Some basic tactics
In this section we will see some of the most basic and useful tactics for constructing proofs in Lean. We will see how they are applied and what effect they have on the InfoView. The rest of the tactics that appear throughout this work can be consulted in the tactics section of the Lean documentation (Lean Prover Community, 2023)Lean Prover Community, 2023. “Mathlib manual: Tactics”. Last accessed: June 24, 2025..
In order to use the tactics mentioned below, it is necessary to import the Mathlib module corresponding to tactic mode via
import Mathlib.TacticFrom here on, instead of showing screenshots of the InfoView, we will use two code blocks side by side: the one on the left contains the Lean code; the one on the right represents the state that would be shown in the InfoView if we placed the cursor on the last line.
2.4.4.1. intro
The intro tactic introduces a new object into the context, similar to writing "Suppose that..." or "Let..." in an informal proof.
It is useful when the goal has the form of an implication or a universal quantifier: we turn the first part of the goal into a new hypothesis and the second part into the new goal. For example, for the implication:
example (p : Prop) : p → p := p:Prop⊢ p → p↓
example (p : Prop) : p → p := p:Prop⊢ p → p
p:Prophp:p⊢ pAnd for removing quantifiers:
example : ∀ (p : Prop), p → p := ⊢ ∀ (p : Prop), p → p↓
example : ∀ (p : Prop), p → p := ⊢ ∀ (p : Prop), p → p
q:Prop⊢ q → q
2.4.4.2. exact
The exact tactic is used when we already have, in our context, exactly what we want to prove. That is, there is a hypothesis that matches the current goal. For example:
example : ∀ (p : Prop), p → p := ⊢ ∀ (p : Prop), p → p
intro p p:Prophp:p⊢ p↓
example : ∀ (p : Prop), p → p := ⊢ ∀ (p : Prop), p → p
intro p p:Prophp:p⊢ p
All goals completed! 🐙By way of comparison, we could construct this proof using only terms in the following way:
example : ∀ (p : Prop), p → p := fun p ↦ (fun hp : p ↦ hp)In this case it may turn out simpler, but in more complex proofs we lose readability.
2.4.4.3. apply
The apply tactic allows us to use an implication to reduce a goal to a simpler one. It amounts to using the Modus Ponens rule: if we have a hypothesis of the form p \rightarrow q and we want to prove q, it suffices to prove p.
example (p q : Prop) (hp : p)
(hpq : p → q) : q := p:Propq:Prophp:phpq:p → q⊢ q↓
example (p q : Prop) (hp : p)
(hpq : p → q) : q := p:Propq:Prophp:phpq:p → q⊢ q
p:Propq:Prophp:phpq:p → q⊢ p
We could complete this proof using exact hp.
2.4.4.4. use
We use use to work with the existential quantifier. If we want to prove a proposition of the form "\exists x, P x", it suffices to find a concrete x_0 that satisfies the property P.
In this case, we apply use to tell Lean the concrete value x_0 that we want to use to prove existence. The goal then becomes proving that x_0 satisfies P. For example:
example : ∃ n : ℕ, n > 3 := ⊢ ∃ n, n > 3↓
example : ∃ n : ℕ, n > 3 := ⊢ ∃ n, n > 3
⊢ 5 > 3
2.4.4.5. left, right
The left and right tactics are used to work with disjunctions, that is, propositions of the form A \lor B.
In an informal proof, if we want to show that "A or B" is true, it is enough to prove one of the two. We use left to indicate that we are going to prove the left part (A), and right if we want to prove the right part (B). For example:
example (p q : Prop) (hp : p) :
p ∨ q := p:Propq:Prophp:p⊢ p ∨ q↓
example (p q : Prop) (hp : p) :
p ∨ q := p:Propq:Prophp:p⊢ p ∨ q
p:Propq:Prophp:p⊢ p
We could complete this proof by applying exact hp.
2.4.4.6. constructor
We use constructor to work with conjunctions, that is, propositions of the form A \land B.
When we want to prove that "A and B" is true, we can prove A on one side and B on the other. When applying constructor, Lean splits a goal A ∧ B into two sub-goals with the same context: one for A and another for B. For example:
example (p q : Prop) (hp : p)
(hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q↓
example (p q : Prop) (hp : p)
(hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q
p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q
After applying constructor, the InfoView will show two pending goals (2 goals). By solving each one separately, we complete the proof.
example (p q : Prop) (hp : p)
(hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q
p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q
p:Propq:Prophp:phq:q⊢ q
All goals completed! 🐙
Although the above is correct, the usual practice when working with more than one goal is to use · to separate them. When we write · after a line break, Lean focuses on the first goal, temporarily hiding the rest. For example:
example (p q : Prop) (hp : p)
(hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q
p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q
p:Propq:Prophp:phq:q⊢ p
If we place the cursor at the end, the InfoView only shows 1 goal, because the second goal is hidden for now. The complete proof in this style would be:
example (p q : Prop) (hp : p)
(hq : q) : p ∧ q := p:Propq:Prophp:phq:q⊢ p ∧ q
p:Propq:Prophp:phq:q⊢ pp:Propq:Prophp:phq:q⊢ q
p:Propq:Prophp:phq:q⊢ p All goals completed! 🐙
p:Propq:Prophp:phq:q⊢ q All goals completed! 🐙
2.4.4.7. cases'
The cases' tactic is used to analyse a disjunction in the context, that is, a hypothesis of the form A \lor B.
In an informal proof, it amounts to reasoning by cases: "Suppose A holds, and let us see whether the goal follows; suppose then that B holds, and let us check whether it also follows".
When applying cases' h to a hypothesis h, Lean duplicates the goal (which does not change), but modifies the context in each of the new goals, introducing the hypotheses corresponding to each case. We use the with keyword to assign names to the new hypotheses. For example:
example (p q : Prop) (h : p ∨ q)
(hpq : p → q) : q := p:Propq:Proph:p ∨ qhpq:p → q⊢ q↓
example (p q : Prop) (h : p ∨ q)
(hpq : p → q) : q := p:Propq:Proph:p ∨ qhpq:p → q⊢ q
p:Propq:Prophpq:p → qhp:p⊢ qp:Propq:Prophpq:p → qhq:q⊢ qWe can then complete the proof with the tools we have so far:
example (p q : Prop) (h : p ∨ q)
(hpq : p → q) : q := p:Propq:Proph:p ∨ qhpq:p → q⊢ q
p:Propq:Prophpq:p → qhp:p⊢ qp:Propq:Prophpq:p → qhq:q⊢ q
p:Propq:Prophpq:p → qhp:p⊢ q p:Propq:Prophpq:p → qhp:p⊢ p
All goals completed! 🐙
p:Propq:Prophpq:p → qhq:q⊢ q All goals completed! 🐙
As we have seen through these examples, completing a proof in tactic mode consists of combining these instructions one after another, making the hypotheses and the goals advance until reaching the desired state: No goals. Tactics give us the flexibility needed to formalise a wide variety of mathematical results.
2.4.5. Automation tools and searching Mathlib
As proofs in Lean become more complex, it is not always practical to build every step manually. To speed up the process, Lean incorporates some automation tools that allow certain tasks to be delegated to the system.
Moreover, instead of proving again results that are already formalised, it is essential to take advantage of Lean's mathematical library, Mathlib, which contains thousands of definitions and theorems available for reuse.
However, relying on Mathlib is not always straightforward: results may have unintuitive or very specific names, and finding the lemma we need at a given moment is not always easy.
For example, a result as simple as: "If a, b, c are real numbers such that a < b and c < 0, then a + c < b" (which in an informal proof we would consider almost trivial), appears in Mathlib under the name add_lt_of_lt_of_neg'. In practice, remembering all these names is unfeasible, even for elementary results.
In this section we will introduce the simp and exact? tactics, which help us solve simple goals, and two external tools we can use to locate results in Mathlib. We will also see how to integrate these tools into our result-proving process.
2.4.5.1. simp
The simplest way to rely on the Mathlib library is to use the simp tactic. This tactic performs an exhaustive search through a database of Mathlib lemmas that are marked with the simp attribute, trying to simplify as much as possible the goal or the hypotheses it is applied to.
The simp tactic can be used at any moment of the proof, but it is especially useful when something we want to prove seems evident or simple enough. For example:
example (G : Type) [Group G] (a b c : G) :
a * a⁻¹ * 1 * b = b * c * c⁻¹ := G:Typeinst✝:Group Ga:Gb:Gc:G⊢ a * a⁻¹ * 1 * b = b * c * c⁻¹
All goals completed! 🐙
Just by using simp we can finish the proof in this case. Really, all it does is repeatedly rewrite results of the form A = B or A ↔ B, until it cannot rewrite anything else, in a mechanical way. Therefore, although it is useful in many cases, in others it may not help us.
In practice, when it is easy for us to use other tactics or known results, that will be preferable to using simp: first because, being an exhaustive search, it is not a computationally efficient tactic, and second because it worsens the readability of the code, since it is sometimes hard to know how certain simplifications happen.
2.4.5.2. exact?
Lean incorporates some tactics that try to close the current goal using both the hypotheses of the context and the results available in the imported files. The most notable ones are exact?The exact? tactic was called library_search in Lean 3. and apply?.
Throughout the project, the one I have used most frequently is exact?. This tactic tries to find an expression that has exactly the type of the current goal, searching both in the local information (context hypotheses, previously defined results) and in the Mathlib library.
For example, in the case of finding local hypotheses:
example (p : Prop) : p → p := p:Prop⊢ p → p
p:Prophp:p⊢ p
All goals completed! 🐙And in the case of finding Mathlib results:
example (n : ℕ) : n ≥ 0 := n:ℕ⊢ n ≥ 0
All goals completed! 🐙
In general, using the expression suggested by exact? will conclude the proof.
Even though exact? can help us in many cases, it is a relatively simple tool, which can only take one step (applying a theorem or a hypothesis). This implies that if we do not have the exact hypotheses of the theorems as they appear in Mathlib, exact? will not find any solution.
When working with more complex hypotheses, the usual approach is not to use exact? directly to prove our goal, but to prove certain intermediate results. For this reason, a crucial tactic when working with exact? is have, the equivalent in informal proofs of stating a lemma in the middle of a proof. For example, suppose we want to prove:
example (p q r : Prop) (hpq : p → q) (hqr : q → r) (hp : p) : r
Instead of trying to prove r immediately, we could prove, as an intermediate step, that q holds. For this we use have:
example (p q r : Prop) (hpq : p → q)
(hqr : q → r) (hp : p) : r := p:Propq:Propr:Prophpq:p → qhqr:q → rhp:p⊢ r
p:Propq:Propr:Prophpq:p → qhqr:q → rhp:p⊢ qp:Propq:Propr:Prophpq:p → qhqr:q → rhp:phq:q⊢ r
Writing have hq : q introduces a new goal, q, independent from the previous one. Once we complete the proof of this new goal, we will be able to use the result in our proof. Therefore, we could complete the previous example in the following way:
example (p q r : Prop) (hpq : p → q) (hqr : q → r) (hp : p) : r := p:Propq:Propr:Prophpq:p → qhqr:q → rhp:p⊢ r
p:Propq:Propr:Prophpq:p → qhqr:q → rhp:p⊢ qp:Propq:Propr:Prophpq:p → qhqr:q → rhp:phq:q⊢ r
p:Propq:Propr:Prophpq:p → qhqr:q → rhp:p⊢ q p:Propq:Propr:Prophpq:p → qhqr:q → rhp:p⊢ p
All goals completed! 🐙
p:Propq:Propr:Prophpq:p → qhqr:q → rhp:phq:q⊢ q
All goals completed! 🐙
Remember that we use the dot · to separate the proof of hq from the rest of the proof.
Let us see, then, what the process of working with exact? looks like. Consider the following example, for which exact? does not find any result:
example (x : ℝ) (hx : x > 0) :
x / x = 1 := by
exact?
State in the InfoView:
Tactic state 1 goal x : ℝ hx : x > 0 ⊢ x / x = 1 Messages `exact?` could not close the goal.
-
Looking at the current state of the proof, identify what hypothesis we would like to have in our context. In this case, since a division is involved, it might be necessary to have the hypothesis
x \neq 0. -
Add the new goal using
haveIn some cases, it will be more useful to write what we believe we may need outside the proof, usingexample, because we will be able to write more general results..example (x : ℝ) (hx : x > 0) : x / x = 1 := x:ℝhx:x > 0⊢ x / x = 1 x:ℝhx:x > 0⊢ x ≠ 0x:ℝhx:x > 0h:x ≠ 0⊢ x / x = 1 x:ℝhx:x > 0⊢ x ≠ 0 -
Try to prove the new goal using
exact?.example (x : ℝ) (hx : x > 0) : x / x = 1 := x:ℝhx:x > 0⊢ x / x = 1 x:ℝhx:x > 0⊢ x ≠ 0x:ℝhx:x > 0h:x ≠ 0⊢ x / x = 1 x:ℝhx:x > 0⊢ x ≠ 0 All goals completed! 🐙
With this new hypothesis, it seems likely that exact? will be able to finish the proof. Indeed:
example (x : ℝ) (hx : x > 0) :
x / x = 1 := x:ℝhx:x > 0⊢ x / x = 1
x:ℝhx:x > 0⊢ x ≠ 0x:ℝhx:x > 0h:x ≠ 0⊢ x / x = 1
x:ℝhx:x > 0⊢ x ≠ 0 All goals completed! 🐙
All goals completed! 🐙
The exact? tactic is an example of a formal search engine: a tool that, through meta-programming in Lean, compares the current goal with the types of all the available lemmas and returns those with exact matches. Therefore, the key to using exact? effectively lies in gradually developing a certain intuition about which results are likely to be formalised in Mathlib, and the concrete way in which they are formulated.
Indeed, recognising that a Mathlib lemma about division by x probably required the hypothesis x\neq0 (and not simply x>0) was essential to being able to apply exact? successfully in the previous example.
Besides exact?, there are similar tactics such as apply? and rw?, which work in the same way and allow intermediate steps to be taken. However, in practice these tactics usually return a long list of options, many of which are not relevant or useful. Therefore, when exact? is not enough, it is more effective to turn to other search tools.
2.4.5.3. Other tools
Throughout this project I have mainly used two external Mathlib search tools: Moogle (Morph, 2023)Morph, 2023. “Moogle, a semantic search engine for Mathlib, the Lean mathematical library”. Last accessed: May 24, 2025. and LeanSearch (Gao et al., 2024)Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong, 2024. “A semantic search engine for Mathlib4”. arXiv:2403.13310. Both are semantic search engines, which means that they do not limit themselves to searching for literal matches in the text, but instead try to interpret the mathematical meaning of our query and compare it with the results in Mathlib. To do so, they use large language models (LLMs), which make it possible to establish relationships between statements even if they are formulated in different ways. In particular, they accept queries in the following formats (Gao et al., 2024)Guoxiong Gao, Haocheng Ju, Jiedong Jiang, Zihan Qin, and Bin Dong, 2024. “A semantic search engine for Mathlib4”. arXiv:2403.13310:
-
Descriptions in natural language
-
Names of known theorems
-
Mathematical notation (in LaTeX)
-
Lean code
For example, if in the previous case the idea of first proving x \neq 0 had not occurred to us, we could have searched Moogle for something like "division by itself is 1". In fact, the second result of this search in Moogle is:
Which is not the same result that exact? suggested, but it looks even simpler. We could go back to our example and write
example (x : ℝ) (hx : x > 0) :
x / x = 1 := x:ℝhx:x > 0⊢ x / x = 1
x:ℝhx:x > 0⊢ x ≠ 0
After which we would only need to prove that x \neq 0.
In general, I have found that LeanSearch works better than Moogle, especially in terms of the relevance of the results obtained. However, at the beginning of the project I only knew about Moogle, and I discovered LeanSearch later, so I have mostly used Moogle.
An example of a real search I needed for this work in LeanSearch was "subset of set has at most the dimension of the set".
The first result that appears is exactly the one I needed. However, before searching for it I had no idea how to formalise the results I was working on, especially because I was not familiar with the Cardinal module. This was a clear example of how these tools give access to parts of Mathlib that would otherwise be hard to locate.
Altogether, tools such as exact?, LeanSearch or Moogle have been fundamental in making the formalisation process more efficient, allowing one to rely on Mathlib effectively without needing to know it in depth from the start.
2.4.6. Noncomputable and the axiom of choice
To finish this section on Lean in practice, it is useful to briefly comment on a question that will appear in some of the later definitions: the use of the axiom of choice and the noncomputable keyword.
In Lean, the axiom of choice is introduced in the following way:
axiom choice {α : Sort u} : Nonempty α → α
That is, given a non-empty type, choice returns an element of that type, although it does not tell us how to find it. For this reason, its use prevents extracting computable information from the result.
Consequently, when we define functions or constructions that depend on choice, Lean forces us to mark them as noncomputable. An example is the choose function, which, given a proof of an existential type, selects a witness:
noncomputable def choose {α : Sort u} {p : α → Prop}
(h : ∃ x, p x) : α :=
(indefiniteDescription p h).val
We will often use choose (Classical.choose, since it is found in the Classical module) in our results, together with the following lemma
theorem choose_spec {α : Sort u} {p : α → Prop}
(h : ∃ x, p x) : p (choose h) :=
(indefiniteDescription p h).property
which is a proof that the element chosen through choose satisfies the properties we asked of it.
The use of noncomputable does not represent a problem for us (nor, in general, for the mathematical community), since in this work we are not interested in the constructions being computable: we work with them from a logical and mathematical point of view, not an algorithmic one.
Moreover, using the axiom of choice has a practical advantage: when we use choose, the chosen element will always be the same (even if we do not know which one it is), and it will always have the property choose_spec. This makes it possible to work with it consistently within a proof and to refer to it several times as if it were a determined object.
In contrast, another way of obtaining a witness from a proof of existence is to use the obtain tactic, which is used in the following way:
example : (∃ n : ℕ, n > 3) → ∃ m : ℕ, m > 2 := by intro h -- h : ∃ n : ℕ, n > 3 obtain ⟨n, hn⟩ := h -- n : ℕ, hn : n > 3 ...
The fundamental difference between using the axiom of choice and using obtain is that two witnesses obtained through obtain from the same type (for example of type ∃ n : ℕ, n > 3) will not necessarily be equal, whereas if they were obtained through Classical.choose they will always be equal.