Zulip Chat Archive

Stream: condensed mathematics

Topic: sorry count

Johan Commelin (Mar 22 2021 at 15:21):

$ rg -l sorry | xargs -I % sh -c 'nsorry=`rg sorry % | wc -l`; echo -n "$nsorry\t%\n"'
1       src/normed_spectral.lean
3       src/lem97.lean
9       src/thm95/default.lean
15      src/thm95/constants.lean
5       src/thm95/double_complex.lean
3       src/toric/scarti_commentati.lean
5       src/toric/dual_extremal_API_sorry.lean
10      src/pseudo_normed_group/profinitely_filtered.lean
15      src/toric/toric.lean
4       src/polyhedral_lattice/cech.lean

Johan Commelin (Mar 22 2021 at 15:22):

Total: 70

Johan Commelin (Mar 22 2021 at 15:23):

The 1 sorry in normed_spectral will dissolve when we have semi_normed_groups

Johan Commelin (Mar 22 2021 at 15:23):

The 15 sorrys in thm95/constants will be fixed along the way, when we figure out the exact way the constants are increased during the proof of 9.5

Johan Commelin (Mar 22 2021 at 15:25):

The 10 sorrys in pseudo_normed_group/profinitely_filtered are setting up products of profinitely filtered pseudo normed groups. If you enjoy showing that a space (X^n)_c is comp Haus tot disc because it is canonically isomorphic to (X_c)^n (where the claim is obvious), then feel free to kill these sorrys.

Johan Commelin (Mar 22 2021 at 15:25):

The sorrys in toric/* are the territory of Damiano :smiley:

Johan Commelin (Mar 22 2021 at 15:26):

The sorrys in polyhedral_lattice/cech are tricky. We need to show that a certain quotient group is free abelian.

Damiano Testa (Mar 22 2021 at 15:56):

As for the sorrys that I own, I am not as good as "others", so not all are actually needed/useful and not everything that I would like is sorried, so the count there is somewhat inaccurate. However, now that the teaching term is over, I should have some time to clean up and make some progress!

Riccardo Brasca (Mar 22 2021 at 17:20):

When #6819 will be merged I can start the refactoring offor_mathlib/normed_group_quotient to add quotient by non closed subspace.

Johan Commelin (Apr 28 2021 at 08:29):

I think that two or three weeks ago we have > 70 sorry's in the repo. Now it's 47 :tada:

2       src/thm95/row_iso.lean
11      src/thm95/polyhedral_iso.lean
3       src/thm95/default.lean
1       src/thm95/double_complex.lean
1       src/locally_constant/NormedGroup.lean
4       src/pseudo_normed_group/profinitely_filtered.lean
3       src/polyhedral_lattice/basic.lean
4       src/polyhedral_lattice/cech.lean
2       src/for_mathlib/dfinsupp.lean
1       src/for_mathlib/Gordan.lean
5       src/for_mathlib/int_grading_lemma.lean
10      src/thm95/constants.lean

Johan Commelin (Apr 28 2021 at 08:29):

We are on the right track :big_smile:

Johan Commelin (Apr 28 2021 at 14:42):

Advertising some sorrys:

-- src/polyhedral_lattice/basic.lean
instance (Λ : Type*) [polyhedral_lattice Λ] : no_zero_smul_divisors ℤ Λ :=
sorry

Johan Commelin (Apr 28 2021 at 14:42):

and

-- src/polyhedral_lattice/cech.lean
@[to_additive]
def saturated (H : subgroup G) : Prop := ∀ ⦃n g⦄, gpow n g ∈ H → n = 0 ∨ g ∈ H

@[to_additive]
lemma closure_saturated (s : set G) (H : ∀ n g, gpow n g ∈ s → n = 0 ∨ g ∈ closure s) :
  (closure s).saturated :=
begin
  intros n g h,
  rw or_iff_not_imp_left,
  intro hn,
  sorry
end

Johan Commelin (Apr 28 2021 at 14:42):

In src/polyhedral_lattice/cech.lean there is another lemma about proving that a specific subgroup is saturated. I've stubbed out a proof, but there are still some sub-sorrys

Riccardo Brasca (Apr 28 2021 at 14:52):

I can do these later today

Johan Commelin (Apr 28 2021 at 14:59):

They are mostly math-trivial. But several of them are quite fiddly, I think.

Riccardo Brasca (Apr 28 2021 at 15:44):

Hmm... what is the proof of closure_saturated?

Riccardo Brasca (Apr 28 2021 at 15:44):

I mean, the math proof

Johan Commelin (Apr 28 2021 at 16:07):

Hmm, maybe I took a wrong turn there.

Johan Commelin (Apr 28 2021 at 16:07):

I guess it is true in free groups.

Johan Commelin (Apr 28 2021 at 16:07):

But maybe we should just not think about that, and try to find a different proof for L_saturated

Johan Commelin (Apr 28 2021 at 16:08):

I think we can write down an explicit basis of L f m.

Johan Commelin (Apr 28 2021 at 16:08):

But it will be a bit nasty.

Johan Commelin (Apr 28 2021 at 16:09):

And then we have to show that you can extend that basis to a basis of the full group. So that L f m splits off.

Riccardo Brasca (Apr 28 2021 at 16:53):

Let me think a little bit about closure_saturated. We need it for abelian groups, right?

Johan Commelin (Apr 28 2021 at 16:55):

Oh did I forget the commutativity assumption?? :face_palm:

Riccardo Brasca (Apr 28 2021 at 17:14):

Well. the definition makes sense in general :grinning:

Riccardo Brasca (Apr 28 2021 at 17:25):

Hm... what if we take $\{(1,2)\} \subseteq \mathbf{Z}^2$ ? The condition seems satisfied, but the generated subgroup is not saturated.

Riccardo Brasca (Apr 28 2021 at 17:47):

BTW instance (Λ : Type*) [polyhedral_lattice Λ] : no_zero_smul_divisors ℤ Λ is now sorry free.

Johan Commelin (Apr 28 2021 at 17:48):

Riccardo Brasca said:

Hm... what if we take $\{(1,2)\} \subseteq \mathbf{Z}^2$ ? The condition seems satisfied, but the generated subgroup is not saturated.

I think the subgroup generated by (1,2) will be saturated, right?

Riccardo Brasca (Apr 28 2021 at 17:52):

~~$2\cdot (1,1)$ is in the subgroup but $(1,1)$ is not~~. Saturated means that the quotient is torsion-free (if I didn't misunderstood everything).

Riccardo Brasca (Apr 28 2021 at 17:53):

Ops. OK, forget about this

Riccardo Brasca (Apr 29 2021 at 09:18):

I think I now have a counterexample: let $G = \mathbf{Z}^2$ and let $S = \{s_1, s_2\}$ , where $s_1=(1,1)$ and $s_2=(1,3)$ . The assumption in closure_saturated is satisfied since if $k \cdot(a,b) = s_i$ , for $i=1,2$ , then $ka = 1$ , so $k = \pm 1$ and $(a,b) = \pm s_i \in \langle S \rangle$ . Now $s_1+s_2=(1,1)+(1,3)=(2,4)=2\cdot(1,2) \in \langle S \rangle$ . If $(1,2) \in \langle S \rangle$ , then there would be $x,y \in \mathbf{Z}$ such that $(1,2) = x \cdot s_1 + y \cdot s_2 = x \cdot (1,1) + y \cdot (1,3) = (x+y,x+3y)$ , so $y = 1-x$ and $2 = -2x + 3$ , that is impossible. So $\langle S \rangle$ is not saturated.

Johan Commelin (Apr 29 2021 at 11:24):

@Riccardo Brasca Hmm, good example. So we can throw that lemma away.

Johan Commelin (Apr 29 2021 at 11:24):

The thing we care about is L_saturated

Johan Commelin (Apr 29 2021 at 12:15):

@Riccardo Brasca Do you have an idea how to attack L_saturated? Otherwise I'll start thinking about it.

Johan Commelin (Apr 29 2021 at 12:15):

And sorry for taking that wrong turn...

Peter Scholze (Apr 29 2021 at 12:15):

Can you remind me of the precise statement you need here?

Johan Commelin (Apr 29 2021 at 12:18):

We have $\Lambda^{(m)} := (\Lambda')^m / L_m$ , and to prove that this if finite free, we need to show that $L_m$ is saturated.

Johan Commelin (Apr 29 2021 at 12:18):

So, I think you said some time in the past that it might be best to show that $L_m$ splits off from $(\Lambda')^m$ .

Johan Commelin (Apr 29 2021 at 12:19):

But now we need to figure out how to execute that in practice.

Riccardo Brasca (Apr 29 2021 at 12:19):

To be honest I forgot what L f m means :sweat_smile: I tried the other lemma since it didn't use complicated objects... but let me have a look at it

Johan Commelin (Apr 29 2021 at 12:19):

Ooh, no worries. I can also look at this one.

Johan Commelin (Apr 29 2021 at 12:19):

In Lean

def Lset : set (fin m →₀ Λ') :=
{x | ∃ (l : Λ) (n : fin m →₀ ℤ) (hn : n.sum (λ _, add_monoid_hom.id _) = 0),
     x = finsupp.map_range_hom (int.cast_add_hom' (f l)) n}

def L : add_subgroup (fin m →₀ Λ') := add_subgroup.closure $ Lset f m

Johan Commelin (Apr 29 2021 at 12:20):

Here f is an arbitrary map $\Lambda \to \Lambda'$ with saturated image.

Johan Commelin (Apr 29 2021 at 12:21):

We can't really write $L_m := (\Lambda \otimes \Z^m)_{\Sigma = 0}$

Johan Commelin (Apr 29 2021 at 12:21):

That would require internal tensor products of submodules (additive subgroups actually, in this Lean code).

Peter Scholze (Apr 29 2021 at 12:21):

How hard is it to prove that the map $\Lambda\to \Lambda'$ splits (as abelian groups)?

Johan Commelin (Apr 29 2021 at 12:21):

We don't have that yet, so I gave a hands on definition of Lset.

Johan Commelin (Apr 29 2021 at 12:23):

In the actual application, where $\Lambda' = \Lambda^N$ , it shouldn't be hard. So here we can just assume it.

Peter Scholze (Apr 29 2021 at 12:23):

I would have thought that knowing this splitting should make the desired result quite easy, as one would get an explicit splitting of $\Lambda'^m/L_m$ into $\Lambda'^m$

Johan Commelin (Apr 29 2021 at 12:24):

With splitting, you just mean a map $g : \Lambda' \to \Lambda$ , right? Or a direct sum decomposition?

Peter Scholze (Apr 29 2021 at 12:24):

A map $g$ such that $\Lambda\to \Lambda'\to \Lambda$ is the identity

Johan Commelin (Apr 29 2021 at 12:25):

Right. I agree that if we have such a map, then showing that the range of f is saturated shouldn't be Lean-hard.

Johan Commelin (Apr 29 2021 at 12:31):

Hmm, does this lead to a different definition of $L_m$ ?

Johan Commelin (Apr 29 2021 at 12:31):

I wouldn't mind swapping out the current definition. It's not that pleasant to work with.

Peter Scholze (Apr 29 2021 at 12:33):

That's not what I mean; I mean that $\Lambda'^m/L_m$ should also inject into $\Lambda'^m$ . Let me see... take the map $\Lambda'^m\to \Lambda'^m$ given by $(\lambda_1',\ldots,\lambda_m')\mapsto (\lambda_1'-fg(\lambda_1')+a,\lambda_2'-fg(\lambda_2')+a,\ldots,\lambda_m'-fg(\lambda_m')+a)$ where $a=fg(\lambda_1'+\ldots+\lambda_m')$ . Then this vanishes on $L_m$ : On $L_m$ , all $\lambda_i'$ come from $\lambda_i\in \Lambda$ , and $fg$ doesn't do anything to them, so the map is $(\lambda_1,\ldots,\lambda_m)\mapsto (a,\ldots,a)$ , and $a=0$ on $L_m$ . The kernel is in fact exactly $L_m$ : On the kernel, all $\lambda_i'=fg(\lambda_i')-a\in \Lambda$ , and then $a=0$ shows that they are in $L_m$ .

So indeed $\Lambda'^m/L_m$ injects into $\Lambda'^m$ and hence is torsion-free.

Johan Commelin (Apr 29 2021 at 12:34):

Thanks!

Johan Commelin (Apr 29 2021 at 12:35):

So one could define $L_m$ to be that kernel. But it's not clear to me that this will make the "Cech" part of the construction easier.

Johan Commelin (Apr 29 2021 at 12:35):

So maybe we should stick to the current definition for now, and formalize your argument.

Peter Scholze (Apr 29 2021 at 12:36):

Sounds good to me.

Kevin Buzzard (Apr 29 2021 at 12:43):

Related: at some point I will need that if $\Lambda$ is a finite free $\Z$ -module of rank $n+1$ and $\phi:\Lambda\to\Z$ is non-zero then the kernel is finite free of rank $n$ . I've been putting this off because I am dimly aware that Anne is refactoring is_basis (in fact I've also been putting off a ton of completely trivial things about finite free $\Z$ -modules -- anything that involves rank basically -- for the same reason).

Johan Commelin (Apr 29 2021 at 13:05):

So this is the correct lemma, instead of that closure_saturated:

lemma add_subgroup.ker_saturated [no_zero_smul_divisors ℤ G₂] (f : G₁ →+ G₂) :
  (f.ker).saturated :=
begin
  intros n g hg,
  simpa only [f.mem_ker, gsmul_eq_smul, f.map_gsmul, smul_eq_zero] using hg
end

Johan Commelin (Apr 29 2021 at 13:05):

Easy to state, trivial to prove.

Johan Commelin (Apr 29 2021 at 13:09):

So, now we have:

lemma L_saturated
  [hf : fact (∃ f' : polyhedral_lattice_hom Λ' Λ, (f'.comp f) = polyhedral_lattice_hom.id)] :
  (L f m).saturated :=
begin
  unfreezingI { obtain ⟨f', h⟩ := hf },
  rw ← finite_free.claim f f' m h,
  apply add_subgroup.ker_saturated
end

Johan Commelin (Apr 29 2021 at 13:10):

What is left is to fill in this sorry:

namespace finite_free

-- move this, better names?

def Δ : Λ' →+ (fin m →₀ Λ') :=
add_monoid_hom.mk' (λ l, ∑ i, finsupp.single_add_hom i l) $
λ l₁ l₂, by simp only [add_monoid_hom.map_add, finset.sum_add_distrib]

def σ : (fin m →₀ Λ') →+ Λ' :=
add_monoid_hom.mk' (λ l, l.sum (λ _, add_monoid_hom.id _)) $
λ l₁ l₂, finsupp.sum_add_index' _

def a : (fin m →₀ Λ') →+ Λ' :=
add_monoid_hom.comp (f.comp f').to_add_monoid_hom (σ m)

def φ : (fin m →₀ Λ') →+ (fin m →₀ Λ') :=
(finsupp.map_range_hom $ add_monoid_hom.id _ - (f.comp f').to_add_monoid_hom) +
  ((Δ m).comp (a f f' m))

lemma claim (h : (f'.comp f) = polyhedral_lattice_hom.id) : (φ f f' m).ker = L f m :=
begin
  sorry
end

end finite_free

Johan Commelin (Apr 29 2021 at 13:28):

Hmm, I actually think that defining $L_m$ to be that kernel is not so bad.

Johan Commelin (Apr 29 2021 at 13:29):

You need to prove that this kernel plays will with morphisms from the simplex category. But that seems to be a straightforward calculation, so far.

Johan Commelin (Apr 29 2021 at 13:30):

Whereas working with the additive subgroup closure of

{x | ∃ (l : Λ) (n : fin m →₀ ℤ) (hn : n.sum (λ _, add_monoid_hom.id _) = 0),
     x = finsupp.map_range_hom (int.cast_add_hom' (f l)) n}

is just painful.

Peter Scholze (Apr 29 2021 at 13:31):

Why not define it as the set of elements of $\Lambda'^m$ all of whose coordinates are in $\Lambda$ , and sum to $0$ ? That's very close to the kernel of this map, but seems a bit easier to manipulate still.

Johan Commelin (Apr 29 2021 at 13:37):

Asking that the coordinates are in $\Lambda$ introduces an existential. Which means that you constantly have to choose witnesses.

Johan Commelin (Apr 29 2021 at 13:37):

The splitting map circumvents that in a very nice way.

Peter Scholze (Apr 29 2021 at 13:38):

Aha! But the splitting map in itself is a choice... but maybe it doesn't matter so much if you just make this choice globally

Johan Commelin (Apr 29 2021 at 13:40):

Exactly, you only choose it once.

Johan Commelin (Apr 30 2021 at 08:14):

These sorrys are now fixed.

Johan Commelin (Apr 30 2021 at 08:15):

I'm just building locally before I push.

Johan Commelin (Apr 30 2021 at 08:22):

Pushed

Peter Scholze (Apr 30 2021 at 08:26):

So this takes care of the polyhedral lattice - Cech nerve?

Johan Commelin (Apr 30 2021 at 08:30):

Well, we still need to check that the quotients are polyhedral

Johan Commelin (Apr 30 2021 at 08:30):

And this might need Gordan again

Johan Commelin (Apr 30 2021 at 08:31):

We need to write down generators for the norm, and we need to show that the quotient is a normed group.

Peter Scholze (Apr 30 2021 at 08:31):

But can you already verify that it is a Cech nerve?

Johan Commelin (Apr 30 2021 at 08:31):

(At the moment it's only semi-normed.)

Peter Scholze (Apr 30 2021 at 08:31):

OK, nice

Johan Commelin (Apr 30 2021 at 08:32):

Right, we have the Cech construction. But it's a bit ad hoc, and needs to be glued to the general theory that Adam developed.

Johan Commelin (Apr 30 2021 at 09:58):

Current sorry count:

1       src/thm95/default.lean
1       src/thm95/row_iso.lean
10      src/thm95/constants.lean
1       src/locally_constant/NormedGroup.lean
3       src/polyhedral_lattice/basic.lean
4       src/pseudo_normed_group/profinitely_filtered.lean
2       src/polyhedral_lattice/cech.lean
2       src/for_mathlib/dfinsupp.lean
1       src/for_mathlib/Gordan.lean
3       src/for_mathlib/int_grading_lemma.lean
8       src/for_mathlib/grading_monoid_algebra.lean
4       src/thm95/polyhedral_iso.lean
Total:  40

Johan Commelin (Apr 30 2021 at 15:24):

1       src/thm95/default.lean
1       src/thm95/row_iso.lean
1       src/locally_constant/NormedGroup.lean
10      src/thm95/constants.lean
3       src/polyhedral_lattice/basic.lean
2       src/polyhedral_lattice/cech.lean
2       src/for_mathlib/dfinsupp.lean
1       src/for_mathlib/Gordan.lean
8       src/for_mathlib/grading_monoid_algebra.lean
3       src/for_mathlib/int_grading_lemma.lean
Total:  32

Johan Commelin (May 01 2021 at 19:42):

The list of files is getting shorter:

1       src/thm95/default.lean
1       src/locally_constant/NormedGroup.lean
10      src/thm95/constants.lean
3       src/polyhedral_lattice/basic.lean
2       src/polyhedral_lattice/cech.lean
1       src/for_mathlib/Gordan.lean
2       src/for_mathlib/dfinsupp.lean
8       src/for_mathlib/grading_monoid_algebra.lean
6       src/for_mathlib/int_grading_lemma.lean
Total:  34

Kevin Buzzard (May 01 2021 at 21:19):

Those last four files are a work in progress. I've stated Gordan and yesterday I also managed to state the intermediate commutative algebra lemma about $\Z$ -graded rings, so things are going in the right direction. It's a long weekend in the UK and I'm away from my home and unlikely to do much, but on the other hand @Eric Wieser has filled in a couple of sorries in a DM so the true total is lower

Kevin Buzzard (May 01 2021 at 23:40):

src/for_mathlib/dfinsupp.lean is now sorry-free thanks to Eric's #7311

Johan Commelin (May 15 2021 at 21:03):

1       src/thm95/default.lean
1       src/locally_constant/SemiNormedGroup.lean
10      src/thm95/constants.lean
1       src/prop_92/prop_92.lean
3       src/polyhedral_lattice/topology.lean
2       src/polyhedral_lattice/basic.lean
1       src/polyhedral_lattice/cech.lean
8       src/for_mathlib/grading_monoid_algebra.lean
2       src/for_mathlib/int_grading_lemma.lean
7       src/for_mathlib/finite_free.lean
3       src/prop_92/concrete.lean
Total:  39

Johan Commelin (May 15 2021 at 21:03):

As far as I can tell, all the sorry's in for_mathlib are for the algebraic approach to Gordan. So they are not on the critical path to 9.5.

Kevin Buzzard (May 15 2021 at 21:41):

Yeah the int_grading sorries are not on the path to 9.5, I'm going to PR them to mathlib and move all grading stuff out of the repo now we no longer need it here (we'll need it for projective schemes though)

Johan Commelin (May 18 2021 at 02:43):

1       src/thm95/default.lean
10      src/thm95/constants.lean
1       src/locally_constant/SemiNormedGroup.lean
2       src/prop_92/concrete.lean
1       src/prop_92/prop_92.lean
Total:  15

David Michael Roberts (May 18 2021 at 02:54):

Going down!

David Michael Roberts (May 18 2021 at 02:56):

I think it fitting that constants.lean is where the majority of the sorrys are, given Peter's original concerns :-)

Johan Commelin (Oct 04 2021 at 06:49):

rg -l sorry | rg -v scripts | xargs -I % sh -c 'nsorry=`rg sorry % | wc -l`; echo -n "$nsorry\t%\n"'; echo -en "Total:\t"; rg sorry | rg -v scripts | wc -l
1       src/challenge.lean
2       src/laurent_measures/basic.lean
3       src/for_mathlib/horseshoe.lean
1       src/for_mathlib/short_exact_sequence.lean
1       src/for_mathlib/homological_complex.lean
1       src/for_mathlib/ext.lean
4       src/for_mathlib/exact_seq.lean
2       src/for_mathlib/derived_functor.lean
2       src/for_mathlib/abelian_group_object.lean
1       src/for_mathlib/Profinite/extend.lean
3       src/condensed/proj_cond.lean
6       src/condensed/basic.lean
22      src/condensed/ab.lean
1       src/Mbar/functor.lean
1       src/laurent_measures/thm69.lean
Total:  51

Johan Commelin (Oct 04 2021 at 08:00):

One downside of all the hacking in the last few months is that we haven't been writing any docstrings, which makes the linter unhappy.

Johan Commelin (Oct 04 2021 at 08:01):

I wonder what the best approach is. It would be nice to have a linter check that the first part of LTE doesn't degrade. But at the same time, I want to have a sort of no-rules-just-fun approach to the second half, so that we can do many cheap experiments.

Johan Commelin (Oct 04 2021 at 08:01):

And once we settle down on something, we can clean it up and document it.

Ben Toner (Oct 04 2021 at 10:43):

Has the linter managed to detect anything useful so far?

One compromise might be to have the linter continue running as is, but not mark the build red if there are new linting errors. Or we could stop running it on pushes, but keep it running each day on schedule.

Johan Commelin (Oct 04 2021 at 11:19):

@Ben Toner Occasionally it has been useful. But it was probably a wrong decision by me to think we would start writing docstrings on all our defs in LTE

Johan Commelin (Oct 04 2021 at 11:19):

So disabling that linter is probably a good idea.

Ben Toner (Oct 05 2021 at 04:54):

Okay, I disabled the doc_blame linter.

Johan Commelin (Oct 05 2021 at 04:58):

Merci!

Johan Commelin (Jan 10 2022 at 16:14):

1       src/challenge.lean
6       src/condensed/ab.lean
6       src/condensed/basic.lean
3       src/condensed/proj_cond.lean
2       src/condensed/is_proetale_sheaf.lean
1       src/combinatorial_lemma/profinite.lean
23      src/laurent_measures/thm69.lean
2       src/for_mathlib/derived_functor.lean
1       src/for_mathlib/split_exact.lean
1       src/for_mathlib/homological_complex.lean
1       src/for_mathlib/mapping_cone.lean
1       src/for_mathlib/short_exact_sequence.lean
Total:  48

Johan Commelin (Jan 21 2022 at 12:18):

Because I've been travelling this week, I just haven't done anything with LTE. Every 12 hrs I randomly login to my server, do a git pull, see that 1000 lines have been edited/added/etc... Start a build, and wiat for it to finish. But then something else happens, so I can't actually do something. 12 hrs later... same thing happens.

It's really fun to see all this stuff happening. Even if there isn't much chat here on the stream, there's quite a bit going on behind the screens :octopus: :tools:

Johan Commelin (Feb 07 2022 at 18:11):

Time for a new sorry count, since all the nice progress in the last few days:

1       src/challenge.lean
3       src/condensed/basic.lean
2       src/condensed/ab.lean
2       src/condensed/is_proetale_sheaf.lean
1       src/Mbar/ext.lean
2       src/for_mathlib/derived_functor.lean
1       src/for_mathlib/homological_complex.lean
1       src/for_mathlib/short_exact_sequence.lean
1       src/for_mathlib/sheaves_of_modules/multilinear.lean
Total:  14

Adam Topaz (Feb 24 2022 at 14:43):

I just killed a bunch of sorrys from the condensed folder. Here is the current count:

1 src/challenge.lean
1 src/condensed/exact.lean
21 src/laurent_measures/ses.lean
5 src/laurent_measures/ses2.lean
2 src/laurent_measures/thm69.lean
1 src/laurent_measures/functor.lean
1 src/Lbar/ext.lean
4 src/for_mathlib/derived/K_projective.lean
36 total

Johan Commelin (Feb 24 2022 at 14:51):

Great! We're getting at a stage where all the "basics" are done.

Johan Commelin (Mar 21 2022 at 05:16):

1       src/challenge.lean
1       src/condensed/exact.lean
1       src/Lbar/ext.lean
4       src/breen_deligne/eval.lean
1       src/free_pfpng/main.lean
2       src/laurent_measures/thm69.lean
26      src/laurent_measures/ses.lean
5       src/laurent_measures/ses2.lean
9       src/for_mathlib/triangle_shift.lean
Total:  50

Whoohoo, a lot of annoying sorrys in for_mathlib/derived/* are gone! Thanks @Andrew Yang :octopus:

Kevin Buzzard (Mar 21 2022 at 14:43):

Just looking at these sorrys to feel my way back into the project. The sorry in condensed.exact involves proving a theorem about something called exact_with_constant, a definition with no docstring and with no reference to either the blueprint or the Scholze lectures. Is someone in a position to add some clues?

Johan Commelin (Mar 21 2022 at 14:46):

https://leanprover-community.github.io/liquid/dep_graph_section_2.html

Johan Commelin (Mar 21 2022 at 14:46):

https://leanprover-community.github.io/liquid/sect0010.html#exact-with-constant

Johan Commelin (Mar 21 2022 at 14:46):

There is a exact-with-constant node in that graph

Kevin Buzzard (Mar 21 2022 at 14:47):

The sorry in Lbar.exthas a warning above Ext_iso_zero which seems to say "we need this theorem in more generality". Is it even possible to state what we need? Is there sorried data elsewhere?

Kevin Buzzard (Mar 21 2022 at 14:48):

Johan Commelin: There is a exact-with-constant node in that graph

Thanks. I didn't know how to search the graph for the node corresponding to the exact_with_constant declaration in the project. The blueprint didn't seem to have a search and I couldn't get google site search to work. What am I missing?

Johan Commelin (Mar 21 2022 at 14:48):

Ctrl-F should work

Johan Commelin (Mar 21 2022 at 14:49):

Kevin Buzzard said:

The sorry in Lbar.exthas a warning above Ext_iso_zero which seems to say "we need this theorem in more generality". Is it even possible to state what we need? Is there sorried data elsewhere?

Aah, this now needs to be updated. It should become this statement: https://leanprover-community.github.io/liquid/sect0010.html#Ext-Lbar

Kevin Buzzard (Mar 21 2022 at 14:49):

You mean I have to clone the blueprint? Ctrl-F on what?

Johan Commelin (Mar 21 2022 at 14:49):

On the graph

Johan Commelin (Mar 21 2022 at 14:49):

Or just ask here. That's the best solution, I guess

Kevin Buzzard (Mar 21 2022 at 14:50):

got it, although it was 50-50 whether it was going to be part 1 or part 2 I guess

Johan Commelin (Mar 21 2022 at 14:50):

The graph of part 1 is completely green. It's really everything leading up to thm 9.4, which is sorry free.

Kevin Buzzard (Mar 21 2022 at 14:50):

Ctrl-F fails for me because of the issue with hyphen v underscore

Johan Commelin (Mar 21 2022 at 14:51):

Good point

Kevin Buzzard (Mar 21 2022 at 14:51):

but anyway this is a very cool answer to the question

Johan Commelin (Mar 21 2022 at 14:52):

One "problem" with the sorry in Lbar.ext is that the experiments of last week taught us that we should probably switch to the new LTE definition of Ext.

Kevin Buzzard (Mar 21 2022 at 14:52):

I see!

Johan Commelin (Mar 21 2022 at 14:53):

Namely the Ext' from src/for_mathlib/derived/K_projective.lean

Kevin Buzzard (Mar 21 2022 at 14:53):

Ouch you're using $\subset$ ? That symbol terrifies me. I always use ssubsetneq or whatever it's called -- "it's definitely not equal despite what some people think"

Johan Commelin (Mar 21 2022 at 14:53):

Where am I using it? In the blueprint?

Kevin Buzzard (Mar 21 2022 at 14:56):

This definition of Ext' imports a file for_mathlib/triangle_shift.leanwith sorries.

Adam Topaz (Mar 21 2022 at 14:57):

Those should be by sorry; {proof}.

Johan Commelin (Mar 21 2022 at 14:58):

Not all of them :sad:

Adam Topaz (Mar 21 2022 at 14:58):

Oh :sad:

Johan Commelin (Mar 21 2022 at 14:58):

Some are genuine sorries

Johan Commelin (Mar 21 2022 at 14:59):

They should be math-trivial. But they use lax monoidal functors. So they are very lean-nontrivial.

Adam Topaz (Mar 21 2022 at 14:59):

ugh

Adam Topaz (Mar 21 2022 at 14:59):

I'm up for a little pair programming later if you want to tackle those.

Johan Commelin (Mar 21 2022 at 15:00):

I'm in a talk...

Kevin Buzzard (Mar 21 2022 at 15:00):

I can't do this today but next week I will have opportunities for this

Adam Topaz (Mar 21 2022 at 15:00):

Adam Topaz said:

...later...

Kevin Buzzard (Mar 21 2022 at 15:02):

Oh I see! This is the first time I've seen the sorry; trick in the wild! Will we notice if bumping mathlib breaks any of these sorried out proofs?

Kevin Buzzard (Mar 21 2022 at 15:02):

these are the easiest sorries I've ever killed in LTE

Kevin Buzzard (Mar 21 2022 at 15:04):

OK there are 6 remaining, and they are all Props

Eric Rodriguez (Mar 21 2022 at 15:08):

sorry; {proof} is now superseded by sorry { proof }!

Yaël Dillies (Mar 21 2022 at 15:09):

Kevin Buzzard said:

Ouch you're using $\subset$ ? That symbol terrifies me. I always use ssubsetneq or whatever it's called -- "it's definitely not equal despite what some people think"

cf our discussion with the Isabelle team about SRL

Johan Commelin (Mar 21 2022 at 15:11):

I think that > 95% of mathematicians use $⊂$ to mean ⊆. I'm one of them. I know Lean disagrees with me about this symbol...

Johan Commelin (Mar 21 2022 at 16:45):

@Kevin Buzzard If you want a specific target to think about, I think this one might be easy to get started on: https://leanprover-community.github.io/liquid/sect0010.html#Lbar-ses

Johan Commelin (Mar 21 2022 at 16:46):

@Damiano Testa is also working on it. So you would have to coordinate with him a bit.

Kevin Buzzard (Mar 21 2022 at 16:46):

I'm just figuring out where we are right now

Kevin Buzzard (Mar 21 2022 at 16:46):

I still need to make a bunch more videos and finish up other term stuff.

Johan Commelin (Mar 21 2022 at 16:47):

Ok, I'll try my best to make sure that the landscape looks completely different next week. So that you can reorient all over again :rofl:

Adam Topaz (Mar 22 2022 at 03:39):

New sorry count

1 src/challenge.lean
1 src/condensed/exact.lean
27 src/laurent_measures/ses.lean
5 src/laurent_measures/ses2.lean
2 src/laurent_measures/thm69.lean
1 src/free_pfpng/main.lean
4 src/breen_deligne/eval.lean
1 src/Lbar/ext.lean
42 total

(Note that for_mathlib/triangle_shift is missing from the above ;))

Johan Commelin (Mar 22 2022 at 06:17):

Marvellous!

Kevin Buzzard (Mar 22 2022 at 07:57):

How much data is sorried, and how much data is not even defined but you know we're going to have to define it to finish the job?

Kevin Buzzard (Mar 22 2022 at 07:58):

I was attempting to figure out the answer to the first question yesterday but then I had to go back to work stuff

Johan Commelin (Mar 22 2022 at 08:21):

I think almost all of the sorrys in the count above are Props. But there is still data to be defined.

Johan Commelin (Mar 22 2022 at 08:21):

My plan is to try and define a lot of data today.

Filippo A. E. Nuccio (Mar 22 2022 at 18:10):

ses.lean is down to 4 sorrys.

Johan Commelin (Mar 22 2022 at 18:16):

Wow!!

1       src/challenge.lean
1       src/condensed/exact.lean
1       src/Lbar/ext.lean
1       src/free_pfpng/main.lean
1       src/breen_deligne/main.lean
5       src/breen_deligne/eval.lean
2       src/laurent_measures/thm69.lean
4       src/laurent_measures/ses.lean
5       src/laurent_measures/ses2.lean
5       src/for_mathlib/complex_extend.lean
Total:  26

Johan Commelin (Mar 22 2022 at 18:16):

@Filippo A. E. Nuccio That's really nice!

Johan Commelin (Mar 22 2022 at 18:17):

commit e07d5d19f77b18c5d98d99d5c2860465d696ae49 (origin/lean-3.42.0)
Author: Filippo A. E. Nuccio <filippo.nuccio@univ-st-etienne.fr>
Date:   Tue Mar 22 19:11:50 2022 +0100

    killed 22 sorry

Johan Commelin (Mar 22 2022 at 18:17):

How would you describe the remaining 4? Are they math-trivial? Lean-hard?

Filippo A. E. Nuccio (Mar 22 2022 at 18:17):

It took me a while, but a painful continuity business is now OK. Now I have 2 easy things, and two about which I am still unsure...

Filippo A. E. Nuccio (Mar 22 2022 at 18:18):

One is certainly math-easy (not entirely trivial), and probably Lean-doable. The other I do not know yet, but I will know soon, and will report here.

Filippo A. E. Nuccio (Mar 22 2022 at 18:21):

Of the two "easy" one was very easy...

begin
  refl,
end

:rofl:

Kevin Buzzard (Apr 08 2022 at 01:17):

for_mathlib/complex_extend is now sorry-free (but some of my proofs are a bit crappy; I had a bunch of motive is not type correct issues which I avoided using heq)

Scott Morrison (Apr 08 2022 at 03:05):

proved embedding of complexes is additive (was a sorry in breen_deligne/eval, but I moved the content to for_mathlib/complex_extend)

Johan Commelin (Apr 08 2022 at 05:12):

Thanks! This is cool!

Johan Commelin (Apr 08 2022 at 05:12):

I'm glad you found a heq-hack Kevin!

Scott Morrison (Apr 08 2022 at 13:38):

I just did the comm and fac fields in functor_eval_flip_preserves_colimits_of_shape, but uniq has me confused as usual.

Adam Topaz (Apr 08 2022 at 13:38):

Where is this functor_eval_flip_preserves_colimits_of_shape? Just looking at the name makes me think we have something like this in mathlib alreeady

Scott Morrison (Apr 08 2022 at 13:44):

I just finished it, actually. It is in breen_deligne/eval.lean.

Adam Topaz (Apr 08 2022 at 13:44):

Ah!

Scott Morrison (Apr 08 2022 at 13:44):

The name hides the fact it is about complexes of functors; so I doubt mathlib has it. :-)

Adam Topaz (Apr 08 2022 at 13:45):

Presumably we have the fact that the functor sending a complex $X_\bullet$ to $X_i$ for a fixed $i$ preserves colimits? We could have used something like that along with the fact that functor evaluation preserves colimits.

Adam Topaz (Apr 08 2022 at 13:46):

Maybe we would also need something like the fact that the functors $X_\bullet \mapsto X_i$ jointly create colimits as $i$ varies.

Scott Morrison (Apr 08 2022 at 13:47):

I thought something like that too, but I think I was a bit confused. How would such an argument use the fact that we're looking at a complex of colimit-preserving functors?

Johan Commelin (Apr 08 2022 at 13:47):

Wow, you're on fire Scott!

Scott Morrison (Apr 08 2022 at 13:47):

breen_deligne/eval is done now :-)

Johan Commelin (Apr 08 2022 at 13:47):

I claim this means that there's another oval to be turned green.

Scott Morrison (Apr 08 2022 at 13:47):

oooh

Scott Morrison (Apr 08 2022 at 13:48):

I still can't make head or tail of the dependency graph. I wouldn't start to guess which oval. :-)

Johan Commelin (Apr 08 2022 at 13:48):

Technically, to apply the result, we need to know that A ↦ ℤ[A] preserves filtered colimits. We'll still need to do that. (For condensed ab groups A.)

Johan Commelin (Apr 08 2022 at 13:49):

It's homology-Qprime.

Adam Topaz (Apr 08 2022 at 13:49):

Johan Commelin said:

Technically, to apply the result, we need to know that A ↦ ℤ[A] preserves filtered colimits. We'll still need to do that. (For condensed ab groups A.)

This is going to be tricky

Johan Commelin (Apr 08 2022 at 13:56):

I hope it follows formally from the same claim for the category Ab?

Adam Topaz (Apr 08 2022 at 13:57):

Oh, yeah, that argument shouldn't be too bad -- sheafification already preserves colimits.

Adam Topaz (Apr 08 2022 at 13:58):

There was some other point where we need something to preserve filtered colimits that was more complicated, but I don't recall exactly what that was right now.

Johan Commelin (Apr 11 2022 at 05:10):

Yuchai! We're back in the < 50 sorry realm!

1 src/challenge.lean
5 src/Lbar/ext.lean
1 src/Lbar/ses.lean
6 src/real_measures/basic.lean
1 src/breen_deligne/main.lean
1 src/free_pfpng/acyclic.lean
3 src/free_pfpng/main.lean
6 src/invpoly/ses.lean
2 src/laurent_measures/thm69.lean
3 src/laurent_measures/ses2.lean
14 src/laurent_measures/ses.lean
1 src/for_mathlib/bicartesian.lean
1 src/for_mathlib/derived/les.lean
1 src/for_mathlib/derived/les2.lean
2 src/for_mathlib/derived/les_facts.lean
1 src/for_mathlib/derived/K_projective.lean
49 total

Johan Commelin (Apr 11 2022 at 05:10):

Major kudos to all the sorry-killers off the last few days.

Johan Commelin (Apr 28 2022 at 06:40):

The total number of sorries hasn't changed much. But still, it is very fair to say that we've made huge progress since the previous post in this thread.

1 src/breen_deligne/main.lean
1 src/condensed/acyclic.lean
2 src/for_mathlib/acyclic.lean
3 src/for_mathlib/derived/les2.lean
3 src/for_mathlib/derived/les_facts.lean
1 src/for_mathlib/derived/les.lean
1 src/for_mathlib/ennreal.lean
7 src/for_mathlib/salamander.lean
5 src/invpoly/ses.lean
3 src/laurent_measures/ses2.lean
17 src/laurent_measures/ses.lean
3 src/laurent_measures/thm69.lean
4 src/Lbar/ext.lean
51 total

Kevin Buzzard (Apr 28 2022 at 07:27):

I am hoping to make thm69 sorry-free today. It was sorry-free before but then two of the main definitions got refactored to make our lives easier elsewhere, which broke a very elaborate convergence argument; I've added new results to for_mathlib.nnreal and for_mathlib.ennreal in order to make the proof more conceptual but it's still pretty gnarly.

Yaël Dillies (Apr 28 2022 at 08:20):

The sorry in for_mathlib.ennreal is commented by the way.

Kevin Buzzard (Apr 28 2022 at 18:04):

OK thm69 is now sorry-free again. It was sorry-free a couple of weeks ago but then we refactored a definition and the refactor was a lot of work for me -- I had to learn how to steer nnreal.

Filippo A. E. Nuccio (Apr 28 2022 at 19:06):

Yes, I agree that nnrealcan be very painful, I went through some pain as well. But thanks for your help!

Johan Commelin (Apr 28 2022 at 19:16):

Hooray! Seems like it's time for another sorry-count then :grinning:

1 src/breen_deligne/main.lean
1 src/condensed/acyclic.lean
2 src/for_mathlib/acyclic.lean
3 src/for_mathlib/derived/les2.lean
3 src/for_mathlib/derived/les_facts.lean
1 src/for_mathlib/derived/les.lean
7 src/for_mathlib/salamander.lean
5 src/invpoly/ses.lean
3 src/laurent_measures/ses2.lean
2 src/laurent_measures/ses.lean
4 src/Lbar/ext.lean
32 total

Yaël Dillies (Apr 28 2022 at 19:18):

Yaël Dillies said:

The sorry in for_mathlib.ennreal is commented by the way.

This is still true :point_up:

Johan Commelin (Apr 28 2022 at 19:19):

I just removed it (-;

Johan Commelin (May 23 2022 at 20:06):

Time for an update

1 src/breen_deligne/main.lean
1 src/condensed/acyclic.lean
2 src/for_mathlib/acyclic.lean
1 src/for_mathlib/derived/Ext_lemmas.lean
1 src/for_mathlib/derived/les3.lean
1 src/for_mathlib/is_quasi_iso.lean
2 src/for_mathlib/snake_lemma_naturality2.lean
15 src/Lbar/ext.lean
2 src/pseudo_normed_group/QprimeFP.lean
26 total

Adam Topaz (May 23 2022 at 20:46):

A little progress:

1 src/condensed/acyclic.lean
1 src/breen_deligne/main.lean
15 src/Lbar/ext.lean
2 src/for_mathlib/acyclic.lean
2 src/for_mathlib/snake_lemma_naturality2.lean
1 src/for_mathlib/is_quasi_iso.lean
2 src/pseudo_normed_group/QprimeFP.lean
1 src/for_mathlib/derived/Ext_lemmas.lean
25 total

Kevin Buzzard (May 23 2022 at 22:04):

Will the reorganisation of category theory in master mean that bumping will be difficult?

Johan Commelin (May 24 2022 at 03:26):

Yes, probably. But we might be able to postpone the bump till LTE is sorry-free.

Adam Topaz (May 25 2022 at 03:44):

Quick update:

1 src/condensed/acyclic.lean
1 src/breen_deligne/main.lean
11 src/Lbar/ext.lean
2 src/for_mathlib/acyclic.lean
2 src/for_mathlib/snake_lemma_naturality2.lean
1 src/for_mathlib/is_quasi_iso.lean
2 src/pseudo_normed_group/QprimeFP.lean
20 total

Riccardo Brasca (May 25 2022 at 08:01):

The sorry in snake_lemma_naturality2.lean seems very annoying :unamused:

Riccardo Brasca (May 25 2022 at 09:24):

I mean, there are 625 cases....

Johan Commelin (May 25 2022 at 10:06):

Ouch.... let me check which sorry you are talking about. This doesn't sound good.

Johan Commelin (May 25 2022 at 10:10):

snake.snake_diagram is defined in terms of mk_functor which in turn uses col and row which are using fin{3,4}_functor_mk. My guess is that you would have to go back to those and prove things for them first.

Johan Commelin (May 25 2022 at 10:10):

Hopefully that allows you to take a square root out of the number of cases...

Adam Topaz (May 25 2022 at 13:38):

Is it possible to trick the simplifier into doing all the grunt work, and only proving commutativity of around 12 squares?

Johan Commelin (May 25 2022 at 14:28):

600 * simp = eternity?

Riccardo Brasca (May 25 2022 at 14:38):

Indeed the first thing I tried is some any_goals {... simp...} hoping to decrease the number of thing to prove, but I got a deterministic timeout.

Johan Commelin (May 25 2022 at 14:42):

So I think we have to help Lean by explaining that a bunch of the grunt work is repetitive.

Adam Topaz (May 25 2022 at 14:43):

I think something like this could help

def cast_horizontal (i : fin 4) (j : fin 2) : snake_diagram := (i,j.cast_succ)
def cast_vertical (i : fin 3) (j : fin 3) : snake_diagram := (i.cast_succ,j)
def succ_horizontal (i : fin 4) (j : fin 2) : snake_diagram := (i, j.succ)
def succ_vertical (i : fin 3) (j : fin 3) : snake_diagram := (i.succ,j)
def to_succ_horizontal (i : fin 4) (j : fin 2) :
  cast_horizontal i j ⟶ succ_horizontal i j := sorry
def to_succ_vertical ( i : fin 3) (j : fin 3) :
  cast_vertical i j ⟶ succ_vertical i j := sorry

lemma snake_diagram_induction
  {motive : Π {i j : snake_diagram} (f : i ⟶ j), Prop}
  (id : ∀ i : snake_diagram, motive (𝟙 i))
  (comp : ∀ (i j k : snake_diagram) (f : i ⟶ j) (g : j ⟶ k),
    motive f → motive g → motive (f ≫ g))
  (succ_horizontal : ∀ (i : fin 4) (j : fin 2),
    motive (to_succ_horizontal i j))
  (succ_vertical : ∀ (i : fin 3) (j : fin 3),
    motive (to_succ_vertical i j)) (i j : snake_diagram) (f : i ⟶ j) : motive f := sorry

Johan Commelin (May 25 2022 at 14:44):

Yay, motives!

Adam Topaz (May 25 2022 at 14:51):

I pushed this sketch to snake_lemma_naturality2

Adam Topaz (May 25 2022 at 14:52):

I guess we will need a similar inductive principle for morphisms in fin n

Johan Commelin (May 25 2022 at 14:53):

I wish Lean could auto-generate that induction lemma.

Johan Commelin (May 25 2022 at 15:11):

Maybe we also want an induction lemma for product cats?

Adam Topaz (May 25 2022 at 15:12):

Yeah, that snake_diagram_induction should just be a combination of an induction for fin n and an induction for product cats

Johan Commelin (May 25 2022 at 15:12):

@Riccardo Brasca @Adam Topaz Is either of you working on this file atm?

Adam Topaz (May 25 2022 at 15:12):

I'm not.

Riccardo Brasca (May 25 2022 at 15:12):

Not really

Johan Commelin (May 25 2022 at 15:14):

Ok, I'll see if I can close some goals

Riccardo Brasca (May 25 2022 at 15:17):

I have a proof of (the very easy) to_succ_horizontal

Riccardo Brasca (May 25 2022 at 15:28):

I've pushed it (and also the other easy sorry). I am not working on the serious ones.

Johan Commelin (May 25 2022 at 15:35):

Ok, I have an induction lemma for prod cats, working on fin (n+1) now.

Johan Commelin (May 25 2022 at 15:47):

Nooo :cry: :cry: :cry:
The category structure of fin 4 × fin 3 is not category_theory.prod. It comes from the product preorder...

Adam Topaz (May 25 2022 at 15:49):

Aren't these the same?

Adam Topaz (May 25 2022 at 15:49):

The preorder is the product of the preorders.

Kevin Buzzard (May 25 2022 at 15:49):

It's not lex?

Adam Topaz (May 25 2022 at 15:51):

example (i i' : fin 4) (j j' : fin 3) (e : i ⟶ i') (f : j ⟶ j') :
  ((i,j) : snake_diagram) ⟶ (i',j') := (e,f)

That typechecks

Adam Topaz (May 25 2022 at 15:53):

Also this

example (i j : snake_diagram) (e : i.1 ⟶ j.1) (f : i.2 ⟶ j.2) : i ⟶ j :=
hom_of_le $ by { cases i, cases j, simp only [prod.mk_le_mk], dsimp at e f, exact ⟨e.le,f.le⟩ }

Adam Topaz (May 25 2022 at 15:54):

OOkay, so I guess they're "the same" up to some silliness with hom_of_leand le_of_hom.

Johan Commelin (May 25 2022 at 15:56):

There is a defeq problem somewhere.

Johan Commelin (May 25 2022 at 15:57):

But I just proved the induction lemma for products of preorders.

Johan Commelin (May 25 2022 at 16:16):

I pushed. The induction lemma is now sorry-free.

Yaël Dillies (May 25 2022 at 16:19):

Johan Commelin said:

Nooo :cry: :cry: :cry:
The category structure of fin 4 × fin 3 is not category_theory.prod. It comes from the product preorder...

I mean maybe we'll one day define preorder as category.{0}.

Adam Topaz (May 25 2022 at 16:19):

That's not what you think it is.

Adam Topaz (May 25 2022 at 16:19):

category.{0} means morphisms are in Type 0 not Sort 0.

Yaël Dillies (May 25 2022 at 16:29):

But couldn't it be?

Adam Topaz (May 25 2022 at 16:31):

It could be. If I recall correctly, it was discussed when docs#quiver was introduced, but I don't remember what happened.

Kevin Buzzard (May 25 2022 at 17:23):

IIRC @Scott Morrison tried allowing Props for morphisms a couple of years ago, but then rowed back.

Johan Commelin (May 25 2022 at 18:33):

snake delta naturality is now sorry free

Adam Topaz (May 25 2022 at 18:34):

So now we have 37 variants of the snake lemma?! Which one should go to mathlib?

Johan Commelin (May 25 2022 at 18:36):

I think we really only have two variants... one was nice for being proven, the other is nice for applying in other proofs.

Adam Topaz (May 25 2022 at 18:40):

Oh, sure, I was just using the following well-known theorem

example (n : ℕ) (hn : 1 < n) : n = 37 := by Kevin_Buzzard

Adam Topaz (May 25 2022 at 18:41):

In any case, presumably the salamander lemma is the one that should go into mathlib.

Johan Commelin (Jun 01 2022 at 18:53):

Time for an update:

10 src/breen_deligne/main.lean
8 src/condensed/acyclic.lean
1 src/condensed/adjunctions2.lean
1 src/condensed/adjunctions.lean
4 src/for_mathlib/abelian_sheaves/exact.lean
3 src/for_mathlib/chain_complex_exact.lean
2 src/for_mathlib/derived/example.lean
6 src/for_mathlib/endomorphisms/basic.lean
4 src/for_mathlib/endomorphisms/Ext.lean
1 src/for_mathlib/truncation_Ext.lean
11 src/for_mathlib/truncation.lean
2 src/for_mathlib/wide_pullback_iso.lean
12 src/Lbar/ext.lean
2 src/pseudo_normed_group/QprimeFP.lean
67 total

Johan Commelin (Jun 01 2022 at 18:54):

That's a lot of sorries. But we are rapidly breaking down all the sorries into small pieces. There's a little bit left about tensor products of condensed abelian groups with abelian groups, and the interaction with Q'(M). But apart from that, I think that all sorries are now "small".
Many of them are also self-contained, in the sense that you don't need a lot of context to jump into them once you are familiar with abstract homological algebra.

Adam Topaz (Jun 03 2022 at 22:40):

I finished off a few more sorries today... here's the current count.

10 src/breen_deligne/main.lean
2 src/pseudo_normed_group/QprimeFP.lean
1 src/condensed/adjunctions2.lean
5 src/condensed/acyclic.lean
8 src/for_mathlib/truncation.lean
1 src/for_mathlib/truncation_Ext.lean
12 src/Lbar/ext.lean
2 src/for_mathlib/derived/example.lean
4 src/for_mathlib/endomorphisms/Ext.lean
6 src/for_mathlib/endomorphisms/basic.lean
51 total

Johan Commelin (Jun 04 2022 at 05:04):

I guess we are getting close to have all the acyclicity stuff sorry-free?

Kevin Buzzard (Jun 04 2022 at 05:42):

I'm about to get on a train from Zurich to London and work on truncation.lean for a while

Eric Rodriguez (Jun 04 2022 at 07:19):

Swiss trains are a wonder, perfect working environment imo

Adam Topaz (Jun 08 2022 at 12:31):

A quick update after some good progress!

11 src/breen_deligne/main.lean
2 src/pseudo_normed_group/QprimeFP.lean
4 src/condensed/tensor.lean
1 src/condensed/bd_lemma.lean
7 src/for_mathlib/truncation.lean
1 src/for_mathlib/truncation_Ext.lean
6 src/for_mathlib/single_coproducts.lean
12 src/Lbar/ext.lean
4 src/for_mathlib/endomorphisms/Ext.lean
5 src/for_mathlib/endomorphisms/basic.lean
53 total

Kevin Buzzard (Jun 08 2022 at 13:45):

Again it would be nice to have a feeling about these sorries. I am about to take on for_mathlib/truncation and I know that (a) there's sorried data (b) I know how to unsorry it (c) I am confident that within a couple of days, for_mathlib/truncation will be sorry-free (because I know the maths and I know that all the techniques are avilable to me). Are there others prepared to offer their thoughts about the status of some of the other sorrys? Is there a bottleneck? Is there more sorried data, or data which we will need to build but has not even been formalised at all ("invisible sorries")?

Adam Topaz (Jun 08 2022 at 13:46):

@Kevin Buzzard if you want to practice your colimit chops, I just added a bunch of sorries in for_mathlib/single_coprodcts

Adam Topaz (Jun 08 2022 at 13:46):

All props

Johan Commelin (Jun 08 2022 at 13:47):

Probably src/condensed/tensor.lean is the part that is the least fleshed out.

Johan Commelin (Jun 08 2022 at 13:48):

Some of the other files, like src/Lbar/ext.lean are pretty fleshed out, but it might be hard to jump right in, because this files is about the nitty-gritty glue between part 1 and part 2 of LTE.

Johan Commelin (Jun 08 2022 at 13:48):

A file like src/for_mathlib/endomorphisms/basic.lean should be fairly self-contained.

Kevin Buzzard (Jun 08 2022 at 13:49):

Right now is a really good time for me to hack on this stuff. I am happy to do as much self-contained stuff as I can while you take on the messy stuff, and I'll come and join you when the sorries are down to single figures.

Johan Commelin (Jun 27 2022 at 04:08):

We are sub-70 sorries again! Thanks so much for your help @Joël Riou!

$ ./scripts/count_sorry.sh | sort -k2
7 src/breen_deligne/main.lean
1 src/condensed/ab5.lean
25 src/condensed/bd_lemma.lean
1 src/for_mathlib/ab5.lean
3 src/for_mathlib/derived/homology.lean
1 src/for_mathlib/endomorphisms/Ext.lean
9 src/for_mathlib/exact_functor.lean
8 src/for_mathlib/homological_complex2.lean
4 src/for_mathlib/single_coproducts.lean
4 src/Lbar/ext.lean
1 src/Lbar/torsion_free_profinite.lean
5 src/pseudo_normed_group/QprimeFP.lean
69 total

Johan Commelin (Jun 27 2022 at 04:08):

Anyone who likes to hack on some homological algebra, feel free to join!

Joël Riou (Jun 27 2022 at 07:04):

Now, it is 68!
(If you have time, please see the note I have added in breen_deligne/main.lean, as I believe the definition of mk_bo_ha_ca should be reconsidered. It should not be too annoying though.)

Johan Commelin (Jun 27 2022 at 07:45):

@Joël Riou let me take a look

Johan Commelin (Jun 27 2022 at 07:47):

Yeah, I think you are right. I had the same solution in mind, but I hadn't yet gotten around to refactoring the defn.

Johan Commelin (Jun 27 2022 at 14:06):

I'm working on this refactor right now

Johan Commelin (Jun 27 2022 at 15:20):

I pushed a refactor. Dinner time now. Some stuff can still be cleaned up. But at least the sorrys should now be provable.

Kevin Buzzard (Jun 27 2022 at 16:06):

Do you have any kind of feeling about (a) how much sorried data there is (b) how many more sorries are likely to appear in future?

Johan Commelin (Jun 27 2022 at 16:57):

I think apart from the sorry you claimed, almost everything is math-trivial, and shouldn't generate a lot of new sorries.

Johan Commelin (Jun 27 2022 at 16:58):

Concerning data. It's done here and there, but it's all about canonical isoms.

Johan Commelin (Jun 28 2022 at 16:55):

In src/for_mathlib/homological_complex2.lean there is only 1 sorry left. I fixed the rest. Again, I'm missing the trick for this last one.

Johan Commelin (Jun 29 2022 at 03:46):

Thanks to the force of @Joël Riou a lot of sorries were closed recently

3 src/breen_deligne/main.lean
1 src/condensed/ab5.lean
25 src/condensed/bd_lemma.lean
1 src/for_mathlib/ab5.lean
3 src/for_mathlib/derived/homology.lean
1 src/for_mathlib/endomorphisms/Ext.lean
1 src/for_mathlib/exact_functor.lean
8 src/for_mathlib/homological_complex2.lean
4 src/Lbar/ext.lean
2 src/Lbar/torsion_free_profinite.lean
7 src/pseudo_normed_group/QprimeFP.lean
56 total

Note that 7 of the 8 sorries in src/for_mathlib/homological_complex2.lean are fake. They are only there to speed up the proof while working on the last sorry. So in reality we are < 50 sorries.

Kevin Buzzard (Jun 29 2022 at 06:34):

Yeah but sometimes it goes up by 20 :-) Are we at the point where this won't happen any more?

Johan Commelin (Jun 29 2022 at 06:40):

It might happen once or twice. But not so often, I think.

Johan Commelin (Jul 04 2022 at 13:12):

Some progress has been made! Thanks to everyone who helped!

2 src/breen_deligne/main.lean
16 src/condensed/bd_lemma.lean
3 src/for_mathlib/derived/homology.lean
1 src/for_mathlib/endomorphisms/ab4.lean
6 src/for_mathlib/endomorphisms/Ext.lean
4 src/Lbar/ext.lean
2 src/Lbar/torsion_free_profinite.lean
7 src/pseudo_normed_group/QprimeFP.lean
41 total

Johan Commelin (Jul 04 2022 at 15:18):

Closed another 2 sorries. We're finally below 40 again.

Kevin Buzzard (Jul 04 2022 at 16:14):

yeah but it will randomly go up to 60 again at some point, right? ;-)

Kevin Buzzard (Jul 04 2022 at 16:15):

My plan is to spend all my Lean time this week removing the sorries in src/for_mathlib/endomorphisms/Ext.lean

Adam Topaz (Jul 04 2022 at 16:21):

4 src/Lbar/ext.lean
3 src/Lbar/torsion_free_profinite.lean
2 src/breen_deligne/main.lean
14 src/condensed/bd_lemma.lean
5 src/pseudo_normed_group/QprimeFP.lean
3 src/for_mathlib/derived/homology.lean
1 src/for_mathlib/endomorphisms/ab4.lean
6 src/for_mathlib/endomorphisms/Ext.lean
38 total

:downwards_trend:

Joël Riou (Jul 04 2022 at 22:06):

breen_deligne/main.lean is now sorry free :-)

Adam Topaz (Jul 04 2022 at 22:09):

Nicely done!

Johan Commelin (Jul 05 2022 at 00:43):

Awesome!

Johan Commelin (Jul 05 2022 at 03:11):

As fas as I can tell, that file now only depends on the sorry in Ext.lean that Kevin is working on.

Johan Commelin (Jul 05 2022 at 03:12):

Modulo that sorry, https://github.com/leanprover-community/lean-liquid//blob/160f7019cfc803467e0f664f55714093e385f4db/src/breen_deligne/main.lean#L310 is done.

Johan Commelin (Jul 05 2022 at 03:12):

Ooh, I meant to link to the blueprint instead of github: https://leanprover-community.github.io/liquid/sect0008.html#Qprime-prop

Johan Commelin (Jul 05 2022 at 04:58):

12 src/condensed/bd_lemma.lean
3 src/for_mathlib/derived/homology.lean
6 src/for_mathlib/endomorphisms/Ext.lean
4 src/Lbar/ext.lean
3 src/Lbar/torsion_free_profinite.lean
2 src/pseudo_normed_group/QprimeFP.lean
30 total

Johan Commelin (Jul 05 2022 at 05:14):

The 3 sorries in derived/homology are most likely not needed.

Johan Commelin (Jul 05 2022 at 06:00):

@Joël Riou is on a rampage

11 src/condensed/bd_lemma.lean
6 src/for_mathlib/endomorphisms/Ext.lean
4 src/Lbar/ext.lean
3 src/Lbar/torsion_free_profinite.lean
2 src/pseudo_normed_group/QprimeFP.lean
26 total

Johan Commelin (Jul 05 2022 at 15:01):

Adam just killed a really gnarly sorry:

7 src/condensed/bd_lemma.lean
1 src/condensed/tensor.lean
7 src/for_mathlib/endomorphisms/Ext.lean
4 src/Lbar/ext.lean
1 src/Lbar/torsion_free_profinite.lean
3 src/pseudo_normed_group/QprimeFP.lean
23 total

Kevin Buzzard (Jul 05 2022 at 16:13):

FWIW my talk is at 2022-07-09T09:15:00+01:00

Johan Commelin (Jul 06 2022 at 10:38):

src/Lbar/torsion_free_profinite.lean is now sorry-free! Thanks @Filippo A. E. Nuccio

Adam Topaz (Jul 06 2022 at 15:05):

The file for_mathlib/nnreal_to_nat_colimit has a very simple sorry (involving absolutely zero category theory)

Adam Topaz (Jul 06 2022 at 15:06):

variables (c : ℝ≥0) [fact (0 < c)]

lemma exists_int_mul (r : ℝ≥0) : ∃ n : ℕ, r ≤ ↑n * c := sorry

Any takers?

Damiano Testa (Jul 06 2022 at 15:07):

I've been inactive on the LTE front for a while: can I claim it?

Adam Topaz (Jul 06 2022 at 15:08):

Go for it!

Damiano Testa (Jul 06 2022 at 15:17):

Ok, that was easy! I just pushed its proof.

Adam Topaz (Jul 06 2022 at 15:20):

Thanks :)

Adam Topaz (Jul 06 2022 at 15:21):

I'll be adding a good number of other sorries throughout the day (some will be more challenging ;))

Damiano Testa (Jul 06 2022 at 15:21):

I look forward to them!

Damiano Testa (Jul 06 2022 at 15:21):

(Although the easy ones are very welcome as well!)

Johan Commelin (Jul 07 2022 at 13:08):

2 src/condensed/bd_lemma.lean
1 src/condensed/bd_ses_aux.lean
1 src/condensed/bd_ses.lean
1 src/condensed/filtered_colimits_commute_with_finite_limits.lean
1 src/condensed/Qprime_isoms.lean
1 src/for_mathlib/hom_single_iso.lean
4 src/Lbar/ext.lean
3 src/pseudo_normed_group/QprimeFP.lean
14 total

Johan Commelin (Jul 10 2022 at 13:02):

Single digits!

6 src/Lbar/ext.lean
3 src/pseudo_normed_group/QprimeFP.lean
9 total

Adam Topaz (Jul 10 2022 at 13:03):

rest assured that I'm going to kill those 3 in QprimeFP in the next few days

Adam Topaz (Jul 10 2022 at 13:20):

Make count an 8

Johan Commelin (Jul 10 2022 at 13:29):

We have build errors though:
we need to dedup nat_trans.comp_app_assoc and freeCond
and I also got an error

/home/runner/work/liquid/liquid/lean-liquid/src/list_decls.lean:382:0: error: invalid import: condensed.filtered_colimits_commute_with_finite_limits
invalid object declaration, environment already has an object named 'CondensedSet.colim_to_lim._proof_1'
<unknown>:1:1: error: invalid object declaration, environment already has an object named 'CondensedSet.colim_to_lim._proof_1'

Johan Commelin (Jul 10 2022 at 13:29):

https://github.com/leanprover-community/liquid/runs/7270784245?check_suite_focus=true#step:7:1355

Johan Commelin (Jul 10 2022 at 13:30):

But I need to go now. If someone wants to fix those, then the blueprint can be updated. (Two oval can become green! Yay!)

Adam Topaz (Jul 10 2022 at 13:51):

If I find some time later today I will try to fix these errors

Adam Topaz (Jul 10 2022 at 15:09):

I did some linting, but there is still more to do, and I need to do other things for a little while. The errors are almost all gone

Johan Commelin (Jul 10 2022 at 16:08):

https://leanprover-community.github.io/liquid/dep_graph_section_2.html is now updated

Yaël Dillies (Jul 10 2022 at 16:10):

Dangling items :scared:

Yaël Dillies (Jul 10 2022 at 16:11):

Also, is it my browser or is this really supposed to be green or a square? :rofl: image.png

Johan Commelin (Jul 10 2022 at 16:37):

I see a green square. I think it's some issue with google fonts...

Johan Commelin (Jul 10 2022 at 17:12):

And the linter is happy!

Johan Commelin (Jul 10 2022 at 17:12):

Although the CI badge disagrees...

Adam Topaz (Jul 12 2022 at 14:10):

New sorry count:

4 src/Lbar/ext.lean
4 total

Filippo A. E. Nuccio (Jul 12 2022 at 14:11):

Are they vaguely accessible, or certainly inaccessible?

Adam Topaz (Jul 12 2022 at 14:11):

We shall see ;)

Johan Commelin (Jul 12 2022 at 15:27):

This is so cool!

David Michael Roberts (Jul 13 2022 at 03:37):

On the web version of the repo it's still at 5, I believe. Have you pushed, @Adam Topaz ?

Adam Topaz (Jul 13 2022 at 03:38):

Currently it's

 1 src/Lbar/ext.lean
2 src/Lbar/ext_aux2.lean
3 total

Adam Topaz (Jul 13 2022 at 03:38):

It's in flux

David Michael Roberts (Jul 13 2022 at 03:38):

ok, glad to see though that it's trending down :-)

Johan Commelin (Jul 13 2022 at 03:39):

Well, the trend can't continue much longer (-;

David Michael Roberts (Jul 13 2022 at 03:40):

Proof by infinite descent... :-P

Adam Topaz (Jul 13 2022 at 03:42):

Let's hope :downwards_trend:

Johan Commelin (Jul 13 2022 at 09:35):

Only sorries left are in Lbar/ext_aux2.lean.

Johan Commelin (Jul 13 2022 at 14:59):

Things are starting to look pretty good :upwards_trend:

1 src/Lbar/ext_aux1.lean
10 src/Lbar/ext_aux2.lean
11 total

Johan Commelin (Jul 13 2022 at 15:50):

Next update:

16 src/Lbar/ext_aux2.lean
16 total

Johan Commelin (Jul 13 2022 at 16:21):

Next update:

6 src/Lbar/ext_aux2.lean
6 total

Adam Topaz (Jul 13 2022 at 16:22):

Oh, just wait....

Riccardo Brasca (Jul 13 2022 at 16:33):

Should we put the champagne in the fridge?

Johan Commelin (Jul 13 2022 at 16:43):

Blueprint has been updated: https://leanprover-community.github.io/liquid/dep_graph_section_2.html
1 oval to go.

Johan Commelin (Jul 13 2022 at 16:43):

We're really close now!

Peter Scholze (Jul 13 2022 at 18:08):

The closing ceremony of the ICM is tomorrow, will you be done in time for that :-)?

Johan Commelin (Jul 13 2022 at 18:13):

I will not exclude that possibility :wink:

Adam Topaz (Jul 13 2022 at 18:15):

I don't know... right now I'm fighting with the fact that $0 - i = -i$ .

Adam Topaz (Jul 13 2022 at 18:15):

Thanks Lean :-/

Peter Scholze (Jul 13 2022 at 20:34):

The glue with the first target, is that already done? Or is that the remaining step? (As formulated, Ext-Lbar-aux is roughly "first target implies desired result" and Ext-Lbar is roughly "desired result", but on the other hand the dependency graph seems to say that the glue with the first target has already been taken care of.)

Johan Commelin (Jul 13 2022 at 21:16):

@Peter Scholze The mathematical content of the glue is completely done (so the short exact sequence of $Q'$ complexes, and the prozero/proisom argument with bicartesian squares, etc...).

What is left is the fact that $\hat V(M^•_•)$ is isomorphic to $\text{Hom}(Q'(M), V)$ in a functorial way. The isomorphism is done for specific M and V. But we need functoriality for the T⁻¹ endomorphisms.

Johan Commelin (Jul 14 2022 at 11:28):

2 src/Lbar/ext_aux2.lean
2 total

Johan Commelin (Jul 14 2022 at 15:09):

1 src/Lbar/ext_aux2.lean
1 total

Riccardo Brasca (Jul 14 2022 at 15:13):

Wow!!

Riccardo Brasca (Jul 14 2022 at 15:13):

You should live stream the last line :grinning_face_with_smiling_eyes:

Johan Commelin (Jul 14 2022 at 15:14):

Adam and I are both on pretty flaky wifi at the moment :sad:

Peter Scholze (Jul 14 2022 at 15:17):

What is the last sorry about?

Adam Topaz (Jul 14 2022 at 15:18):

naturality of the T_inv coming from V

Adam Topaz (Jul 14 2022 at 15:18):

But it involves completions and ulifts so it's a little annoying

Kevin Buzzard (Jul 14 2022 at 19:08):

It's going to go back up to 15, don't get too excited ;-)

Kevin Buzzard (Jul 14 2022 at 19:09):

Actually this is not true, Johan bet me it would be finished today and there's a beer riding on it.

Kevin Buzzard (Jul 14 2022 at 19:09):

I'm trying to find a counterexample

Peter Scholze (Jul 14 2022 at 19:12):

a counterexample to what?

Kevin Buzzard (Jul 14 2022 at 19:19):

The last remaining sorry

Kevin Buzzard (Jul 14 2022 at 19:19):

Then he has to buy me a beer instead

Peter Scholze (Jul 14 2022 at 19:20):

I had assumed that all the sorries were math-trivial for a while?

Kevin Buzzard (Jul 14 2022 at 19:29):

Oh they are, I'm not being serious, I was just trying to get a free beer

Johan Commelin (Jul 14 2022 at 19:48):

0 total

Johan Commelin (Jul 14 2022 at 19:48):

It's done!!!

Kevin Buzzard (Jul 14 2022 at 19:52):

I'll buy you a beer after Yury's talk!

Kevin Buzzard (Jul 14 2022 at 19:52):

Congratulations!

Kevin Buzzard (Jul 14 2022 at 19:52):

Peter should now carefully read the statement of the claim to check that you didn't cheat.

Adam Topaz (Jul 14 2022 at 19:53):

He'll need to read our def of Ext also :upside_down:

Kevin Buzzard (Jul 14 2022 at 19:53):

This is why I mentioned this! The definition of each object in the statement of the theorem needs to be human-verified. If people are happy with the definition then they don't need to read the proof.

Johan Commelin (Jul 14 2022 at 19:54):

Major thanks and congratulations to everyone involved!!!! Special shoutout to Adam!

Peter Scholze (Jul 14 2022 at 19:56):

Whohoo! Congratulations!!

Kevin Buzzard (Jul 14 2022 at 19:56):

One slip in the definition of Ext and maybe you find that Ext^i(X,Y)=0 for all i,X,Y by accident.

Patrick Massot (Jul 14 2022 at 19:56):

Great!

Johan Commelin (Jul 14 2022 at 19:57):

Kevin Buzzard said:

One slip in the definition of Ext and maybe you find that Ext^i(X,Y)=0 for all i,X,Y by accident.

We checked that Ext(Z/2, Z/2) is isom to Z/2

Kevin Buzzard (Jul 14 2022 at 19:57):

OK I'm convinced :-)

Filippo A. E. Nuccio (Jul 14 2022 at 19:58):

Johan Commelin said:

Kevin Buzzard said:

One slip in the definition of Ext and maybe you find that Ext^i(X,Y)=0 for all i,X,Y by accident.

We checked that Ext(Z/2, Z/2) is isom to Z/2

Ah, so with this definition Ext(A,A)=A for all A?

Kevin Buzzard (Jul 14 2022 at 19:58):

Update the blueprint!

Johan Commelin (Jul 14 2022 at 19:58):

It's building!

Johan Commelin (Jul 14 2022 at 19:59):

Blueprint is green!

Johan Commelin (Jul 14 2022 at 20:00):

https://leanprover-community.github.io/liquid/dep_graph_section_2.html

Riccardo Brasca (Jul 14 2022 at 20:06):

This is great!!!

Riccardo Brasca (Jul 14 2022 at 20:07):

Congratulations to everybody involved!!!

Kevin Buzzard (Jul 14 2022 at 21:31):

IMG_20220714_172917501_HDR.jpg

Kevin Buzzard (Jul 14 2022 at 21:32):

Johan pouring champagne

David Michael Roberts (Jul 14 2022 at 21:40):

Are you going to announce this, @Kevin Buzzard , say in a blog post? Or @Peter Scholze ? I'm itching to publicise the fact, but I won't jump the gun this time....

Peter Scholze (Jul 14 2022 at 22:17):

This is really up to Adam, Johan, Kevin, and the others

Riccardo Brasca (Jul 14 2022 at 22:31):

I have to admit I wrote this on Twitter, but I have like 5 followers

Kevin Buzzard (Jul 14 2022 at 23:01):

I'm waiting for Johan, who right now is drinking beer in Providence.

Johan Commelin (Jul 15 2022 at 01:30):

We'll do bigger announcements tomorrow.

David Michael Roberts (Jul 15 2022 at 02:31):

If anyone is still awake: ok to mention on Twitter?

Filippo A. E. Nuccio (Jul 15 2022 at 02:31):

I think it is really better to wait for Johan to do the first announcement, the others can follow after him. As it is night time where he is now, we should probably wait until he wakes up before doing anything.

Riccardo Brasca (Jul 15 2022 at 02:58):

I've deleted my tweet

Johan Commelin (Jul 15 2022 at 09:04):

Here's what I would propose:

Yesterday Rob and I worked on polishing challenge.lean.
We should polish the blueprint. Currently the graph is not connected. We should fix up the section on real measures.
I will draft a blogpost that we can try to publish around lunch time (East Coast US).
After that, people can start tweeting about it.

Joël Riou (Jul 15 2022 at 09:55):

Congratulations!

Johan Commelin (Jul 15 2022 at 10:01):

Thanks for your help!

Filippo A. E. Nuccio (Jul 15 2022 at 11:27):

I can take up the section on real measures of the blueprint.

Riccardo Brasca (Jul 15 2022 at 11:49):

I can also work on a section of the blueprint if needed. (Or anything elese)

Kevin Buzzard (Jul 15 2022 at 15:17):

@Johan Commelin I've tweeted that there will be an announcment at 2pm during my talk.

Adam Topaz (Jul 15 2022 at 15:37):

@Kevin Buzzard I'm not sure the ICERM stream is accessible publicly

Filippo A. E. Nuccio (Jul 15 2022 at 15:57):

Adam Topaz said:

Kevin Buzzard I'm not sure the ICERM stream is accessible publicly

It seems that nothing is expected today...

Riccardo Brasca (Jul 15 2022 at 15:59):

The "live stream" button doesn't work for Leo's talk, and I am sure it was the same yesterday, so I guess it will be the case also later today.

Riccardo Brasca (Jul 15 2022 at 16:00):

I am talking about the button here.

Junyan Xu (Jul 15 2022 at 16:07):

image.png It's working for me now at https://icerm.brown.edu/live-stream/

Andrew Yang (Jul 15 2022 at 16:07):

I believe it is a bug in the website. It checks the start and end time with your local time, so it only works if you are in the same timezone as them.

Ben Toner (Jul 15 2022 at 16:08):

Direct link to Leo's livestream
Direct link to Kevin's livestream

Andrew Yang (Jul 15 2022 at 16:09):

If there is somewhere that I could post a bug report, I believe the bug is in the lsApp_refreshStreams function in livestream.min.js.

Johan Commelin (Jul 15 2022 at 16:10):

I'll pass it on to ICERM staff.

Last updated: Dec 20 2023 at 11:08 UTC