Real measures

Stream: condensed mathematics

[Adam Topaz]

The branch Radon_wip now has the following isomorphism

def Radon_iso_real_measures (X : Profinite.{0}) (p c : ℝ≥0)
  [fact (0 < p)] [fact (p ≤ 1)] :
  CompHaus.of (X.Radon p c) ≅
  (CompHausFiltPseuNormGrp₁.level.obj c).obj
  ((Profinite.extend (real_measures.functor p)).obj X) :=

in the file src/examples/Radon/main.lean, but it depends on a bunch of relatively small sorries.

If anyone wants to help fill in these sorries, that would be greatly appreciated!

[Adam Topaz]

Here X.Radon p c is defined as the space of all continuous linear maps $\mu : C(X,\mathbb{R}) \to \mathbb{R}$ such that for any clopen partition $X = \cup_i U_i$ of $X$, one has $\sum_i |\mu(\mathbb{1}_{U_i}) | \le c$

[Adam Topaz]

(Well, rather I have used discrete quotients of $X$ instead of clopen partitions.)

[Adam Topaz]

If needed, we could use this to put a comphaus filtered pseudo normed group structure on the space of Radon measures, and show that it's condensification is isomorphic to what we call $\mathcal{M}$ in challenge.lean -- this should be fairly straightforward with what we have now.

[Damiano Testa]

I'm going through src/examples/Radon/setup.lean, if that is helpful!

[Adam Topaz]

I should also mention that the file example/radon_aux (which is completely commented out) has a few proofs that would be useful for some of these sorries!

[Adam Topaz]

For example, I think most of the sorries in Radon/setup are some minor variants of proofs in radon_aux.lean.

[Damiano Testa]

Turns out that I did not have as much time as I hoped: I pushed one proof in Radon/setup, copied over from radon_aux on branch#adomani_radon.

(The link does not work, but the branch name is indeed adomani_radon.)

[Adam Topaz]

@Damiano Testa please feel free to push directly to the Radon_wip branch!

[Damiano Testa]

I just did!

[Adam Topaz]

I added the following to the file examples/radon_measures:

variables (p : ℝ≥0) [fact (0 < p)] [fact (p ≤ 1)]

example (S : Profinite.{0}) :
  (real_measures.condensed p).obj S ≅
  CompHausFiltPseuNormGrp.to_Condensed.obj
  (CHFPNG₁_to_CHFPNGₑₗ.obj $ S.Radon_png p) :=
CompHausFiltPseuNormGrp.to_Condensed.map_iso $
CHFPNG₁_to_CHFPNGₑₗ.map_iso $ (S.Radon_png_iso p).symm

But again, it depends on a whole lot of small sorries (all of which should be props!).

All of this is in the Radon_wip branch, in case anyone wants to help fill in some sorries.

[Adam Topaz]

Once this and the $l^p$ example file that Heather and Filippo are working on are done, then I think we have essentially all of the examples we would want for our project!

[Adam Topaz]

I hope it shouldn't get too much larger ;)

find lean-liquid/src/examples/Radon -name '*.lean' | xargs wc -l
  505 lean-liquid/src/examples/Radon/png_reflects_limits.lean
  244 lean-liquid/src/examples/Radon/LC_limit.lean
  176 lean-liquid/src/examples/Radon/LC_comparison.lean
  173 lean-liquid/src/examples/Radon/png.lean
  331 lean-liquid/src/examples/Radon/setup.lean
   81 lean-liquid/src/examples/Radon/defs.lean
  311 lean-liquid/src/examples/Radon/main.lean
 1821 total

[Adam Topaz]

I killed most of the sorries in the examples/Radon folder, but my laptop is about to run out of battery and I won't have time to work on this for the rest of the day. Anyone want to finish off the last few?

[Johan Commelin]

I'll look at them after I finish the mathlib bump, if nobody beats me.

[Adam Topaz]

You would need to merge master into this branch as well once the mathlib bump is done, but that should be fairly easy since this folder is essentially completely isolated.

[Adam Topaz]

find lean-liquid/src/examples/Radon -name '*.lean' | xargs wc -l
  505 lean-liquid/src/examples/Radon/png_reflects_limits.lean
  254 lean-liquid/src/examples/Radon/LC_limit.lean
  213 lean-liquid/src/examples/Radon/LC_comparison.lean
  253 lean-liquid/src/examples/Radon/png.lean
  331 lean-liquid/src/examples/Radon/setup.lean
   81 lean-liquid/src/examples/Radon/defs.lean
  337 lean-liquid/src/examples/Radon/main.lean
 1974 total

Can you keep it under, say, 2400?

[Johan Commelin]

Let's find out!

[Adam Topaz]

Okay, I killed all the remaining sorries:

find lean-liquid/src/examples/Radon -name '*.lean' | xargs wc -l
  505 lean-liquid/src/examples/Radon/png_reflects_limits.lean
  254 lean-liquid/src/examples/Radon/LC_limit.lean
  352 lean-liquid/src/examples/Radon/LC_comparison.lean
  253 lean-liquid/src/examples/Radon/png.lean
  421 lean-liquid/src/examples/Radon/setup.lean
  169 lean-liquid/src/examples/Radon/defs.lean
  337 lean-liquid/src/examples/Radon/main.lean
 2291 total

I haven't done any linting and this stuff includes a lot of new defs.

[Damiano Testa]

I am removing some unused arguments, but I broke some proof now. I am trying to fix it, but in 10 minutes I will have to go. Should I revert the changes to a working version?

[Damiano Testa]

Actually, all the Radon folder builds on my machine now, so maybe this is good!

[Damiano Testa]

Ok, CI is linting now! It turns out that a lot of compact, t2 assumptions were not needed.

[Damiano Testa]

Branch adomani_lint_universe should pass CI on GitHub but seems to have universe issues on my local machine. This is the reason for not pushing directly to Radon_wip. I do not really know what to do with universe issues, though.

Linting locally examples/Radon/png_reflects_limits.lean gives:

/- The `check_univs` linter reports: -/
/- THE STATEMENTS OF THE FOLLOWING DECLARATIONS HAVE BAD UNIVERSE LEVELS. This usually means that there is a `max u v` in the type where neither `u` nor `v` occur by themselves. Solution: Find the type (or type bundled with data) that has this universe argument and provide the universe level explicitly. If this happens in an implicit argument of the declaration, a better solution is to move this argument to a `variables` command (then it's not necessary to provide the universe level).
It is possible that this linter gives a false positive on definitions where the value of the definition has the universes occur separately, and the definition will usually be used with explicit universe arguments. In this case, feel free to add `@[nolint check_univs]`. -/
#check @CompHausFiltPseuNormGrp₁.create_iso_from_level /- universes [u_1, u_2] only occur together. -/

and some doc-blames.

These issues arose when I removed some "unused" hypotheses.

[Adam Topaz]

Hmmm... I'll try to take a look later today

[Adam Topaz]

@Damiano Testa if you explicitly specify that both X and Y are in CompHausFilt...Grp_1.{u} (i.e. explicitly add the u), in that declaration, does that fix the issue?

[Damiano Testa]

Sorry, I left my computer: I will try to look at it in a couple of hours.

[Adam Topaz]

Well, in any case, everything in the file where that problematic declaration is made should be in the same universe level u. I would guess that adding the universe parameter explicitly everywhere would fix the issue

[Damiano Testa]

Adam Topaz said:

Damiano Testa if you explicitly specify that both X and Y are in CompHausFilt...Grp_1.{u} (i.e. explicitly add the u), in that declaration, does that fix the issue?

Adam, fixing the universe worked! Locally, I only see doc-blames. I pushed my branch to GitHub: if it again compiles with no errors, I will merge Random_wip with it.

Btw, even without the universe fix, CI was happy and green.

[Adam Topaz]

Great! And many MANY thanks for your help Damiano!

[Damiano Testa]

Ok, I have pushed the version that compiled and added 2 (or maybe 3) doc-strings.

[Damiano Testa]

Adam Topaz said:

Great! And many MANY thanks for your help Damiano!

No worries! It was really all very easy: Lean was guiding me through unused assumptions and most of them were typeclass assumptions, so nothing else to fix!

[Damiano Testa]

I also just pushed over doc-strings for Radon.setup. I will probably not have any more time today to add more doc-strings, though.

[Damiano Testa]

I thought that I had only added doc-string, but the build failed. I have to leave now: feel free to revert to the previous successful build: I do not know what went wrong with the doc-strings...

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/pull/113

[Johan Commelin]

So here's a thing we should discuss: I think I would like all of examples/* to be as readable as possible.
So what do you think of moving 90% of the Radon stuff to a new (top-level?) directory. And then only have some demo stuff in the examples/ dir?

[Adam Topaz]

Fine with me!

[Adam Topaz]

Let me do it now

[Adam Topaz]

Ok I moved it. I think I fixed all the imports, but let's see if CI agrees

[Adam Topaz]

The examples/radon_measures file is self contained as far as I'm concerned.

[Damiano Testa]

I'm going to push some typos in doc-strings, if that's alright with you.
(Although I might wait for CI to finish anyway!)

[Adam Topaz]

I was a little haphazard with some docstrings, please go ahead!

[Damiano Testa]

Adam Topaz said:

I was a little haphazard with some docstrings, please go ahead!

Some of the "copy-pasted" ones, were not even copy-pasted! :rofl:

[Damiano Testa]

Jokes aside, the doc-strings look great! I am always grateful when I can read some words, before parsing Lean code.

[Adam Topaz]

Hmm after @Damiano Testa 's comment about docstrings vs comments in the examples folder, I looked more closely at some of the other files, and we seem to have a mix of /-, /-- and /-!. We should probably come up with something consistent. What do you think we should do?

[Adam Topaz]

I guess we're intending for these files to be "literate lean" (analogous to literate haskell, literate agda, etc.). I guess we have a standard way to do this, but I never thought about such issues.

[Damiano Testa]

My impression is that the examples folder is likely one that will get the attention of the large number of mathematicians. For this reason, I think that it will probably not be a "typical" literate file. I tend to use /- comments for remarks that are either helpful to maintain a proof or inside an actual tactic block, to guide what is going on. In the case of the examples folder, I think that the code should not need any such comments, but it would probably be beneficial if it were much more verbose than usual mathlib (or even lean-liquid) files.

For this reason, Adam, I thought that your comments would have fit well as doc-strings.

[Damiano Testa]

In fact, I wonder whether the examples folder should also contain some counter-/non-examples, since, for me at least, they are also very useful.

[Adam Topaz]

As I see it, the only benefit of docstrings over comments is that they are used by docgen to generate documentation.

[Adam Topaz]

Well, that and by the vscode/emacs extensions to display the docstring of a given declaration.

In this respect, I don't really see any reason to add docstrings to examples

[Damiano Testa]

I think that in my mind, docgens for lean-liquid were a reality and I was following the conventions that I would use for mathlib, in this respect.

Still, even if there will never be automatically generated documentation for the whole of lean-liquid, maybe the examples folder could be an exception and still have some form of (possibly rudimentary) exposed web-page.

[Adam Topaz]

The correct thing to do is probably just use /-! for everything

[Adam Topaz]

(or almost everything)

[Adam Topaz]

Well, in any case, since this affects all the example files, we should probably just make whatever change we need to once the rest of the files are done.

[Johan Commelin]

Yeah, I think using /-! everywhere makes sense.

[Johan Commelin]

But in the end it doesn't matter too much I guess.

[Adam Topaz]

The nice thing about something like this

A test of literate lean programming

import category_theory.limits.has_limit

open category_theory

def test : nat := 0

[Adam Topaz]

is that it displays nicely in github

[Adam Topaz]

A test of literate lean programming

Here is a lean code block:

import category_theory.limits.has_limit

open category_theory

def test : nat := 0

And some more plain markdown.

[Adam Topaz]

We could easily write some script to scrape the lean blocks into a separate file to ensure it compiles.

[Adam Topaz]

maybe this can even be part of leanproject?

[Adam Topaz]

Since github renders latex now, this could be a really nice feature

[Johan Commelin]

I think we can look into that. But it's future work.

[Johan Commelin]

I would suggest merging the Radon PR now. I'm happy with the examples file.

[Johan Commelin]

We can then standardise docstrings etc in future PRs.

[Johan Commelin]

@Adam Topaz @Damiano Testa do you agree?

[Damiano Testa]

I also agree!

[Adam Topaz]

I clicked "merge"

[Yaël Dillies]

@Sky Wilshaw recently set up docgen for Con(NF) and I love it. I highly encourage you to do the same.

[Adam Topaz]

But that will reveal how messy we've been!

[Yaël Dillies]

The first step towards redemption! :stuck_out_tongue_wink:

[Yaël Dillies]

I already took a stab at fixing the type of comments in some files a while back. I could finish that up quickly if you want me to.

[Johan Commelin]

@Peter Scholze I think examples/ now contains a nice set of "demos" to illustrate the ingredients of the main statement. Only an example of a p-Banach is missing, but that's WIP. Are there other things you would like to see?
Or do you have questions about what is currently there?

[Peter Scholze]

Thanks, that looks quite convincing!

Someone just told me the following psychological effect (basically confirmation bias, but I found it striking nonetheless). Person A makes up a rule of which sequences of three numbers are "good" (the others are "bad"). The job of Person B is to figure out the rule. To get started, A gives an example of a good sequence. For example, they might say "1,2,4" is good. Then B asks "is 1,3,6 good?". A: Yes. B: Is 1,4,8 good? A: Yes. B: Is 1,5,10 good? A: Yes. B: Is the rule that 1,n,2n is good? A: No. B: Is 1,6,12 good? A: Yes. B: Is 1,7,14 good? A: Yes B: But you see, the rule is that 1,n,2n is good! A: No, that is not the rule.

Apparently people are much rather trying to confirm their idea of what the rule is, then trying to prove it false by finding counterexamples. (In the experiment, A chose the rule "any increasing sequence is good", but virtually no person B ever chose any sequence violating that...)

In the case at hand, I am psychologically predisposed to think that the computer is accurately capturing the mathematics, and your examples are confirming this; sometimes you've added lots of syntactic sugar to make it look seamless. But somehow these are all "positive" examples. I'm not exactly sure what I'm asking for; I guess I'm just currently feeling that mathematics remains a human activity, because if I were to truly check that the computer did the right thing, I would have to unravel the whole proof in my head and convince myself that it all adds up. (You might argue that I only need to check your examples file, but I'm not sure; for one, there's too much syntax I don't really understand and where something sneaky might hide; for the other, the examples files don't actually contain the definitions (because those need a lot of background...), so the above tale on confirmation bias becomes relevant, I think.)

PS: In line 32 of Ext.lean, you say that the example gives the isomorphism of Ext-groups functorially in X (but not Y?). Why is functoriality in X built in? To me the statement reads like a non-functorial isomorphism. (Which probably just confirms that I don't actually understand what the Lean code means...)

[Johan Commelin]

Thanks for your input! I very much agree that mathematics is a human activity. But I also think that using a computer is a human activity (-;
I guess your 3-number-sequence tale is saying that we should somehow look for counter-counter-examples? Not sure what that means...

[Johan Commelin]

Peter Scholze said:

PS: In line 32 of Ext.lean, you say that the example gives the isomorphism of Ext-groups functorially in X (but not Y?). Why is functoriality in X built in? To me the statement reads like a non-functorial isomorphism. (Which probably just confirms that I don't actually understand what the Lean code means...)

Good point. It is actually functorial on both objects. But as you rightly observe the statement as written only gives an isomorphism on objects and doesn't treat morphisms at all. So the documentation on the line above is not exactly in sync with the Lean code.

[Peter Scholze]

Johan Commelin said:

Peter Scholze said:

PS: In line 32 of Ext.lean, you say that the example gives the isomorphism of Ext-groups functorially in X (but not Y?). Why is functoriality in X built in? To me the statement reads like a non-functorial isomorphism. (Which probably just confirms that I don't actually understand what the Lean code means...)

Good point. It is actually functorial on both objects. But as you rightly observe the statement as written only gives an isomorphism on objects and doesn't treat morphisms at all. So the documentation on the line above is not exactly in sync with the Lean code.

Well, please make sure the comments and the Lean code are in sync. In that example, I could "feel" that something is not quite right. For some of the claims about Radon measures, there's too much syntax for me to understand what's really going on, and I simply have to trust you that the Lean code means what you write in the comments.

[Johan Commelin]

@Peter Scholze If there is Lean code in examples/* that you cannot read, that means we didn't do our homework well. Please flag such lines, so that we can try to improve them.

[Peter Scholze]

Let me flag two things:

"(f + g).down.val s = f.down.val s + g.down.val s" -- I have no idea what .down.val means.

"inducing (λ μ : filtration (S.Radon_png p) c, embedding_into_the_weak_dual p S μ) := ⟨rfl⟩" -- Here I think I'm confused why you have to write some \lambda code (which I kind of understand, but is very far from mathematical notation); can you not simply use the map embedding_into_the_weak_dual ? Or is the code just about restricting to a filtration step?

[Peter Scholze]

Also, what you call "embedding" is only a map in the Lean code.

[Peter Scholze]

I guess strictly speaking with your examples, everything could be zero. You would have to argue that the elements constructed via the example on line 96 give the expected linear functionals on continuous functions, otherwise those example elements might just be zero.

[Peter Scholze]

Maybe another required example file would be for profinite sets, actually. Maybe all your profinite sets in universe level 0 are just finite sets?

[Peter Scholze]

Regarding the \lambda code: I must admit that it took me a long time to realize that this is not about two elements \lambda and \mu of filtration (S.Radon_png p) c!

[Peter Scholze]

Also, in this \lambda-code line: Why is the rfl in angle brackets?

[Peter Scholze]

Also, in Ext.lean, you can't seriously imagine I can read a line like

"example (n : ℕ) (X Y : 𝓐) : ((Ext' n).obj (op X)).obj Y =
((Ext n).obj (op ((single _ 0).obj X))).obj ((single _ 0).obj Y)"

:upside_down:

[Johan Commelin]

Ok, that's useful feedback! We'll try to improve things!

[Peter Scholze]

Sorry for playing devil's advocate here!

[Peter Scholze]

Actually, can you explain what the ".obj" is doing?

[Peter Scholze]

Is it that a functor is some bundled information, and in particular it's a map on objects, and one has to say that explicitly?

[Peter Scholze]

I'm sure you've already tried to make the API for functors nicer, but it would really be good if Lean could figure out itself that if you apply a functor to something whose type is that of an object of the source category, it's supposed to apply the map on objects (while if the type is that of morphism between objects, it applies the map on morphisms)

[Johan Commelin]

Yes, unfortunately we have to write F.obj X and F.map f at the moment. We tried to have better notation, so that you could just write F X and F f, but it was too brittle. However, we have good hopes that in Lean 4 we can actually make this work.

[Yaël Dillies]

In fact I was discussing this just yesterday (making Lean understand that for F : C ⥤ D, X Y : C, f : X ⟶ Y, F X means F.obj X and F f means F.map f) and the .obj bit is fine. What's not is the .map one because it's a function dependent in X and Y in a way that subtly exceeds the limits of our current system.

[Yaël Dillies]

The way to do this currently is using docs#has_coe_to_fun. has_coe_to_fun α β (α : Type*, β : α → Sort*) means that a : α can be thought of as a map of type β a. So what we would want is

instance {X Y : C} : has_coe_to_fun (C ⥤ D) (λ F, (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=

but λ F, (X ⟶ Y) → (F.obj X ⟶ F.obj Y) depends on X and Y, which do not appear in the C ⥤ D argument. Mathematically, this is because a functor is not actually two maps, but a map on objects and many maps on homs.

[Yaël Dillies]

Wait, it is actually two maps, if you quantify over X and Y. So the following works:

import category_theory.functor.basic

open category_theory

variables {C D : Type*} [category C] [category D]

instance : has_coe_to_fun (C ⥤ D) (λ F, ∀ {X Y : C}, (X ⟶ Y) → (F.obj X ⟶ F.obj Y)) :=
⟨λ F X Y f, F.map f⟩

example (X Y : C) (f : X ⟶ Y) (F : C ⥤ D) : F f = F.map f := rfl

[Yaël Dillies]

But now you want a map on the objects as well, so you need a second has_coe_to_fun. And this is where things go haywire

import category_theory.functor.basic

open category_theory

variables {C D : Type*} [category C] [category D]

instance obj_coe : has_coe_to_fun (C ⥤ D) (λ F, C → D) := ⟨λ F, F.obj⟩

instance hom_coe : has_coe_to_fun (C ⥤ D) (λ F, ∀ {X Y : C}, (X ⟶ Y) → (F X ⟶ F Y)) :=
⟨λ F X Y f, F.map f⟩

example (X Y : C) (f : X ⟶ Y) (F : C ⥤ D) : F X ⟶ F Y := F f -- Lean confused

[Yaël Dillies]

If you want to understand what's going on, you need to know what docs#out_param does and I highly encourage you read @Anne Baanen's recent paper on bundled hom typeclasses.

[Yaël Dillies]

In short, Lean doesn't try to guess whether you mean to use F : C ⥤ D as a C → D or as a ∀ {X Y : C}, (X ⟶ Y) → (F X ⟶ F Y) for performance reasons. So it picks whichever it finds first, which is doomed to fail half of the time.

[Adam Topaz]

Johan Commelin said:

Ok, that's useful feedback! We'll try to improve things!

Agreed! That's very useful! It's easy for us to forget that Lean3 is still a different language.

[Adam Topaz]

Here's a start on the profinite example file
https://github.com/leanprover-community/lean-liquid/pull/115

Two additional things that could potentially be added, if you think it's worthwhile:

1. Explain how to view a profinite set as a limit of finite sets.
2. Explain how the proetale topology is defined

[Adam Topaz]

More generally, I would say the example files are not about fully checking the defs all the way down to the axioms, but rather all the way down to mathlib.

[Adam Topaz]

We didn't do that in some cases (e.g. mathlib doesn't have delta functors), but I think that's what we should aim for (within reason)

[Adam Topaz]

Peter Scholze said:

Also, in Ext.lean, you can't seriously imagine I can read a line like

"example (n : ℕ) (X Y : 𝓐) : ((Ext' n).obj (op X)).obj Y =
((Ext n).obj (op ((single _ 0).obj X))).obj ((single _ 0).obj Y)"

:upside_down:

I'm going to introduce a coe to fun for functors just on the object level. Also, I'm introducing a coercion from an abelian category to the bounded homotopy category $X \mapsto X[0]$. With those tricks, we have

/--
`Ext' n (X,B)` is definitionally equal to `Ext n (X, B)`.
We have to manually tell Lean that a coercion is involved in this case using `↑`.
-/
example (n : ℕ) (X Y : 𝓐) :
  (Ext' n (op X)) Y =
  (Ext n (op ↑X)) ↑Y := rfl

I hope that looks a bit more reasonable?

[Adam Topaz]

https://github.com/leanprover-community/lean-liquid/pull/116
I addressed most of Peter's comments above. Please feel free to push to this branch with further fixes!

[Mario Carneiro]

@Yaël Dillies Could you summarize this functor map issue and post it as an MWE on #lean4 ? We might need to do something special to make it work.

[Yaël Dillies]

Sure!

[Adam Topaz]

Can this be accomplished in lean4 with unification hints?

[Reid Barton]

Really just having F X for F.obj X would already be nice. I know this was discussed in the olden days of lean-category-theory. I can't remember what the specific reason for not supporting it was.

[Reid Barton]

Maybe @Scott Morrison knows? It could well be something that no longer makes sense in the context of current mathlib

[Adam Topaz]

I got this to work in Lean4.... but it feels hacky and it probably won't scale

class Quiver (A : Type _) where
  hom : A → A → Type v

structure PreFunctor (A B : Type _) [Quiver A] [Quiver B] where
  obj : A → B
  map : {X Y : A} → Quiver.hom X Y → Quiver.hom (obj X) (obj Y)

instance {A B : Type _} [Quiver A] [Quiver B] : CoeFun (PreFunctor A B) (λ F => A → B) where
  coe := PreFunctor.obj

notation F O => PreFunctor.map F O

example {A B : Type _} [Quiver A] [Quiver B] (F : PreFunctor A B) (X : A) : B := F X
example {A B : Type _} [Quiver A] [Quiver B]
  (F : PreFunctor A B) (X Y : A) (f : Quiver.hom X Y) : Quiver.hom (F X : B) (F Y) := F f

[Adam Topaz]

Removing the : B in the last line breaks the last example

[Adam Topaz]

Another option

structure Quiver where
  carrier : Type u
  hom : carrier → carrier → Type v

instance : CoeSort Quiver (Type _) where coe := Quiver.carrier

structure PreFunctor (A B : Quiver) where
  obj : A → B
  map : {X Y : A} → A.hom X Y → B.hom (obj X) (obj Y)

notation F O => PreFunctor.obj F O
notation F O => PreFunctor.map F O

example {A B : Quiver} (F : PreFunctor A B) (X : A) : B := F X
example {A B : Quiver} (F : PreFunctor A B) (X Y : A) (f : A.hom X Y) : B.hom (F X) (F Y) := F f

[Johan Commelin]

Harris wrote

Thus formalization inevitably requires a human decision to read a proposed formalization as a translation of the human proof: in other words an act of faith, like the acts of faith that sustain human mathematics in this first half of the 21st century — in the refereeing process, in the published documents, and in the seminar room. Formalization can only eliminate the epistemological antinomies if humans are excluded from the process entirely, and the machines are left to sort it out among themselves.

over at https://siliconreckoner.substack.com/p/game-over-for-mathematicians .
I guess that it's the same kind of thing that Peter was also talking about when he said that mathematics remains a human activity.

[Jireh Loreaux]

I realize that Harris is talking about the translation here, and I agree with the sentiment that mathematics remains a human activity, but I think Harris has missed a key distinction. In mathematics as practiced today, the act of faith is in the proofs of the proposed results. Definitions are (and have been) frequently taken for granted. In fact, we often conflate multiple definitions for convenience by appealing to some notion of equivalence between the two. If I go to a conference on C⋆-algebras and start talking about them, no one will wonder whether or not I'm talking about a different definition than the one they are used to; in this sense, definitions (frequently) are an implicit act of faith.

In contrast, when formalizing, it is only the definitions that one must take on faith, assuming one can adequately parse the statements of the theorems. In so doing, we have completely eliminated the previously required act of faith, and only now do we (i.e., your everyday mathematicians) realize that the implicit act of faith for definitions really should have been explicit all along.

Moreover, by formalizing enough theorems, one can verify the usual behavior of a given object, thereby minimizing the possibility that they are defined in a way sufficiently different to cause problems. That is, if it looks like a duck and quacks like a duck, it is generally (although admittedly not always) a duck.

So, does formalization completely eliminate all acts of faith for a human to "verify" for themselves the correctness of a certain theorem? No, but it greatly shifts where our faith rests.

[Frédéric Dupuis]

Also, when formalizing, you know that someone talking about X is necessarily using the same definition of X as everyone else using the same system.

[Mario Carneiro]

... when formalizing in mathlib, at least.

[Reid Barton]

at least, if both people are using the same version of mathlib :upside_down:

[Matthew Ballard]

“We are very good at figuring out things that computers can’t do. If we were to imagine a future in which all the theorems we currently know about could be proven on a computer, we would just figure out other things that a computer can’t solve, and that would become ‘mathematics.’ ”

[Matthew Ballard]

Ellenberg's quote here has stayed with me

[Peter Scholze]

I guess my perspective here was that for this project, it's unfeasible to check the definitions. To a human it's easier to convince themselves that there are enough ideas in there to get a proof, than to say with absolute certainty that all the definitions entering the theorem statement are correct.

Even after your example files, it could be that a lot of things are secretly zero, and it's an absolute impossibility for me to read enough of the Lean code to check all your definitions -- it's just way too much buildup! (And this checking would require me to have a much better understanding of Lean's syntax.)

Arguably, this issue becomes less pressing once a lot of stuff is in a trusted library like mathlib. So if somebody proves a theorem and formalizes it, then the referee has an easy job if all the definitions entering their main theorem are in that library. But much of the development of mathematics lies in finding good definitions! So in a paper with new definitions and theorems about those new definitions, the refereeing process will be almost as tedious as before, if not more (as now one has to be make sure the definitions are absolutely correct before they can be allowed to enter the library).

What happened in the first half of LTE is that I could really see how you were following the manuscript line-by-line and, in the process of carefully translating it into Lean, catching a number of small slips. This type of process is certainly something where formal proof verification is doing an excellent job, and it really radically changed my confidence in the argument. However, the second half of LTE has not added anything to my confidence (but it was already at 100% ;-) , so maybe that's not saying much). But of course it's a really impressive achievement to get all this mathematical machinery done in Lean!

[Johan Commelin]

That's actually an interesting observation, I think. Because initially, I think part of the reasoning for making 9.1 the final goal of the challenge as opposed to 9.4/9.5 was that it is easy to check the statement of 9.1 whereas checking that we got all the definition entering into 9.4/9.5 right would be a lot nastier.
And probably this is still true for an outsider. What I mean is that Peter is probably one of the few people (Dustin being another)

[I]n the first half of LTE is that I could really see how you were following the manuscript line-by-line and, in the process of carefully translating it into Lean, catching a number of small slips. This type of process is certainly something where formal proof verification is doing an excellent job, and it really radically changed my confidence in the argument.

could be true. And for the rest of the world, it is a lot easier to be convinced by a formal verification of 9.1 then by the results of the first half that led up to 9.4/9.5.

[Peter Scholze]

Yes, that's right. I think for an outsider, it's definitely easier to be convinced by reading some of the definitions and examples that you give, in order to trust that you probably have the definitions right, and to read the final statement (which certainly is very clean!). But I'd argue that this process will not get up to 100% confidence, and I feel that in this specific situation for me, the confidence level I can get via this procedure is below the one I have via other means.

[Johan Commelin]

I do think that these observations have never really showed up before.

[Johan Commelin]

In other big projects, like 4CT, Odd-Order, Kepler, etc... checking the statement is feasible for most people after they spend a little amount of time learning some syntax.

[Damiano Testa]

This feels a little like the P vs NP distinction, possibly in reverse: some statements are easy to parse, but their proofs are hard. With the P vs NP analogy, parsing the statement is P, while proving it is NP.

This is probably what happens in the (most) of the examples of formalization so far.

In the case of LTE, even the statement is diffcult to parse, regardless of whether it is the formalized statement or the "informal" one.

[Peter Scholze]

I agree.

I guess something I've said a while ago (incidentally in an e-mail to Michael Harris...) is relevant here again: To me, the main obstacle in writing papers is often not finding the proofs, but finding the "right" definitions, and stating the "relevant" theorems. If this is done right, the proofs almost come for free. But for such papers, formalization is of little use -- they could only ever check the proofs (and catch the occasional slip), but those were always the part that was relatively straightforward.

[Peter Scholze]

The proof in LTE really is one of the few examples where I thought we had the right definitions and stated the relevant theorem, but the proof was still hard and unintuitive.

[Johan Commelin]

Do you think the situation for this particular proof has changed compared to 2 years ago?

[Johan Commelin]

E.g. by the insight that Gordan's lemma plays a non-trivial key role.

[Peter Scholze]

What do you mean by "the situation"? If you mean that I find it hard and unintuitive, that's gotten slightly better, but is still true.

[Johan Commelin]

Yeah, that's what I meant.

[Peter Scholze]

It's still the case that I have not been able to convey the idea of the proof in speaking to any other mathematician...

[Peter Scholze]

i.e., of the kind that even if they did not fully understand all the details, they could not go home and reconstruct the argument from the hints I gave

[Johan Commelin]

Maybe some definitions are still missing? But they would probably not be used outside this proof.

[Johan Commelin]

LTE builds a lot more theory around pseudo-normed groups. But I understand that this doesn't really pay off on paper.

[Peter Scholze]

Well, that's certainly a relevant notion, and I've certainly toyed around with making a bit more theory there. But it doesn't really get to the heart of the matter...

[Johan Commelin]

I think the hardest bit is maybe the "normed homological algebra". You would like to say "assume that $M$ is a splittable pseudo-normed group, then it is just a spectral sequence argument".

[Johan Commelin]

Proving that $\bar{\mathcal{M}}$ is splittable boils down to Gordan's lemma. That part is quite intuitive, I think.

[Johan Commelin]

But even the statement of 9.5 is pretty gnarly, because of all the norms and inequalities.

[Peter Scholze]

Hmm yes. The problem is that all these notions come with their own $\epsilon$ and $\delta$, etc.

[Johan Commelin]

Right, if that could somehow be packaged up in a convenient way, then there might be a chance that 9.6 + 9.6=>9.5 becomes "just a spectral sequence" argument.

[Peter Scholze]

For the pseudonormed stuff, there was some really nice discussion also here on the chat about possible formalizations (as some monoidal functors from $\mathbb R_{\geq 0}$ or something), but nothing really gives a nice abelian category or anything

[Johan Commelin]

I think one example of such "convenient packaging" is big-O notation. Of course that doesn't help us here. But maybe a suitable analogue could be made.

[Johan Commelin]

So that once that notation is in place, you can run an "algebraic" argument.

[Peter Scholze]

I very much would want to have such a repackaging of the proof!

[Johan Commelin]

I spent the last week or so, trying to see where there is movement in the proof. But (unsurprisingly) there is very little flexibility. There are two ideas that I feel I haven't exhausted yet:

1. The original proof has to deal with the very inexplicit nature of Breen--Deligne resolutions. Can we get some juice out of working with $Q'$?
2. The original proof uses in one very particular place that deep restrictions have a small operator norm. Can we use this to our advantage in more places?