Span of finite set is sequentially closed

Stream: maths

[Lambert A'Campo]

I am trying to prove the following lemma

open metric set

variables
{V : Type*} [normed_group V] [normed_space ℝ V]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
  sorry,
end

Is this somewhere in mathlib? If not, how can you induct on the cardinality of A?

[Kevin Buzzard]

It might be in there -- @Sebastien Gouezel ? Oh, I just remembered he's giving a talk in Orsay right now ;-)

If it's not then maybe this is a useful induction procedure for you:

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
  intro h,
  apply finite.induction_on h,
  sorry, sorry
end

[Lambert A'Campo]

So it turns out it is actually in mathlib!

variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
{E : Type u} [normed_group E] [normed_space 𝕜 E]
[complete_space 𝕜]

lemma submodule.closed_of_finite_dimensional (s : submodule 𝕜 E) [finite_dimensional 𝕜 s] :
  is_closed (s : set E)

but I'm not quite sure how to make lean transform this into what I need.

[Kevin Buzzard]

I guess you want to find the following facts:
(1) Closed implies sequentially closed [this will be proved near the definition of sequentially closed]
(2) the reals are a nondiscrete normed field [type class inference will handle this]
(3) the vector space spanned by a finite set is finite-dimensional [that will surely be there somewhere]

[Kevin Buzzard]

(2) is indeed there:

noncomputable example : nondiscrete_normed_field ℝ := by apply_instance

so you don't have to do anything -- type class inference will do it for you.

[Lambert A'Campo]

So we are this far

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
  intro h_fin,
  let S := (submodule.span ℝ A).carrier,
  apply is_seq_closed_of_is_closed S,

  apply submodule.closed_of_finite_dimensional,
end

but we get an error:
invalid apply tactic, failed to unify
is_closed S
with
is_closed ↑?m_6

[Lambert A'Campo]

I thought that this should reduce it to showing that submodule.span \R A is finite dimensional

[Kevin Buzzard]

Is there any possibility that you can post some fully working code?

[Kevin Buzzard]

I'm getting a bit sick of having to guess all the imports ;-)

[Lambert A'Campo]

Yes of course, sorry.

import analysis.normed_space.banach
import analysis.normed_space.basic
import linear_algebra.basic
import linear_algebra.basis
import linear_algebra.dimension
import linear_algebra.finite_dimensional
import topology.subset_properties
import set_theory.cardinal
import data.real.basic
import topology.sequences
import order.bounded_lattice
import analysis.specific_limits
import analysis.normed_space.finite_dimension

noncomputable theory
open_locale classical

open metric set

variables
{V : Type*} [normed_group V] [normed_space ℝ V]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
  intro h_fin,
  let S := (submodule.span ℝ A).carrier,
  apply is_seq_closed_of_is_closed S,

  apply submodule.closed_of_finite_dimensional,
end

[Kevin Buzzard]

Yeah. There might be a universe issue and also a typeclass issue.

[Kevin Buzzard]

#check @submodule.closed_of_finite_dimensional
/-
submodule.closed_of_finite_dimensional :
  ∀ {𝕜 : Type u_2} [_inst_1 : nondiscrete_normed_field 𝕜] {E : Type u_2} [_inst_2 : normed_group E]
  [_inst_3 : normed_space 𝕜 E] [_inst_6 : complete_space 𝕜] (s : submodule 𝕜 E)
  [_inst_7 : finite_dimensional 𝕜 ↥s], is_closed ↑s
-/

For some reason 𝕜 and E are supposed to be in the same universe in this lemma. This might be some subtlety that I don't know about, or it might be an error in mathlib.

[Kevin Buzzard]

-- we use linear equivs, which require all the types to live in the same universe
variables {𝕜 : Type u} [nondiscrete_normed_field 𝕜]
{E : Type u} [normed_group E] [normed_space 𝕜 E]
{F : Type v} [normed_group F] [normed_space 𝕜 F]

This is explicit design decision. I don't know what's going on here. This has consequences for you -- the reals have type Type so Lean expects your vector space also to have type Type.

[Kevin Buzzard]

But changing the variable to {V : Type} unmasks a new problem.

[Kevin Buzzard]

which is that type class inference cannot figure out why s is finite-dimensional.

[Kevin Buzzard]

variables
{V : Type} [normed_group V] [normed_space ℝ V]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
  intro h_fin,
  let S : set V := ↑(submodule.span ℝ A),
  apply is_seq_closed_of_is_closed S,
  exact @submodule.closed_of_finite_dimensional ℝ _ V _ _ _ _ sorry,
end

works, but there's a sorry

[Kevin Buzzard]

So what is left is the proof that S is finite-dimensional. Oh -- by the way -- in Lean there is a "canonical" way of doing many things, and your definition of S as (...).carrier is non-canonical: I changed it to the canonical way of writing this, with the little up-arrow.

[Kevin Buzzard]

variables {V : Type} [normed_group V] [normed_space ℝ V]

instance moo {V : Type} [normed_group V] [normed_space ℝ V] (A : set V) (hA : finite A) :
  finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
  sorry
end


lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (submodule.span ℝ A).carrier :=
begin
  intro h_fin,
  let S : set V := ↑(submodule.span ℝ A),
  apply is_seq_closed_of_is_closed S,
  exact @submodule.closed_of_finite_dimensional ℝ _ V _ _ _ _ (moo A h_fin),
end

There is this thing called type class inference, which mathematicians tend to push in all sorts of directions which it turns out that Lean 3 was not quite expecting, because computer scientists did not really know what mathematicians wanted to do with it. I can't actually get it to work in this situation (hence all the ridiculous _s and the moo in the lemma) but probably some fiddling around with priorities could fix this.

[Patrick Massot]

You should really change the statement to use the coercion.

[Kevin Buzzard]

Actually I see now that perhaps moo is a bad instance, because finite is not a typeclass which might mean that typeclass inference will not be able to find the hypothesis that A is finite. I am a bit out of my depth here.

However this is eventually resolved, the missing part of the argument is still the sorry above.

[Patrick Massot]

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V)

[Patrick Massot]

Needing this up-arrow in the statement is really painful, but we don't know how to avoid this. We explain a tiny variation on this issue in our perfectoid paper.

[Patrick Massot]

Exactly in the paragraph where we complain about Lean elaboration being not yet good enough for maths.

[Patrick Massot]

Then you can write:

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V) :=
begin
  intro h_fin,
  apply is_seq_closed_of_is_closed,
  haveI : finite_dimensional ℝ (submodule.span ℝ A) := sorry,
  exact submodule.closed_of_finite_dimensional _,
end

[Patrick Massot]

Where the sorry is still the same one, but there is no more Morse code @... _ _ _ _ _

[Kevin Buzzard]

Patrick do you understand why V has to have type Type?

[Patrick Massot]

It might be in there -- Sebastien Gouezel ? Oh, I just remembered he's giving a talk in Orsay right now ;-)

Yes, he was finishing his talk at that moment. It was very nice talk. He explained maths for 15 minutes, then propaganda for Sledgehammer for 30 minutes then 15 minutes about how simple type theory is unfortunately unbearable.

[Kevin Buzzard]

theorem finite_dimensional_of_finite_span {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
  finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
  sorry
end

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V) :=
begin
  intro h_fin,
  apply is_seq_closed_of_is_closed,
  haveI : finite_dimensional ℝ (submodule.span ℝ A) := finite_dimensional_of_finite_span h_fin,
  exact submodule.closed_of_finite_dimensional _,
end

I moved the sorry to a more respectable place.

[Patrick Massot]

He was a bit unfair to Lean though. He explained how Lean is harder to read than Isabelle by comparing tactic scripts on a white background with proof terms on a black background (using a video beamer making it impossible to read VScode's default dark theme).

[Patrick Massot]

I would rename that as finite_dimensional_span_of_finite.

[Patrick Massot]

And no, I don't know anything about universe issues.

[Kevin Buzzard]

but then did someone ask him the question about which system is more likely to be able to define the tangent space of a manifold, a trivial undergraduate thing?

[Kevin Buzzard]

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
  finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
  sorry
end

lemma finite_span_seq_closed (A : set V) : finite A → is_seq_closed (↑(submodule.span ℝ A) : set V) :=
begin
  intro h_fin,
  apply is_seq_closed_of_is_closed,
  haveI : finite_dimensional ℝ (submodule.span ℝ A) := finite_dimensional_span_of_finite h_fin,
  exact submodule.closed_of_finite_dimensional _,
end

[Patrick Massot]

He was very clear Isabelle/HOL is unusable for maths. And also very clear that any system giving him dependant type (and the type Type -> X) + Sledgehammer would make him quit Lean without thinking twice (which looks like a very sensible thing to do).

[Kevin Buzzard]

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
  finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
  apply finite_dimensional.of_fg,
  sorry
end

Now we need a finset from a finite set

[Kevin Buzzard]

He was very clear Isabelle/HOL is unusable for maths. And also very clear that any system giving him dependant type (and the type Type -> X) + Sledgehammer would make him quit Lean without thinking twice (which looks like a very sensible thing to do).

So we need to make a sledgehammer? Then he'll quit Lean for Lean.

[Patrick Massot]

Look at the discussion we are having. How could we say this software is usable if two non-beginners cannot prove finite_dimensional_span_of_finite within 10 seconds?

[Patrick Massot]

Of course we don't know the linear algebra part of the library, but this was Sébastien main point: sledgehammer makes knowing the library much much less important.

[Patrick Massot]

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

[Kevin Buzzard]

I see -- so this is the sort of thing which Sledgehammer does quickly?

[Kevin Buzzard]

Of course this result is easily provable, we just have to look through the library and learn the relevant parts (except that I need to leave the office in 10 minutes and I'm trying to finish a grant proposal before that ;-) )

[Wojciech Nawrocki]

sledgehammer makes knowing the library much much less important

I found this to be the nicest thing about sledgehammer in Isabelle, even more so than the fact that it gives you a proof. The generated snippet is a proof of the goal at hand, but more importantly it contains a list of lemmas which can be used to prove it. Effectively, it's like library_search on steroids, because it automatically finds relevant facts - you can look at the lemmas it found and use them to write a nicer proof.

[Kevin Buzzard]

Then what is our long-term plan for getting a sledgehammer for Lean?

[Gabriel Ebner]

Then what is our long-term plan for getting a sledgehammer for Lean?

Me moving to Amsterdam. :smile: I'll talk about the current status in January.

[Sebastien Gouezel]

Yes, he was finishing his talk at that moment. It was very nice talk. He explained maths for 15 minutes, then propaganda for Sledgehammer for 30 minutes then 15 minutes about how simple type theory is unfortunately unbearable.

I think that's a fair summary. I also said that Sledgehammer makes the learning curve much smoother in Isabelle/HOL than in Lean or COQ.

[Sebastien Gouezel]

He was a bit unfair to Lean though. He explained how Lean is harder to read than Isabelle by comparing tactic scripts on a white background with proof terms on a black background (using a video beamer making it impossible to read VScode's default dark theme).

The point is that, proof terms don't exist in Isabelle, and this proof in Isabelle would just have been done by automation without needing to think at all. While a tactic proof in Lean would not have been nicer than the term proof. So, I don't think I have been really unfair :)

[Rob Lewis]

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

I don't think that's fair at all, the higher order proving work that they're doing is great progress.

[Lambert A'Campo]

Thanks for the extensive discussion. So do I understand correctly that I cannot use this lemma unless R and V have the same type? I find this very strange.

[Lambert A'Campo]

When I try to prove this theorem I need to transform A : set V to A set ↥(submodule.span ℝ A)... How does that work?

theorem finite_dimensional_span_of_finite {V : Type} [normed_group V] [normed_space ℝ V] {A : set V} (hA : finite A) :
  finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
  apply finite_dimensional.of_fg,
  rw submodule.fg_def,
  existsi (A : set ↥(submodule.span ℝ A)),
end

[Kevin Buzzard]

Things which mathematicians think of as equal are perhaps not equal in type theory. The submodule.span has type submodule ℝ V and probably A has type set V, but when you start talking about the span as an abstract vector space you want A to be a subset of the span, so the span needs to become a type (the ↥) rather than a term, and then A needs to be changed from set V to set <the finite-dimensional space>.

[Kevin Buzzard]

I don't think that's fair at all, the higher order proving work that they're doing is great progress

I don't know anything about what they're doing. I looked at the website and it didn't seem to mention Lean. So the plan is their work + Gabriel will result in a sledgehammer for Lean? This makes me happy, I am somehow convinced that Gabriel can do anything :D

[Sebastien Gouezel]

So do I understand correctly that I cannot use this lemma unless R and V have the same type? I find this very strange.

Not the same type, the same universe. This is an issue with the linear algebra library, that requires vector spaces to be in the same universe to define linear equivalences between them. But in practice one can do all mathematics in a single universe, so this is not a real issue.

[Kevin Buzzard]

But in practice one can do all mathematics in a single universe, so this is not a real issue.

That is not the message we get from the CS people. They assure us that it is important that we be maximally universe polymorphic. Is there an actual reason why this design decision was made or was it just for convenience?

Clark Barwick gave a talk at Imperial yesterday and when he was talking about pyknotic sets he had to fix a strongly inaccessible cardinal. This is a point where one really cannot do mathematics in a single universe. Scholze's condensed sets are a variant of this which does not need the inaccessible cardinal, however Scholze ends up with a slightly different class of objects (and he has to jump through a lot of set-theoretic hoops, choosing uncountable cardinals with properties whose existence can be proved in ZFC). We have to make a decision about whether to follow Scholze's point of view or Barwick's, and Barwick's would be much easier to do in Lean, although his pyknotic sets will end up having type Type 1, so pyknotic vector spaces are not going to work in Lean.

[Mario Carneiro]

But in practice one can do all mathematics in a single universe, so this is not a real issue.

I think that should read "in principle one can do all mathematics in a single universe". In practice you run into exactly the issues that Lambert is noting. Do we have a comprehensive set of instances on ulift? (Including a ulift_instance tactic for making more instances.) If so, it might be possible to work around this by using ulift R as the scalar ring, but it's not a particularly natural solution to work with.

[Kevin Buzzard]

And what about the solution of making mathlib properly polymorphic? Why is it not polymorphic here?

[Sebastien Gouezel]

What prevents you from adding a large cardinal axiom and doing exactly his construction in Type? (Note that I wouldn't mind using the additional flexibility of type theory to simplify things, but my point is that everything you do in usual mathematics with set theory should be doable in Type).

[Kevin Buzzard]

What prevents you from adding a large cardinal axiom and doing exactly his construction in Type? (Note that I wouldn't mind using the additional flexibility of type theory to simplify things, but my point is that everything you do in usual mathematics with set theory should be doable in Type).

Nothing, I believe. Except then you'll have an extra axiom which somehow looks silly in Lean because it basically says "assume Type -1 exists".

[Kevin Buzzard]

The obvious response is "why not renumber?"

[Kevin Buzzard]

And to be honest if we're going to start using cardinal bounds then we may as well do it the Scholze way anyway, because proving the existence of an uncountable strong limit cardinal (a fun exercise for you Mario? ;-) ) will be possible in Lean without any extra axioms.

[Kevin Buzzard]

(what we need is an uncountable $\kappa$ such that $\lambda<\kappa\implies 2^{\lambda}<\kappa$)

[Kevin Buzzard]

(proof: define a sequence of cardinals $\kappa_\alpha$ for $\alpha$ an ordinal by $\kappa_0=\aleph_0$, $\kappa_{\alpha+1}=2^{\kappa_\alpha}$, and unions at limits; then $\kappa_\alpha$ for any (positive) limit ordinal will do the trick)

[Sebastien Gouezel]

I don't know where the root of polymorphism loss is, but dimension.lean starts with the line

variables {K : Type u} {V V₂ V₃ V₄ : Type v}

And since this file was written by Mario and Johannes I am pretty sure there is a very good reason for this.

[Sebastien Gouezel]

Probably when you have maps between these modules you want to compare their dimensions, which are cardinals in some fixed universe.

[Kevin Buzzard]

Probably you sometimes want to compare their dimensions, but you often do not? That's like saying that equiv should only take two types from the same universe because sometimes you might want to compare their cardinalities. That is not what is done there. I am confused.

[Sebastien Gouezel]

For instance

theorem linear_equiv.dim_eq (f : V ≃ₗ[K] V₂) :
  dim K V = dim K V₂

does not make sense if V and V_2 are not in the same universe, as their dimensions don't live in the same place.

[Kevin Buzzard]

So that one theorem could be formalised under the assumption that the universes are the same.

[Sebastien Gouezel]

That's the first statement that breaks in this file if I change the universe constraints, but there are many more below. But I agree with you that it would make sense to only assume the same universe when it is really necessary.

[Kevin Buzzard]

or some ulift nonsense could be added. There are ways around this and all I am saying is that I am surprised that this design decision was taken by people who take universe polymorphism so seriously.

[Kevin Buzzard]

Of course the Barwick example is very much an extreme case. I absolutely agree with you that 99% of modern maths can be done within one universe. I'm sure Lambert doesn't want to assume the existence of an inaccessible cardinal in his proof so he could change V to have type Type and not lose too much sleep about it.

Can the finite-dimensionality proof be made into an instance?

[Sebastien Gouezel]

Sorry, which proof?

[Kevin Buzzard]

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Span.20of.20finite.20set.20is.20sequentially.20closed/near/182481084

finite_dimensional is a class but finite is not.

[Kevin Buzzard]

Oh -- this does not even compile for me! I thought Lambert had done it!

[Kevin Buzzard]

sorry the proof for now :D

[Sebastien Gouezel]

It doesn't look like an instance. It could be one if you replaced your finite set by a finset, I guess.

[Mario Carneiro]

There are a few statements in there that require the universe restriction to typecheck, but I'm wary about having that be in the variables list because this is likely to carry the restriction through to other theorems that don't have the restriction

[Kevin Buzzard]

I'm pretty sure that Lambert's result doesn't need V to be in Type.

[Sebastien Gouezel]

In the dimension file, most of the statements require it, as they talk about dimensions as cardinals. However, when one uses these results to prove things on findim, this imposes the universe restriction in situations where it shouldn't be needed any more.

[Lambert A'Campo]

Oh -- this does not even compile for me! I thought Lambert had done it!

I have not haha. I just changed V : Type* to V:Type (I don't understand what this means anyways.) and I now I am just left with this nonsensical theorem that the span of a finite set is finite dimensional but I don't know how to prove it because I don't understand the coercion stuff.

[Lambert A'Campo]

I tried this but now I don't know how to prove things about B...

theorem finite_dimensional_span_of_finite {V : Type} {A : set V} [normed_group V] [normed_space ℝ V] (hA : finite A) :
  finite_dimensional ℝ ↥(submodule.span ℝ A) :=
begin
  apply finite_dimensional.of_fg,
  rw submodule.fg_def,
  let B : set ↥(submodule.span ℝ A) := {b | ∃ a : V, a ∈ A ∧ a = b},
  existsi B,
  sorry
end

[Patrick Massot]

Jasmin's project http://matryoshka.gforge.inria.fr/ was meant to solve this problem, but it doesn't seem to progress much :sad:

I don't think that's fair at all, the higher order proving work that they're doing is great progress.

I'm very sorry I wrote that too quickly. I was trying to help Lambert, report on Sébastien's talk and cook dinner for my kids in a 10 minutes time slot (on top of the frustration boost I get each time I see sledgehammer). I should have written that end users don't see any progress so far. But I understand there is foundational work to be done, and I'm very excited to read it's progressing (and Gabriel is helping).

[Sebastien Gouezel]

Something along the lines of

theorem finite_dimensional_of_finite_span {A : set V} (hA : set.finite A):
  finite_dimensional K (submodule.span K A) :=
begin
  apply is_noetherian_of_fg_of_noetherian,
  exact submodule.fg_def.2 ⟨A, hA, rfl⟩,
end

could help you.

[Kevin Buzzard]

Do we have to wait until January to hear the progress about Lean's sledgehammer?

[Kevin Buzzard]

Lambert -- you should come along to Xena and get educated by Imperial's undergraduates ;-)

[Lambert A'Campo]

Something along the lines of

theorem finite_dimensional_of_finite_span {A : set V} (hA : set.finite A):
  finite_dimensional K (submodule.span K A) :=
begin
  apply is_noetherian_of_fg_of_noetherian,
  exact submodule.fg_def.2 ⟨A, hA, rfl⟩,
end

could help you.

Thank you! That did it.

[Lambert A'Campo]

Lambert -- you should come along to Xena and get educated by Imperial's undergraduates ;-)

Yeah I want to come, I just didn't have time on Thursdays so far. But the unit ball compact -> finite dimensional proof is now complete !

[Floris van Doorn]

And to be honest if we're going to start using cardinal bounds then we may as well do it the Scholze way anyway, because proving the existence of an uncountable strong limit cardinal (a fun exercise for you Mario? ;-) ) will be possible in Lean without any extra axioms.

Mario already did this fun exercise:
https://github.com/leanprover-community/mathlib/blob/master/src/set_theory/cofinality.lean#L488

[Floris van Doorn]

Unless I misunderstand, and you want a strong limit ordinal in Type 0.

[Patrick Massot]

This certainly looks like a hole in mathlib (whose finite dimensional stuff is very sketchy). Shoud it be PRed? Probably something like:

variables (R : Type*) [comm_ring R] [is_noetherian_ring R]

theorem is_noetherian_span_of_finite {V : Type*} {A : set V} [add_comm_group V] [module R V] (hA : finite A) :
  is_noetherian R (submodule.span R A) :=
is_noetherian_of_fg_of_noetherian _ (submodule.fg_def.mpr ⟨A, hA, rfl⟩)


variables (K : Type*) [discrete_field K]

theorem finite_dimensional_span_of_finite {V : Type*} {A : set V} [add_comm_group V] [vector_space K V] (hA : finite A) :
  finite_dimensional K (submodule.span K A) :=
is_noetherian_span_of_finite K hA

PRed in noetherian.lean and finite_dimensional.lean

[Kevin Buzzard]

Oh that's totally the correct way to do it :-) Finitely-generated modules over a Noetherian ring are Noetherian, and hence finitely-generated vector spaces are finite-dimensional :D That's absolutely great :D My mind was muddied by the fact that they teach finite-dimensional vector spaces several years before Noetherian modules!

[Patrick Massot]

Seriously, that linear algebra library is really really hard to use. What Lambert was trying to do was completely natural, but ended up with had_coe_to_sort hell.

[Kevin Buzzard]

I think that if a part of the library is new to someone then they often find it hard to use.

[Patrick Massot]

In the topology part there is nothing that would get you stuck like Lambert was.

[Johan Commelin]

@Sebastien Gouezel Is there a recording of your talk? (With subtitles :grimacing:)

[Patrick Massot]

I think there will be video available soon (without subtitles).

[Patrick Massot]

I asked and immediately got a temporary url: https://webdiff.math.u-psud.fr/5de68f39862d2a0419e311ed

[Patrick Massot]

I have no idea why they kept the streams from cameras looking at the audience, especially since they were zooming on mostly empty areas of the lecture room.

[Johan Commelin]

Thanks for the link. I'll see if I can get anything out of it (-;