# Zulip Chat Archive

## Stream: general

### Topic: Logic & Proof

#### Kaushik Chakraborty (Jun 07 2018 at 09:42):

Hi, I am going through the online course Logic and Proof. I am stuck in the exercises. Is this the right place to ask such questions?

#### Chris Hughes (Jun 07 2018 at 09:44):

Yes

#### Kaushik Chakraborty (Jun 07 2018 at 09:50):

Thanks. So I'm stuck progressing with the last prob. of Chapter 4's exercises i.e. prove `¬ (A ↔ ¬ A)`

#### Kaushik Chakraborty (Jun 07 2018 at 09:52):

I am thinking of following the rules mentioned in the book till now and start with the assumption that `(A ↔ ¬ A)`

is true and then progress to show `false`

so that I can prove the negation. But I can't figure out a way forward

#### Kenny Lau (Jun 07 2018 at 09:53):

hint: prove `¬ A`

from your assumption

#### Chris Hughes (Jun 07 2018 at 09:58):

This actually came up in M1F, and I was annoyed with myself for assuming excluded middle.

#### Kenny Lau (Jun 07 2018 at 09:58):

not constructive enough, eh :P

#### Kaushik Chakraborty (Jun 07 2018 at 10:02):

am failing to get how can I get `¬ A`

with just assuming `A ↔ ¬ A`

. I can get it if I also assume `A`

and apply left elimination to the iff to get `¬ A`

. Is my understanding correct ?

#### Kenny Lau (Jun 07 2018 at 10:02):

no, you need to assume `A`

and prove `false`

#### Kenny Lau (Jun 07 2018 at 10:03):

ok, which you get via deducing `¬ A`

#### Chris Hughes (Jun 07 2018 at 10:05):

Try `have h : ¬ A`

#### Kaushik Chakraborty (Jun 07 2018 at 10:05):

I am trying to do something like that but I am getting a type mismatch error coz of the additional assumption.

Could you please look at this LEAN code

#### Chris Hughes (Jun 07 2018 at 10:07):

You can only do `assume a : A`

if your goal is `A → something`

#### Chris Hughes (Jun 07 2018 at 10:07):

Have you used `have`

before?

#### Kenny Lau (Jun 07 2018 at 10:08):

variables A : Prop example : ¬ (A ↔ ¬ A) := assume h, have h1 : ¬ A, from _, show false, from _

#### Kenny Lau (Jun 07 2018 at 10:08):

so your code should look like this

#### Kaushik Chakraborty (Jun 07 2018 at 10:12):

yeah that's what I am trying but could not think of any intro/elim rule to apply to get `¬ A`

from `h`

#### Moses Schönfinkel (Jun 07 2018 at 10:15):

The biggest hint here was the innocuous sentence "...and I was annoyed with myself for assuming excluded middle" :). You can't conjure `not A`

from thin air, but you *can* conjure something almost as good.

#### Kaushik Chakraborty (Jun 07 2018 at 10:19):

Ok I think I got it

variables A : Prop example : ¬ (A ↔ ¬ A) := assume h, have h1 : ¬ A, from assume a : A, show false, from (h.mp a) a, show false, from h1 (h.mpr h1)

#### Kaushik Chakraborty (Jun 07 2018 at 10:20):

thanks a lot for the guidance

#### Kaushik Chakraborty (Jul 19 2018 at 07:25):

Hello again. I want to do the exercise 17.1 of the course on proving the equivalence of *principle of complete induction* to *principle of least element* in Lean. So in that regard does the following setup make sense? I still need to do the actual proof.

variable P : ℕ → Prop example : ∀ n, (∀ m, m < n ∧ P(m) → P(n)) → ∀ x, P(x) ↔ ∀ n, P(n) ∧ ∃ m x, m < n ∧ ¬ (x < m) → P(m) := sorry

#### Mario Carneiro (Jul 19 2018 at 07:38):

the parentheses seem to be off in a few places

#### Mario Carneiro (Jul 19 2018 at 08:00):

I think this is correct with minimal parentheses:

variable P : ℕ → Prop example : ((∀ n, (∀ m, m < n → P m) → P n) → ∀ x, P x) ↔ ∀ n, P n → ∃ m, P m ∧ ∀ x, x < m → ¬ P x := sorry

#### Mario Carneiro (Jul 19 2018 at 08:03):

the statement of the principle of least element you gave looks really weird and is probably incorrect - I've changed the statement a bit

#### Mario Carneiro (Jul 19 2018 at 08:04):

I expect it to say something like "if P(n) for some n, then there exists an m such that P(m), and ¬ P(x) for all smaller x"

#### Johan Commelin (Jul 19 2018 at 08:07):

The current statement reads to me as "I can prove `P`

by induction iff the principle of least element holds for `P`

"

#### Mario Carneiro (Jul 19 2018 at 08:12):

My point is that the right hand side doesn't look like the PLE to me

#### Johan Commelin (Jul 19 2018 at 08:14):

Oooh, you are completely right. The right hand side should start with `\exists`

. As stated it is trivial: take `m = 0`

.

#### Mario Carneiro (Jul 19 2018 at 08:14):

Also, I don't think this will actually work (unless you prove both sides individually), since the traditional reduction of induction to PLE and vice versa involves negating P

#### Mario Carneiro (Jul 19 2018 at 08:15):

this can be rectified by quantifying P individually on each side:

example : (∀ P : ℕ → Prop, (∀ n, (∀ m, m < n → P m) → P n) → ∀ x, P x) ↔ ∀ (P : ℕ → Prop) n, P n → ∃ m, P m ∧ ∀ x, x < m → ¬ P x := sorry

#### Kaushik Chakraborty (Jul 19 2018 at 08:17):

Ok. I got the formalization of PLE. Thanks

#### Kaushik Chakraborty (Jul 19 2018 at 08:20):

although in your formalization of PLE, there is no relation between `n`

and `m`

. Shouldn't we mention that `m < n`

?

#### Mario Carneiro (Jul 19 2018 at 08:28):

There is no need, in the same way that there is no relation between n and x in the statement of induction

#### Mario Carneiro (Jul 19 2018 at 08:29):

You can prove, given the conclusion, that `m <= n`

, but it is possible that `m = n`

if `n`

is already the minimal witness

#### Mario Carneiro (Jul 19 2018 at 08:30):

another way to bracket it is `∀ (P : ℕ → Prop), (∃ n, P n) → ∃ m, P m ∧ ∀ x, x < m → ¬ P x`

#### Kaushik Chakraborty (Jul 19 2018 at 08:32):

Ok got it.

#### Kaushik Chakraborty (Jul 23 2018 at 09:25):

I'm stuck at this simple proof. how do I go from `n * n < m * m`

to `n ^ 2 < m ^2`

open nat variables n m : ℕ example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 := assume h, have n * n < n * m, from mul_lt_mul_of_pos_left h.right h.left, have n * m < m * m, from mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right), have n * n < m * m, from lt_trans ‹ n * n < n * m › ‹ n * m < m * m ›, sorry

#### Kenny Lau (Jul 23 2018 at 09:32):

open nat variables n m : ℕ example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 := assume h, calc n ^ 2 = nat.pow n 2 : by dsimp [(^)]; refl ... = 1 * (n * n) : nat.mul_assoc 1 n n ... = n * n : nat.one_mul _ ... < n * m : mul_lt_mul_of_pos_left h.right h.left ... < m * m : mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right) ... = m ^ 2 : by simp [(^), nat.pow]

#### Kenny Lau (Jul 23 2018 at 09:33):

@Mario Carneiro why can't I replace `by dsimp [(^)]; refl`

with `rfl`

?

#### Chris Hughes (Jul 23 2018 at 09:34):

Definitional equality is not transitive.

#### Kenny Lau (Jul 23 2018 at 09:34):

but then why does this work?

#### Kenny Lau (Jul 23 2018 at 09:34):

example : n ^ 2 = nat.pow n 2 := rfl

#### Kenny Lau (Jul 23 2018 at 09:35):

Definitional equality is not consistent either?

#### Kaushik Chakraborty (Jul 23 2018 at 09:37):

thanks @Kenny Lau . I still don't understand tactics. Maybe the theorem proving in lean course will help. Logic and Proof course have few mentions of tactics.

#### Johan Commelin (Jul 23 2018 at 09:42):

Kaushik, to answer your original question, there is `pow_two`

which you can use to rewrite between `n * n`

and `n^2`

.

#### Kenny Lau (Jul 23 2018 at 09:42):

it's not available without further import though

#### Johan Commelin (Jul 23 2018 at 09:51):

Right, you need to import `algebra.group_power`

, I think.

#### Kaushik Chakraborty (Jul 23 2018 at 10:37):

thanks @Johan Commelin. but am still not sure how to use `pow_two`

in my proof. I think I have to use `rewrite`

tactic but not sure how. Here is how I've changed my earlier proof

import algebra.group_power open nat variables n m : ℕ example : 0 < n ∧ n < m → n ^ 2 < m ^ 2 := assume h, have n * n < n * m, from mul_lt_mul_of_pos_left h.right h.left, have n ^ 2 < n * m, by sorry, have n * m < m * m, from mul_lt_mul_of_pos_right h.right (lt_trans h.left h.right), have n * m < m ^ 2, by sorry, lt_trans ‹ n ^ 2 < n * m › ‹ n * m < m ^ 2 ›

#### Johan Commelin (Jul 23 2018 at 10:41):

example (n : ℤ) : n ^ 2 = n * n := begin rewrite pow_two end

#### Kenny Lau (Jul 23 2018 at 10:43):

example (n : ℤ) : n ^ 2 = n * n := pow_two n

#### Kaushik Chakraborty (Jul 23 2018 at 10:53):

yeah I got the function usage part but how do I use `pow_two`

when I've the `lt`

relation i.e. replace sorry in `have n ^ 2 < n * m, by sorry`

when I've established `n * n < n * m`

. Or I'm approaching it wrong ?

#### Kevin Buzzard (Jul 23 2018 at 19:31):

You should be able to do this with `rw`

#### Kevin Buzzard (Jul 23 2018 at 19:39):

import algebra.group_power example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := begin have H : n ^ 2 = n * n := pow_two n, rw H, exact h end

#### Kevin Buzzard (Jul 23 2018 at 19:39):

You should also be able to do it with `eq.subst`

but I can never ever ever for the life of me get it to work.

#### Kenny Lau (Jul 23 2018 at 19:39):

`\t`

#### Kevin Buzzard (Jul 23 2018 at 19:40):

import algebra.group_power example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h

[doesn't work]

#### Kevin Buzzard (Jul 23 2018 at 19:40):

Can you fix it Kenny?

#### Kenny Lau (Jul 23 2018 at 19:41):

I think you would like `by convert h`

#### Kenny Lau (Jul 23 2018 at 19:42):

import algebra.group_power example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := have H : n * n = n ^ 2, from eq.symm $ pow_two n, H ▸ h

#### Kenny Lau (Jul 23 2018 at 19:43):

I'm not sure why your original version doesn't work

#### Kenny Lau (Jul 23 2018 at 19:43):

import algebra.group_power example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := by convert h; from pow_two n

#### Kevin Buzzard (Jul 23 2018 at 19:44):

example (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := ((((pow_two n).symm : n * n = n ^ 2) ▸ (h : n * n < n * m)) : n ^ 2 < n * m)

#### Kenny Lau (Jul 23 2018 at 19:44):

:o

#### Kevin Buzzard (Jul 23 2018 at 19:44):

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables n ^ 2 < n * m

#### Kevin Buzzard (Jul 23 2018 at 19:44):

I see no metavariables!

#### Kenny Lau (Jul 23 2018 at 19:44):

yeah I'm puzzled too

#### Chris Hughes (Jul 23 2018 at 19:44):

`example (m n : ℤ) (h : n * n < n * m) : n ^ (2 : ℕ) < n * m := (pow_two n).symm ▸ h`

#### Kenny Lau (Jul 23 2018 at 19:44):

...

#### Chris Hughes (Jul 23 2018 at 19:44):

works

#### Kevin Buzzard (Jul 23 2018 at 19:44):

...

#### Kevin Buzzard (Jul 23 2018 at 19:45):

The well-known metavariable `2`

#### Kevin Buzzard (Jul 23 2018 at 19:48):

invalid 'eq.subst' application, elaborator has special support for this kind of application (it is handled as an "eliminator"), but expected type must not contain metavariables @has_lt.lt.{0} int int.has_lt (@has_pow.pow.{0 ?l_1} int ?m_2 ?m_3 n (@bit0.{?l_1} ?m_2 ?m_4 (@has_one.one.{?l_1} ?m_2 ?m_5))) (@has_mul.mul.{0} int int.has_mul n m)

#### Kevin Buzzard (Jul 23 2018 at 19:48):

Indeed there was a metavariable

#### Chris Hughes (Jul 23 2018 at 19:48):

This works `lemma thing (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h`

#### Kenny Lau (Jul 23 2018 at 19:49):

?????????????????

#### Chris Hughes (Jul 23 2018 at 19:49):

not this though `def thing (m n : ℤ) (h : n * n < n * m) : n ^ 2 < n * m := (pow_two n).symm ▸ h`

#### Kevin Buzzard (Jul 23 2018 at 19:50):

I think this is a bug in `pow_two`

-- the inbuilt `2`

is a nat

#### Kevin Buzzard (Jul 23 2018 at 19:51):

Clearly pow_two should be a definition not a theorem

#### Kevin Buzzard (Jul 23 2018 at 19:51):

Or am I barking up the wrong tree ;-)

#### Kenny Lau (Jul 23 2018 at 19:52):

I agree. Split the definition into more cases for easier definitional equality.

#### Chris Hughes (Jul 23 2018 at 19:52):

I don't think it has anything to do with `pow_two`

lemma two_add_three : 2 + 3 = 5 := add_comm 0 5 ▸ rfl -- works example : 2 + 3 = 5 := add_comm 0 5 ▸ rfl -- doesn't work

#### Kevin Buzzard (Jul 23 2018 at 20:10):

`example : (2 : ℕ) + 3 = 5 := add_comm 0 5 ▸ rfl -- works`

#### Kevin Buzzard (Jul 23 2018 at 20:11):

So the bit where it says "Ok I can't figure out the type of this `2`

thing, let's let it be `nat`

just so we can get on" is not occurring in the `example`

s

#### Kevin Buzzard (Jul 23 2018 at 20:11):

Maybe `pow_two`

should have been an example. Wait...

#### Mario Carneiro (Jul 23 2018 at 23:50):

The reason that `example`

and `def`

fail while `theorem`

succeeds is due to the separation of statement and proof done with `theorem`

#### Mario Carneiro (Jul 23 2018 at 23:51):

Remember how I mentioned a long time ago that `nat`

is the default type for numerals but it occurs very late in the elaboration? It's basically the last resort if there is a numeral of indeterminate type

#### Mario Carneiro (Jul 23 2018 at 23:54):

In regard to this example, what happens is that since `def`

/`example`

allows the statement and proof to be elaborated together, it checks the proof to see if that will give a hint what is alpha in `(2:alpha) + 3 = 5`

. But that means that when it hits the `eq.subst`

it will still have a lingering metavariable. In the `theorem`

case, there is no information to be had, since the proof doesn't contribute to elaborating the statement, so it goes with the default `nat`

type for numerals. Then when it elaborates the proof, there are no metavariables

#### Kaushik Chakraborty (Jul 24 2018 at 23:29):

For this code in the LEAN live in-browser IDE

import algebra.group_power theorem thing (m n : ℕ) (h : n * n < n * m) : (n ^ 2 < n * m) := (pow_two n).symm ▸ h

am getting following error

"eliminator" elaborator type mismatch, term h has type n * n < n * m but is expected to have type n ^ 2 < n * m Additional information: /test.lean:2:82: context: the inferred motive for the eliminator-like application is λ (_x : ℕ), n ^ 2 < n * m

#### Kevin Buzzard (Jul 24 2018 at 23:33):

Join the `▸`

-haters club!

#### Kevin Buzzard (Jul 24 2018 at 23:34):

Sometimes the issue is that higher-order unification is undecidable, sometimes I've just made a silly mistake.

#### Chris Hughes (Jul 24 2018 at 23:36):

The mistake here is that `pow_two`

is a theorem about `monoid.pow`

and not `nat.pow`

#### Kevin Buzzard (Jul 24 2018 at 23:36):

yes, I just realised that when trying to solve without the triangle

#### Kevin Buzzard (Jul 24 2018 at 23:36):

invalid type ascription, term has type @has_lt.lt nat nat.has_lt (@has_pow.pow nat nat (@monoid.has_pow nat nat.monoid) n 2) (@has_mul.mul nat nat.has_mul n m) but is expected to have type @has_lt.lt nat nat.has_lt (@has_pow.pow nat nat nat.has_pow n 2) (@has_mul.mul nat nat.has_mul n m)

#### Kevin Buzzard (Jul 24 2018 at 23:41):

theorem nat.pow_two (a : ℕ) : a ^ 2 = a * a := show (1 * a) * a = a * a, by rw one_mul theorem thing (m n : ℕ) (h : n * n < n * m) : (n ^ 2 < n * m) := (nat.pow_two n).symm ▸ h

#### Kaushik Chakraborty (Jul 25 2018 at 00:33):

thanks @Kevin Buzzard this worked. however, I have some doubts about the `nat.pow_two`

theorem. In your proof, you showed a different equality than what is in the sig. of the theorem. Is Lean somehow guessing the fact that `(1 * a) * a = a ^ 2`

. Or how is the rewrite tactics working here?

#### Nicholas Scheel (Jul 25 2018 at 01:04):

that’s obtained by unfolding the definition of `pow`

, which basically is that `n^a = (((1*n)*n)*...)*n`

(with `a`

`n`

s of course)

#### Kaushik Chakraborty (Jul 25 2018 at 08:05):

got it. thanks, @Nicholas Scheel

#### Kevin Buzzard (Jul 25 2018 at 09:04):

Yes, there are two kinds of equality in Lean. There's "equal by definition" and "equal because of a theorem". `a^2=1*a*a`

is true by definition of `^`

(you can discover this sort of thing by continually unfolding everything -- switch off notation and just get unfolding in tactic mode and see where you go) but `1*a=a`

is true because of a theorem. Things that are equal by definition you can just use interchangeably (I used `show`

to change the goal to a goal which Lean thinks is the same goal by definition), but then I used a rewrite to apply the theorem.

#### Kaushik Chakraborty (Aug 09 2018 at 00:22):

I am trying to attempt a Lean proof of quotient-remainder theorem shown here and, as usual, clueless on the approach. I've tried to chalk out a rough skeleton of the proof based on my understandings from an earlier chapter on doing induction in Lean & some exploration of Lean's types and functions. Does it make sense?

open int open nat -- quotient / remainder theorem theorem qt (n m q r : ℤ) : m > 0 → n = m * q + r ∧ (0 ≤ r ∧ r < m) := assume h, show (n = m * q + r) ∧ (0 ≤ r ∧ r < m), from int.rec_on n (assume k, show (of_nat k = m * q + r) ∧ ( 0 ≤ r ∧ r < m ), from nat.rec_on k (show (of_nat 0 = m * q + r) ∧ (0 ≤ r ∧ r < m), from sorry) (assume k ih, show of_nat (succ k) = m * q + r ∧ (0 ≤ r ∧ r < m), from sorry) ) (assume k, have h11 : -of_nat (k + 1) = m * q + r, from sorry, have h22 : 0 ≤ r ∧ r < m, from sorry, ⟨ h11 , h22 ⟩)

#### Chris Hughes (Aug 09 2018 at 00:34):

The theorem isn't true. This says for all n m q r, ... Whereas you want `forall m n, exists q r,...`

#### Chris Hughes (Aug 09 2018 at 00:35):

the proof of this theorem in the lean library is a combination of `int.mod_add_div`

, `int.mod_lt`

and `int.mod_nonneg`

.

#### Kaushik Chakraborty (Aug 09 2018 at 05:07):

Oh, thanks for clarifying. Does this theorem statement make sense?

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, (n = m * q + r) ∧ (0 ≤ r ∧ r < m) := sorry

#### Kaushik Chakraborty (Aug 09 2018 at 07:07):

I tried to solve the above statement with the functions you mentioned but I could not figure out how to come up with the existential terms `q`

& `r`

from `n`

and `m`

and hence the proof does not type check. I must be formulating the theorem statement wrong or missing some approach in the proof.

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) := assume n m h, assume q r, assume h2 : q = n / m, assume h1 : r = n % m, have HH: n = m * q + r, from calc n = n % m + m * (n / m) : by rw [int.mod_add_div] ... = r + m * (n / m) : by rw h1 ... = r + (m * q) : by rw h2 ... = (m * q) + r : by rw add_comm, have HH1: 0 ≤ r, from calc 0 ≤ n % m : int.mod_nonneg n (ne_of_gt h) ... ≤ r : by rw h1, have HH2: r < m, from calc r = n % m : by rw h1 ... < abs m : int.mod_lt n (ne_of_gt h) ... = m : abs_of_pos h, exists.intro q (exists.intro r (and.intro HH (and.intro HH1 HH2) ))

#### Mario Carneiro (Aug 09 2018 at 07:12):

This is an incorrect use of the `assume`

keyword. `assume`

is used *only* for proving a forall or pi or implication, and it introduces a variable with the type specified in the domain. To prove an existential, you use `exists.intro`

and provide the witness you want

#### Mario Carneiro (Aug 09 2018 at 07:14):

So after `assume n m h,`

you should write `exists.intro (n / m) $ exists.intro (n % m) $`

instead of `assume q r, assume h2 : q = n / m, assume h1 : r = n % m,`

#### Mario Carneiro (Aug 09 2018 at 07:14):

(The dollar signs are to save on having to close parentheses at the end of the proof)

#### Mario Carneiro (Aug 09 2018 at 07:15):

After that, `q`

and `r`

will no longer be present in the statement, so you won't need to rewrite with `h1`

anymore

#### Kaushik Chakraborty (Aug 09 2018 at 08:03):

I knew what was wrong with that *assume* but your tip on the `exists.intro`

was helpful. Here's my updated proof which type checks

theorem qt : ∀ n m : ℤ, m > 0 → ∃ q r : ℤ, n = m * q + r ∧ (0 ≤ r ∧ r < m) := assume n m h, exists.intro (n / m) $ exists.intro (n % m) $ have HH: n = m * (n / m) + (n % m), from calc n = n % m + m * (n / m) : by rw [int.mod_add_div] ... = m * (n / m) + (n % m) : by rw add_comm, have HH1: 0 ≤ (n % m), from int.mod_nonneg n (ne_of_gt h), have HH2: (n % m) < m, from calc (n % m) < abs m : int.mod_lt n (ne_of_gt h) ... = m : abs_of_pos h, ⟨ HH , ⟨ HH1 , HH2 ⟩ ⟩

#### Olivier de G. (Feb 29 2020 at 06:57):

I am working on exercice 2 of Chapter 2. The exercise states that the first clue can be represented as

$((FA \lor SA) \rightarrow (MW \lor DW)) \land ((MA \lor DA) \rightarrow (FW \lor SW))$

Should the implications be replaced with iff as follows ?

$((FA \lor SA) \leftrightarrow (MW \lor DW)) \land ((MA \lor DA) \leftrightarrow (FW \lor SW))$

#### Olivier de G. (Feb 29 2020 at 07:01):

Humm maybe it's actually equivalent because of

$FW \lor SW \lor MW \lor DW$

and

$FA \lor SA \lor MA \lor DA$

#### Kevin Buzzard (Feb 29 2020 at 11:17):

I think you're right. Both interpretations are valid translations of the sentence and. as you say, both are equivalent in the context (but of course they are not equal).

This is a common theme I guess. I found it interesting watching computer scientists claiming that they had proved there were infinitely many primes by showing that given a finite set of primes, they could find a prime not in this set. I initially thought "that's not what infinite means" but then I realised that actually it's a perfectly reasonable way of formalising it ("no finite set of primes is all the primes") and actually I didn't really know what infinite meant -- there are several definitions of infinite, all equivalent, but not at all equal, and one has to make a choice at some point.

Last updated: May 15 2021 at 23:13 UTC