## Stream: general

### Topic: XenaProject blog posts

#### Marc Huisinga (Jul 03 2020 at 14:09):

some people have expressed interest in kevin's xenaproject lean posts being posted somewhere in this zulip so that they don't miss it, so i am making this topic.

use this topic for posting and discussing new and old xena blog posts.

#### Marc Huisinga (Jul 03 2020 at 14:10):

newest post: Equality, specifications, and implementations

Thank you!

#### Sebastian Ullrich (Jul 03 2020 at 14:25):

The blog does have an RSS feed :) . However, it might not make much sense to post blog updates to the same #rss channel as repo updates

#### Marc Huisinga (Jul 03 2020 at 14:29):

Sebastian Ullrich said:

The blog does have an RSS feed :) . However, it might not make much sense to post blog updates to the same #rss channel as repo updates

i hope that this topic will already work organically. most avid lean users likely read kevin's blog anyways, so someone will most certainly post it eventually now that there's a place for it. in addition, we can also use this topic for discussion!

#### Patrick Massot (Jul 03 2020 at 14:29):

Yes, this RSS question also came to my mind, but I didn't suggest it because this has a clearly distinct flavor from what we put in the rss stream.

#### Sebastian Ullrich (Jul 03 2020 at 14:34):

It might be possible to use different streams for different feeds, but I don't mind this being solved by manual labor

#### Kevin Buzzard (Jul 03 2020 at 15:13):

For what it's worth, of course I don't mind what happens ultimately wrt posting here, but I've not been posting these things here myself here because for me the point of this Zulip is that it is a professional place where experts hang out and help solve Lean problems and make progress with lean and mathlib. My blog posts are just supposed to be for a general mathematical audience. I have no qualms advertising them on the Xena discord but that's full of non-experts.

#### Marc Huisinga (Jul 03 2020 at 15:28):

i think that exactly because they are for a general mathematical audience, they are of interest to the experts here.

discussion on how to improve the theorem proving experience also seems to be an important part of this zulip, and for that this kind of perspective (and any related discussion) is very valuable.
after all, judging from twitter, even plenty of people that build theorem provers read your posts (likely for that exact reason!).
besides, as a cs person myself i found many of your posts very helpful, not only to understand how lean works, but also to gain a broader perspective in terms of how decisions in the lean design impact the people formalizing mathematics :)

#### Marc Huisinga (Jul 03 2020 at 15:41):

(this is in part why i am in favor of this topic working organically as opposed to being run by an rss bot: if people do not deem some post from your blog interesting for this zulip, perhaps because it is entirely unrelated to lean, they will simply not post it)

#### Bryan Gin-ge Chen (Jul 03 2020 at 16:10):

This is a very naïve and probably not well-thought-out question about the latest blog post. When we want to work with specifications in Lean, we usually use structures or type classes, right? Is the issue with using structures for reals that the API is way too big to hide in a structure?

#### Mario Carneiro (Jul 03 2020 at 16:20):

no, we could certainly do that

#### Mario Carneiro (Jul 03 2020 at 16:21):

indeed, when we get to lean 4 I'm thinking of setting up a single structure constant R : RealInterface := ... that proves that there exists an implementation of "the reals" so that we really can get some isolation

#### Mario Carneiro (Jul 03 2020 at 16:22):

but I think there are not too many times when we want a hard barrier like that

#### Mario Carneiro (Jul 03 2020 at 16:25):

@Kevin Buzzard said:

But you’ll find that it’s a real bore with Dedekind cuts, because Dedekind cuts have this annoying property that you need a convention for the cuts corresponding to rational numbers: whether to put the rational number itself into the lower or upper cut. Neither convention gives a nice definition of addition. You can’t just add the lower cuts and the upper cuts, because the sum of two irrationals can be a rational.

Actually addition on dedekind cuts isn't as bad as this. You can say that a dedekind cut is just the lower set (exclusive), and then pointwise addition works just fine. The thing about multiplication is true, but you can avoid the problem by only defining positive reals

#### Alex J. Best (Jul 03 2020 at 16:26):

From a related file I'm (serendipitously) working on, how does class conditionally_complete_linear_ordered_field (F : Type*) extends discrete_linear_ordered_field F, conditionally_complete_linear_order F sound as the structure?

#### Patrick Massot (Jul 03 2020 at 16:28):

Mario Carneiro said:

indeed, when we get to lean 4 I'm thinking of setting up a single structure constant R : RealInterface := ... that proves that there exists an implementation of "the reals" so that we really can get some isolation

The question is: can we do that and still use the notation ℝ to denote some implementation (we don't care which one). And I don't mean having {ℝ : Type} [RealInterface ℝ] (x y z : ℝ)

#### Mario Carneiro (Jul 03 2020 at 16:29):

The idea would be that R there is now a bundled type + real axioms, and so we would define def ℝ := R.carrier and so on

#### Mario Carneiro (Jul 03 2020 at 16:29):

This is still just one type, we just don't know what type it is

#### Patrick Massot (Jul 03 2020 at 16:30):

Does it mean that coercions would be involved everytime we manipulate a real number?

how so?

#### Mario Carneiro (Jul 03 2020 at 16:30):

no more than currently

#### Patrick Massot (Jul 03 2020 at 16:30):

Ok, then I really don't understand what you mean.

#### Mario Carneiro (Jul 03 2020 at 16:31):

Since this ℝ type will be a complete ordered field you can write 2 : ℝ as normal

#### Mario Carneiro (Jul 03 2020 at 16:32):

the only thing that will be different is that you will not be able to prove theorems about ℝ by proving them about the underlying cauchy sequence representation

#### Mario Carneiro (Jul 03 2020 at 16:33):

which we are already doing for the most part by making real irreducible

#### Patrick Massot (Jul 03 2020 at 16:33):

Ok, sounds good, especially if it allows us to finally switch to Bourbaki reals :wink:

#### Mario Carneiro (Jul 03 2020 at 16:33):

The difference with lean 4's constant is that now there will be a literal meta theorem saying that you can swap out for dedekind cuts and nothing will break

#### Chris Hughes (Jul 03 2020 at 16:37):

So this will make it easier to apply polynomial theorems to our favorite super fast polynomial implementation or whatever?

Nice

#### Mario Carneiro (Jul 03 2020 at 16:43):

Ah, I hadn't thought of that. Indeed, if there are any buggy lean tactics that don't take the hint when they see irreducible, constant will be able to block them before they waste too much time

#### Sebastian Ullrich (Jul 03 2020 at 16:50):

At this point I should probably mention that @Leonardo de Moura and I are at least considering introducing a simple module system for Lean 4 (where module = file, not functors involved). It would allow you to view a def inside a file as a constant outside of it (by default or not? All details TBD). The main motivation is to drastically speed up recompilation while programming in Lean, but as discussed, hiding implementations can be useful while proving as well.

#### Mario Carneiro (Jul 03 2020 at 17:10):

I would recommend against tying file structure to this behavior. What about a module keyword that acts mostly like a section, but makes everything in the section private, then compile the module to a structure + an implementation of that structure as a constant + re-exporting the fields of that structure as theorems with the original chosen names

#### Mario Carneiro (Jul 03 2020 at 17:11):

(note in particular that this does not require any kernel changes)

#### Mario Carneiro (Jul 03 2020 at 17:12):

I would be very happy if we could have a feature like Coq modules but with all the mess going through a "module compiler" so that there is no kernel impact

#### Sebastian Ullrich (Jul 03 2020 at 17:20):

I'm not planning to change the kernel, this would be implemented in the import logic (which also means that we could drastically reduce the amount of data being imported). Autogenerating structures is not realistic when the majority of declarations in each file should be made opaque (at least for programming). Think of it as GHC's interface files produced for separate compilation.

#### Mario Carneiro (Jul 03 2020 at 17:25):

maybe a special variant of import that triggers this behavior?

#### Mario Carneiro (Jul 03 2020 at 17:25):

I think in mathlib this would be a small minority of files, you can't just seal all defs

#### Kevin Kappelmann (Jul 03 2020 at 17:26):

+1 for not tying this to files but introducing something like a module keyword.

#### Sebastian Ullrich (Jul 03 2020 at 17:27):

Yes, the default import would most likely be unchanged

#### Mario Carneiro (Jul 03 2020 at 17:27):

I will point out that Haskell also uses module, even though it's written once at the top of every file so it's easy to confuse with file based management

#### Mario Carneiro (Jul 03 2020 at 17:28):

Alternatively, this could be tied to some attribute of the definition. I imagine that most of the defs you want to apply this to are what lean 3 would call meta defs

#### Mario Carneiro (Jul 03 2020 at 17:29):

congratulations, they aren't meta anymore, but that doesn't change the fact that you have no intention to prove any property about them. Maybe make that explicit by using constant

#### Mario Carneiro (Jul 03 2020 at 17:30):

Do you have an example where you need a definition to be transparent in the file and opaque in the next file?

#### Sebastian Ullrich (Jul 03 2020 at 17:34):

You mean apart from real etc? Well, maybe you still need it to be transparent in the next file, but at some point you want to seal it and that will most likely be at a file boundary.

#### Sebastian Ullrich (Jul 03 2020 at 17:37):

For programming you want every definition sealed unless you want it to be inlined or specialized

#### Mario Carneiro (Jul 03 2020 at 19:42):

In the case of real there is a well defined module boundary. I'm wondering about the programming case

#### Mario Carneiro (Jul 03 2020 at 19:43):

Like you say, it seems like you want every definition sealed immediately, in which case there isn't really a reason to use def in the first place since constant already expresses this

#### Mario Carneiro (Jul 03 2020 at 19:44):

Do you think you could achieve your performance goals by using constant everywhere and not changing import for big programming developments?

#### Sebastian Ullrich (Jul 04 2020 at 13:51):

Files are a relatively natural boundary for limiting interprocedural optimizations, especially during development (you rarely want to build such high-level languages completely without optimizations). For example, "Without -O, GHC does inlining within a module, but no cross-module inlining.".

#### Sebastian Ullrich (Jul 04 2020 at 13:56):

But I can see that the requirements for programming and proving might not be that similar here after all, so I'd be happy to see someone build a modules-as-structures system in Lean 4. That is more or less what we imagined a superior replacement for parameter could look like after all.

#### Gabriel Ebner (Jul 05 2020 at 17:28):

Today, Kevin shared his thoughts about the traditional field axiom $\frac x 0 = 0$:
https://xenaproject.wordpress.com/2020/07/05/division-by-zero-in-type-theory-a-faq/

#### Yury G. Kudryashov (Jul 05 2020 at 17:52):

Today we have nnreals and can define nnreal.sqrt to be the "mathematically correct" square root. Then a * b will figure out 0 ≤ a * b automatically.

#### Kevin Buzzard (Jul 05 2020 at 18:20):

You can't subtract them though :-)

#### Jason Rute (Jul 05 2020 at 18:43):

For a while now @Jeremy Avigad has been saying that formal theorem proving presents a unique opportunity for logicians and philosophers of mathematics. Just like the early 1900s when logicians were starting to make formal vague terms like "theorem", "proof", and "algorithm", we have an opportunity to refine those ideas to fit practicing mathematics. (The example Jeremy often used was that formally logicians say that a "proof" is a sequence or tree of statements with certain properties, but is that really how mathematicians think of a proof?) I think this problem of partial functions is a great use case for Jeremy's proposed program. When we say a - b, a/b, sqrt a, or the push forward of the probability measure mu under the map f, we have all these assumptions in mind. Is there a formal logic (maybe very different from anything out there) that captures these statements and makes operations like rewriting seamless. Of course this new logic may only be an impossible pipe dream, but it doesn't seem beyond the realm of possibility. (And if it does exist, it may have applications for programming language design as well, since dividing by zero or taking the 101th element of a list with only 100 elements can lead to bad errors in code.)

#### Jason Rute (Jul 05 2020 at 18:54):

Also, if there is no such logic (or it is hard to find), because this is all related to the ambiguity of human language, then I hold out hope for soft tools like machine learning, especially neural based AI, which has shown itself to be good at working with incomplete and vague information. An AI agent could realize that a - b + b = a is "morally true" (as I've heard mathematicians call it). Then it could prove a lemma automatically by rewriting with that assumption, and then go back and "dot all the i's and cross all the t's" by proving the necessary assumptions needed to make the rewrites work. Again, this may seem like a pipe dream, but I think the tools we have are making a lot of progress in that direction.

#### Kevin Buzzard (Jul 05 2020 at 19:09):

A proof is a solution of a level in a computer game

#### Jeremy Avigad (Jul 06 2020 at 11:24):

I agree with Kevin that this Lean's handling of division by zero isn't the most important issue facing formalized mathematics today, but mathematicians are right to show some concern. It would be disconcerting if it turned out that some important formalized theorem about perfectoid spaces turned out to be false when we change the value of 1/0. Right now, we don't have good ways of ensuring that won't happen, or even determining whether it is the case.

There is a nice survey of logics for partial terms by Feferman: https://math.stanford.edu/~feferman/papers/definedness.pdf. The best known implementation of a proof assistant that builds in partiality is Farmer's IMPS (https://link.springer.com/article/10.1007/BF00881906), but I can't speak for its usability.

The two common ways of dealing partiality in a type theory involve either modifying the output type to take an undefined value (option or roption) or modifying the input type to restrict the valid inputs, with the condition bundled as a subtype or unbundled as a precondition. My preferred solution for division would be to have the fact that the denominator is nonzero is a precondition, one that is handled by automation so that we rarely think about it.

It is sometimes not entirely clear what the mathematics should mean when we deal with partial functions. There are two ways of interpreting the statement "f(x) -> 0 as x -> 0" when f is partial, described here: https://math.stackexchange.com/questions/2883458/what-is-the-right-definition-of-the-limit-of-a-function/2883484#2883484. A couple of years ago I generalized the tendsto relation to cover partial functions and multifunctions (https://github.com/leanprover-community/mathlib/blob/master/src/order/filter/partial.lean), in the hopes that this would be useful for set-valued analysis. But I never got back to it.

#### Kevin Buzzard (Jul 06 2020 at 12:06):

It would be disconcerting if it turned out that some important formalized theorem about perfectoid spaces turned out to be false when we change the value of 1/0. Right now, we don't have good ways of ensuring that won't happen, or even determining whether it is the case.

Right now we're ok because I suspect that no theorem about perfectoid spaces will ever mention division. But for theorems about Banach spaces maybe life isn't so easy.

#### Chris Hughes (Jul 06 2020 at 12:16):

If the theorem mentions division it's always going to be quite easy to prove the statement about partial division given the statement about Lean's division. Maybe not I guess if it mentions division somewhere deep down.

#### Kevin Buzzard (Jul 06 2020 at 12:21):

If a theorem which mathematicians are interested in mentions division then what you're dividing by won't be allowed to be zero, either by theorem or by (possibly unwritten) assumption.

"Does there exists a real number $r$ such that $1/r=0?$ is a good example. It's impossible to find a mathematician who will say "yes" to this, and they will have no complaints about the question being well-posed: we implicitly add the assumption that $r\not=0$ when parsing.

#### Johan Commelin (Jul 06 2020 at 12:55):

It's funny, right. Mathematicians have these promises that they will never do something wrong, hence you can swap out objects and replace them by canonically isomorphic ones...
But if you do this with their field operation, all of a sudden they become very uneasy. It's an implementation detail, but we are getting very close to the boundary of where the "promise" still holds/works.

#### Utensil Song (Jul 06 2020 at 13:12):

The idiomatic way to do it is to allow garbage inputs like negative numbers into your square root function, and return garbage outputs. It is in the theorems where one puts the non-negativity hypotheses.

Just out of curiosity, is the choice of garbage output unique (to make the function total)? Any particular reason to choose 0 except that it seems to be more "neutral" than other choices? When $\infty$ is available, should it be chosen because it's more "extreme" than zero?

I asking this also because something inside me wishes the outputs of further operations on the garbage result are also garbage-ish. Maybe it's just part of the symptoms described in the last part of the post.

The lesson learned here may be: one should not expect sanity from definitions (they should be allowed to be wild), instead the sanity lies in theorems and theorems only.

#### Alex J. Best (Jul 06 2020 at 13:20):

I guess the rule of thumb is that the garbage output should make as many theorems still true without the condition that the input not be garbage as possible, to reduce the proof obligations on the user later.
For the square root of negative reals for example you might want that

lemma (a b : real) : sqrt (a * b) = sqrt a * sqrt b := sorry


this isn't true without some additional assumption, but I believe if you send negatives to zero then you only need to assume one of a or b is nonnegative, but if you use any other fixed number as garbage then you'll need to assume both a and b are nonnegative for this to hold.
The square root function is also still continuous with this definition, which might be nice.

#### Jeremy Avigad (Jul 06 2020 at 14:29):

If a theorem which mathematicians are interested in mentions division then what you're dividing by won't be allowed to be zero, either by theorem or by (possibly unwritten) assumption.

Exactly. So now you prove a theorem formally, and your mathematician friend wants to know: "Why should I be interested in your theorem? I trust my own theorems because I know what they say. But I don't trust all your formal nonsense, especially when you tell me 1/0 = 0."

Right now the best we can do for a formal sanity check is to find a formulation that doesn't mention division and then prove that it follows from your formal statement. But, as Chris says, when the theorem is built on top of definitions that use division all the way down, that's hard to do.

To repeat: I don't think this is the most serious issue we are facing now. But it is a legitimate concern, and there should be better solutions.

#### Mario Carneiro (Jul 06 2020 at 14:30):

But the definitions don't have to avoid division, they just need to not rely on division by zero

#### Jeremy Avigad (Jul 06 2020 at 14:31):

Yes, but how can to determine that they don't?

#### Mario Carneiro (Jul 06 2020 at 14:31):

by looking at them

#### Mario Carneiro (Jul 06 2020 at 14:32):

you have to do this anyway in order to verify the statement is what you expect

#### Mario Carneiro (Jul 06 2020 at 14:34):

Even where there are nontrivial modifications like field, you get a metatheorem like "Let a Lean-field be a field with an operation /' that matches division away from zero and satisfies a /' 0 = 0. Then any theorem about Lean-fields using /' away from zero is also true of fields using division."

#### Kevin Buzzard (Jul 06 2020 at 14:35):

If sqrt(x) were defined to be sqrt(|x|) then sqrt_mul would be true unconditionally. I'm not the first person to observe this.

#### Alex J. Best (Jul 06 2020 at 14:35):

Kevin Buzzard said:

If sqrt(x) were defined to be sqrt(|x|) then sqrt_mul would be true unconditionally. I'm not the first person to observe this.

I was thinking that when I wrote it, we did this for log right?

#### Mario Carneiro (Jul 06 2020 at 14:37):

FWIW I like sqrt x = 0 for negative x because that's the real part of the square root function

#### Jeremy Avigad (Jul 06 2020 at 14:38):

What does it mean to "not rely on division by 0"? If the definitions use our division, and our division takes a value when you divide by 0, the the definitions rely on division by 0. Some of the theorem (x + y) / z along the way do as well.

Mathematicians can (in principle) say that division by 0 is undefined and that the theorems are nonetheless true with that understanding. That is patently false for some theorems in mathlib, and true for others. But how do you tell which is which?

#### Mario Carneiro (Jul 06 2020 at 14:39):

Any assumption that uses division in a statement needs appropriate quantifier bounds to ensure that the value doesn't matter

#### Mario Carneiro (Jul 06 2020 at 14:39):

that is enough to eliminate a large fraction of spurious uses

#### Mario Carneiro (Jul 06 2020 at 14:41):

the use of theorems and proofs that use division by zero along the way doesn't matter, only whether the final theorem statement contains divisions not guarded by a quantifier bound

#### Mario Carneiro (Jul 06 2020 at 14:42):

Kevin's example \exists x, 1/x = 0 is obviously violating this condition, it has a division and no quantifier bound saying x != 0

#### Mario Carneiro (Jul 06 2020 at 14:44):

Something like \exists x > 1, 1 / x = 0, even if the / is Lean-division, is okay because the division occurs in a context where x != 0 is provable

#### Jeremy Avigad (Jul 06 2020 at 14:45):

What does it mean to say a "theorem about Lean-fields uses /' away from 0", especially when there are definitions involved? You need some guarantee that when you unwrap all the definitions and quantifier bounds all the way down, you can prove that anything the division every gets applied to is nonzero. If you can do that, you may as well do an automatic translation to a version with a /'' that has formal preconditions.

#### Mario Carneiro (Jul 06 2020 at 14:46):

If this quantifier bound condition were all there were to it, it would not be difficult to write a program to analyze the statement and determine if the condition is satisfied (or at least, produce a bunch of proof obligations that imply that the statement is okay)

#### Mario Carneiro (Jul 06 2020 at 14:46):

yes, just like that

#### Mario Carneiro (Jul 06 2020 at 14:47):

It gets harder when you have definitions that legitimately use division by zero, like field

#### Mario Carneiro (Jul 06 2020 at 14:47):

here you have to track definedness conditions on the use of the new definition that imply that they are safe and propagate them (so other functions also become partial)

#### Mario Carneiro (Jul 06 2020 at 14:48):

If you can do that, you may as well do an automatic translation to a version with a /'' that has formal preconditions.

I'm not sure what this translation would be though

#### Johan Commelin (Jul 06 2020 at 14:48):

Maybe we could use an attribute to flag such definitions?

#### Mario Carneiro (Jul 06 2020 at 14:50):

It basically boils down to a definition that doesn't mean the same as what the mathematician thinks they mean

#### Mario Carneiro (Jul 06 2020 at 14:51):

But I think we have bigger fish to fry in this arena, for example 0 < 0.1 being false

#### Jeremy Avigad (Jul 06 2020 at 14:51):

Exactly. It would be nice to have automation that does it. It is easy to do in simple cases. When I first proved the prime number theorem in Isabelle many years ago, it said "pi n * log n / n --> 1". In the definition of the limit of a sequence, n could be 0. It is pretty obvious that this doesn't break anything; for example, you can substitute "n+1" for "n" and the problem goes away. But I think it is reasonable for a mathematician to complain that an entire analysis library is built on top of division, with no sort of guarantee that it is being used correctly.

#### Jeremy Avigad (Jul 06 2020 at 14:53):

You think / type faster than me. The "Exactly" referred to the statement that it would be nice if we could check all the implicit side conditions.

#### Gabriel Ebner (Jul 06 2020 at 14:53):

0 < 0.1 is false??? Is that because 0.1 is a natural number?

yes

#### Johan Commelin (Jul 06 2020 at 14:54):

Of course it is...

#### Johan Commelin (Jul 06 2020 at 14:54):

If it quacks like a duck...

#### Mario Carneiro (Jul 06 2020 at 14:54):

I think you need to look at the problem modularly, where you say "does log match what I think natural log is?" If you can do that for all the definitions, then you will have a good understanding of the visible theorem statement, and all you have to worry about is the explicit division in PNT

#### Mario Carneiro (Jul 06 2020 at 14:55):

That is, for each formal notion you work out what its mathematical meaning is, without presupposing that it is exactly the same as the math notion

#### Mario Carneiro (Jul 06 2020 at 14:55):

I often have to do this anyway if the formal statement uses some unfamiliar terminology

#### Mario Carneiro (Jul 06 2020 at 14:56):

like I would probably look up --> in that isabelle statement

#### Mario Carneiro (Jul 06 2020 at 14:57):

I'm sure it means limit, but is it a limit over natural numbers? Real numbers? How does it handle partiality? These questions must be answered by looking at the formal definition

#### Mario Carneiro (Jul 06 2020 at 14:59):

I don't think an automated tool can solve this problem because it is fundamentally about the difference between a formal object and an informal object (the meaning in the mathematician's head)

#### Kevin Buzzard (Jul 06 2020 at 16:52):

I will repeat the offer I occasionally make -- if there is anyone out there who thinks they have something which will appeal to mathematics undergraduates who perhaps don't know anything about Lean (these are usually the people I'm thinking about when I write) or perhaps to a more general audience (e.g. people who read hacker news or r/math) then they should feel free to get in touch and propose writing a guest post. So far Chris Hughes is the only person who did this. Ideally the post will have some relation to mathematics, and will be more accurate than the kind of poorly researched nonsense I churn out.

#### Jasmin Blanchette (Jul 06 2020 at 18:48):

Even more accurate than that? You're setting the bar too high.

#### Gabriel Ebner (Jul 06 2020 at 19:38):

Mario Carneiro said:

But I think we have bigger fish to fry in this arena, for example 0 < 0.1 being false

I'm in the mood for fish bbq: lean#381

#### Floris van Doorn (Jul 06 2020 at 19:41):

@Gabriel Ebner I don't think we got to a consensus whether this change is desirable.

#### Gabriel Ebner (Jul 06 2020 at 19:42):

To be clear, this is more of an RFC. I'm also not sure if it's a good idea, particularly given how unlikely it would be to have this in Lean 4.

#### Jasmin Blanchette (Jul 06 2020 at 20:09):

I propose a truce between the "it's obvious from the lemma statement whether division by 0 can arise" camp and the "it's subtle and mathematicians have reasons to worry" camp. Since the proof of the pudding is in the eating, one should just have a division operator that carries a proof in addition to the current one and, for those statements where we care/worry about this, prove the lemma with that operator, reusing the lemma proved using the Lean division. That proof should be easy/trivial in most cases, notably those that have a guard. That's what I'd do if I were to base a math textbook on a Lean formalization.

#### Kevin Buzzard (Jul 06 2020 at 20:13):

It would certainly make some mathematicians happy

#### Gabriel Ebner (Jul 06 2020 at 20:34):

I'm always surprised that $x/0$ is such a contentious topic. There is one good and canonical choice, namely the one which makes $1/\cdot$ a pseudo-inverse. Extending structures and operations to have nicer properties is so basic it borders on being invisible. Who would object to prove a property of integers by embedding them into the real numbers, even though it extends the division operation? How is it any different to embed fields into simple meadows? Meanwhile there are multiple reasonable ways to define $0^0$, or what about $\log(-1)$?

#### Chris Hughes (Jul 06 2020 at 21:01):

Found the definition

#### Gabriel Ebner (Jul 06 2020 at 21:04):

Meadow are like field if you replace the axioms for division by being a pseudo-inverse ($(x/y)y = x$ for all $x$ and $y$). Then they are a variety, in particular the smallest variety containing the fields. (Every meadow is a direct product of fields.)

#### Gabriel Ebner (Jul 06 2020 at 21:07):

Funnily enough, I first heard of meadows before I got involved with proof assistants. But now after I am looking again at the paper that introduced them, I have to realize that they were motivated by formalization.

#### Kevin Buzzard (Jul 06 2020 at 21:16):

The whole 1/0 topic is silly and the reason I wrote the blog post was precisely because mathematicians were asking about it on Twitter and I thought I should at least try and put down some coherent thoughts into one place so that I can refer people to it later. But now I'm getting people saying to me that the systems should adapt and make it work the way mathematicians are used to, and just do the type theory way behind the scenes

#### Kyle Miller (Jul 06 2020 at 21:17):

The axiom reminds me a lot of von Neumann regular rings, where for every $x$ there is an $a$ such that $x=xax$. It's not just a von Neumann regular ring, though, since a meadow has an involutive map $x \mapsto x^{-1}$ that gives the $a$.

#### Mario Carneiro (Jul 06 2020 at 21:19):

It seems like a classic bikeshedding problem. Everyone understands the question so you get an outsized number of complaints/suggestions

#### Kyle Miller (Jul 06 2020 at 21:21):

(Though it looks like commutative von Neumann regular rings have such an involution, so I guess I'm not sure whether meadows are any different from commutative von Neumann regular rings. I like the name, though.)

#### Mario Carneiro (Jul 06 2020 at 21:22):

(By the way, if every Xena post generates this much discussion, one Zulip topic may not be enough)

#### Kevin Buzzard (Jul 06 2020 at 21:55):

This one is now trending on Hacker news so I'm getting 500 views an hour.

#### Kevin Buzzard (Jul 06 2020 at 21:55):

And it's about such a ridiculous subject!

#### Kyle Miller (Jul 06 2020 at 22:03):

(Here's a fun fact to justify the color of Lean's bikeshed. The class of elementary recursive functions $\mathbb{N}\to\mathbb{N}$ can be given as expressions involving only the variable, nat.add, nat.sub, nat.div, and nat.pow as Lean defines them.)

#### Jason Rute (Jul 07 2020 at 00:52):

That is a good point about bike shedding. I’ll try to be more careful in the future.

#### Kyle Miller (Jul 08 2020 at 01:33):

I was just experimenting with a way to hide domain hypotheses inside equations. I'm sure others have tried something like this before.

def safe_minus (x : ℕ) (y : ℕ) {h : x ≥ y} : ℕ := x - y

reserve infixl  -! :65

notation x  -!  y := @safe_minus x y (by linarith)

example (x y : ℕ) : x + y -! y = x :=   -- Lean can figure out this is OK
begin
dunfold safe_minus, simp,
end

example (x y : ℕ) {h : x ≥ y} : x -! y + y = x :=   -- if you remove the h hypothesis, Lean will complain
begin
end


#### Johan Commelin (Jul 08 2020 at 04:44):

Yup, it's really cool when it works, but when it breaks it's a pain (at least in lean).
I do think there is potential for something like this. However, I have don't have a good idea how to treat -! when linarith fails. Is the fallback scenario simply that the user must write

have foobar : y ≤ x := some proof,
rw nat.safe_sub_add_cancel, -- now linarith can figure it out


#### Jasmin Blanchette (Jul 21 2020 at 06:04):

Johannes Hoelzl, a very experienced formaliser, told me that in his opinion porting mathlib from Lean 3 to Lean 4 whilst simultaneously refactoring it would be a bad idea.

I fully agree with Johannes. A basic principle of programming is to start with a program that works (e.g. int main() { return 0; }) and do the smallest change possible so that the program still works. And indeed, that's pretty much what Kevin suggests when he points out that it's good to have a syntactically correct proof at (almost) all times. Porting is a very big step, but one should aim at keeping it as small as possible. Refactoring can be done in $n$ iterations afterwards. Doing both together, in the best of cased, might save some work; but it makes the worst case (the whole thing going off tracks) much more likely.

#### Kevin Buzzard (Jul 24 2020 at 14:25):

I might split that post into two, I'm not sure. I think the link between Gowers' two kinds of mathematician and Prop v Type is interesting but I also think it's interesting that the mathlib commiters are a bunch of random people from different departments and ranging from undergraduates to professors

#### Kevin Buzzard (Jul 24 2020 at 14:26):

I was just knocking something up quickly so that the quanta guy had something to read

#### Kevin Buzzard (Jul 24 2020 at 14:27):

(I was interviewed by someone from Quanta yesterday, who will be writing a piece on computer proof systems in a couple of weeks). But I really rushed that post

#### Bryan Gin-ge Chen (Jul 25 2020 at 02:05):

I just realized I'm the only contributor with a net negative number of lines contributed to mathlib.

#### Scott Morrison (Jul 25 2020 at 02:09):

We need some appropriate efficiency measure.

#### Reid Barton (Jul 25 2020 at 02:10):

IMO the real metric should be something like lines of comments minus lines of code

#### Bryan Gin-ge Chen (Jul 25 2020 at 02:15):

Each tactic should have a running total of the number of lines of proof that were saved through its use.

#### Johan Commelin (Sep 19 2020 at 17:30):

https://xenaproject.wordpress.com/2020/09/19/thoughts-on-the-pythagorean-theorem/

And then there is the proof, which originally is either due to Pythagoras or not depending on who you believe.

That's LEM, right there...

#### Marc Huisinga (Dec 05 2020 at 22:20):

https://xenaproject.wordpress.com/2020/12/05/liquid-tensor-experiment/

#### Marc Huisinga (Dec 05 2020 at 22:23):

This is a guest post, written by Peter Scholze, explaining a liquid real vector space mathematical formalisation challenge.

#### Adam Topaz (Dec 05 2020 at 22:40):

What's the appropriate emoji for "solid"? :black_large_square: ?

#### Riccardo Brasca (Dec 05 2020 at 22:46):

Is @Kevin Buzzard ready to coordinate this ? :innocent:

#### Marc Huisinga (Dec 05 2020 at 22:55):

i find section 6 to be especially interesting, which provides context for the motivation of the challenge

#### Patrick Massot (Dec 05 2020 at 22:56):

Yes, this Section 6 comes a bit late, maybe Kevin should warn readers who fear the pure math part they can skip to that section.

#### Patrick Massot (Dec 05 2020 at 22:57):

Although people should make sure not to miss Example 2.3 if they think they understand decimal expansions of real numbers.

#### Jesse Michael Han (Dec 05 2020 at 23:06):

secretly, in high school we learn to think of the interval as a quotient of a profinite set.

:thinking:

#### Bryan Gin-ge Chen (Dec 05 2020 at 23:34):

I'm guessing the recent #5147 was motivated by this (or condensed math in general)? Is there a roadmap or a list of some other milestones for this project?

#### Kevin Buzzard (Dec 06 2020 at 00:13):

Good question! I guess I have been thinking about proving some basic condensed sets stuff, but at some point I'm going to have to understand more of the content of the post. We had a study group on the condensed stuff at Imperial and I think several others on this chat have done as well.

#### David Michael Roberts (Dec 06 2020 at 00:14):

I think getting small sheaves, rather than all sheaves is a good goal regardless of this challenge. I vaguely recall it being mentioned before, but no idea where.

#### Kevin Buzzard (Dec 06 2020 at 00:57):

Patrick Massot said:

Yes, this Section 6 comes a bit late, maybe Kevin should warn readers who fear the pure math part they can skip to that section.

I added a sentence to my introduction.

#### Kevin Buzzard (Dec 06 2020 at 01:09):

David Michael Roberts said:

I think getting small sheaves, rather than all sheaves is a good goal regardless of this challenge. I vaguely recall it being mentioned before, but no idea where.

There is a big design decision to be made here. Do we just consider profinite sets in Type and sheaves on these sets, which will I guess live in Type 1, or do we do all the cardinality hoop-jumping to prove that it all descends nicely? Scholze outlines the details of how to avoid universe-bumping in lecture 1 of condensed.pdf (compare for example Definition 1.2 of a condensed set, and then remarks 1.3 and 1.4, where a modified "correct" definition is made).

But there is a counterpoint to David's point here. In R. Hamming's The unreasonable effectiveness of mathematics he emphasizes (in a big box on page 86!) The Postulates of Mathematics Were Not on the Stone Tablets that Moses Brought Down from Mt. Sinai. He is arguing that fixating on one particular set of axioms (like ZFC) might hinder rather than help mathematics, and "we should be prepared to change postulates when the need becomes apparent". I was talking to Reid about whether we should worry about all these cardinality bounds and he observed that there was a saying in computer science "Build one to throw away". Thus one approach could be just to ignore these things for now, and worry about them later. Note that Grothendieck took this approach in SGA4 -- he assumed the existence of universes so he could push on with his study of topoi, and then other people did the necessary contortions afterwards to force the theory of etale cohomology and hence the proof of the Weil conjectures back into ZFC.

#### David Michael Roberts (Dec 06 2020 at 01:25):

Heh, let it be known that it is a theorem that ZFC is overkill for étale cohomology.

#### David Michael Roberts (Dec 06 2020 at 01:26):

I suspect that if one is reasonably careful no universe bumping is needed at all, even temporarily. But this is, as you say, a design decision.

#### David Michael Roberts (Dec 06 2020 at 01:55):

We will then define the category of condensed sets as the (large) colimit of the category of $\kappa$-condensed sets along the filtered poset of all uncountable strong limit cardinals $\kappa$ (from Condensed.pdf)

well, for a start, this is much better than working with a general filtered poset [sic], it's a well-ordered class, hence linearly ordered. So one can just (!) take the union with no extra identifications of objects or morphisms, as the inclusions are fully faithful. Objects of the category of condensed sets are pairs consisting of a strong limit cardinal $\kappa$ (the uncountability is moot) and an appropriate sheaf. A morphism $(\kappa,F) \to (\lambda,G)$ consists of a map of sheaves where we have extend the smaller of $F$ and $G$ to the site of profinite sets of size $\leq\mathrm{max}\{\kappa,\lambda\}$.

In particular, this is not just a universe-bumping issue, since even allowing ourselves universes, this is not the same thing as sheaves on the large site of all profinite sets. The proposal

Do we just consider profinite sets in Type and sheaves on these sets, which will I guess live in Type 1

is the pyknotic approach.

#### David Michael Roberts (Dec 06 2020 at 02:07):

And, now that I think about it, I'm not sure that strong limit cardinals need to be singled out here at all as far as constructing the category of condensed sets goes. The only thing that is needed is that every cardinal $\mu$ is has a strong limit cardinal $\kappa$ above it, so that every sheaf on any small category of profinite sets (bounded above in size by $\mu$), extends to a sheaf on a category of profinite sets of size up to but below $\kappa$. This should hopefully be enough to access the nice properties that the $\kappa$ s afford.

This means the definition of a condensed set is even easier: it consists of a pair $(\mu,F)$, where $\mu$ is an arbitrary cardinal and $F$ is a sheaf on the site of profinite sets smaller than $\mu$.

Proving any particular topological space/abelian group/vector space is a condensed set/abelian group/vector space would then be a matter of picking an appropriate $\mu$, for instance something a few powersets above the size of the space/abelian group/vector space. Just enough to get a cover from a profinite set to the space etc. Once one has $\mu$, then knowing continuous maps to a space form a sheaf should do.

#### David Michael Roberts (Dec 06 2020 at 02:10):

This seems amenable to an abstract framework, at least as a definition. Of course, proving things about this is less easy, but one can only try it and see. The definition of sheaf on (bounded in size) profinite sets is, mercifully, less complicated than for general spaces!

#### Reid Barton (Dec 06 2020 at 02:33):

This is a situation where things easily expressable in set theory don't match up well with things easily expressible in type theory

#### Reid Barton (Dec 06 2020 at 02:34):

Even having a small category of "sets of cardinality $< \kappa$" is not that simple, and it's worse if you want it to have (say) finite limits and colimits

#### Reid Barton (Dec 06 2020 at 02:39):

It almost seems easier to represent just the small sheaves as formal colimits, and then try to compute the correct Hom sets between them somehow.

#### Kenny Lau (Dec 06 2020 at 02:42):

That's why we have universes, I think.

#### David Michael Roberts (Dec 06 2020 at 05:40):

@Reid Barton hmm, you're right. I guess essentially small doesn't quite cut it...

#### David Michael Roberts (Dec 07 2020 at 12:39):

I said:

And, now that I think about it, I'm not sure that strong limit cardinals need to be singled out here at all as far as constructing the category of condensed sets goes. The only thing that is needed is that every cardinal $\mu$ is has a strong limit cardinal $\kappa$ above it, so that every sheaf on any small category of profinite sets (bounded above in size by $\mu$), extends to a sheaf on a category of profinite sets of size up to but below $\kappa$. This should hopefully be enough to access the nice properties that the $\kappa$ s afford.

This means the definition of a condensed set is even easier: it consists of a pair $(\mu,F)$, where $\mu$ is an arbitrary cardinal and $F$ is a sheaf on the site of profinite sets smaller than $\mu$.

OK, so Peter S confirmed my guess over on MathOverflow. The issue is only about proving nice stability properties of each topos (sheaves on the $\kappa$-proétale site) in the large diagram whose colimit is the category of condensed sets.

#### David Michael Roberts (Dec 07 2020 at 12:40):

But since this is not helping with actual formalisation I'll pipe down, now.

#### Marc Huisinga (Jan 09 2021 at 23:16):

The end of summer

So, what’s been happening? Well, the Lean 4 developers told us in mid-June that Lean 4 would be released at “the end of the summer“. And on Monday Lean 4 got released! The corollary is that it’s the end of the summer now, so it must finally be time to talk about the summer projects, and some of the things which happened since then.

#### Bryan Gin-ge Chen (Jan 09 2021 at 23:32):

It's great to hear about some of the projects done in the Discord server. I hope more of the users there will share their work here (and maybe make some PRs to mathlib)!

#### Kevin Buzzard (Jan 09 2021 at 23:44):

The reason I've not written a blog post for months is that I always felt that the next one I should write should be about the summer projects and that would involve trying to figure out some of the things worth mentioning, which took a while today. I'm half way through the next post now, my thoughts on LT2021.

Some kids are really not into the Zulip. These are people who use Discord under a pseudonym and aren't scared to ask stupid questions there. They have this perception that Zulip is where the experts hang out so it's not really for them yet. On the other hand we have a healthy culture of people asking questions on the discord now and other students answering, as well as a healthy dose of people working on harder stuff like category theory (Bhavik is a regular there, he has become our resident category theory expert, which is wonderful).

#### Kevin Buzzard (Jan 09 2021 at 23:50):

A bunch of recent graph theory stuff (some of which has been PR'ed) was created in live streams on the Discord with people like Alena coding and people like Bhavik and Shing watching.

#### Bryan Gin-ge Chen (Jan 09 2021 at 23:52):

I'm glad there are alternative spaces for students who might feel more comfortable with a different crowd. But I do hope at least some of the fun things they're doing make it to the rest of us!

#### Kevin Buzzard (Jan 09 2021 at 23:57):

The goofy stuff with the widgets seems to be a discord thing, which is a shame, because widgets are really fun! Angela Li (who disappears during term time and appears in the vacation) has been looking at Simon Tatham's puzzle games. I know these games very well. In 2017 before I got into Lean the Android app of these puzzle games was the only game I had installed on my phone, and before I was Lean-competent I was offering MSc projects to prove that various of these games were PSPACE-complete or whatever.

#### Bhavik Mehta (Jan 10 2021 at 00:24):

Bryan Gin-ge Chen said:

I'm glad there are alternative spaces for students who might feel more comfortable with a different crowd. But I do hope at least some of the fun things they're doing make it to the rest of us!

We try to encourage people to ask questions and post here too!

#### EricGT (Jan 10 2021 at 10:13):

Kevin Buzzard said:

These are people who use Discord under a pseudonym and aren't scared to ask stupid questions there.

Perhaps they might come here but with a fantasy name. Using Fantasy Name Generator at the top click Real Names and then pick a specialization. If they do this they should stick with one name and not use a new name each time.

One downside that I find with Discord is that searching for something is not easy. While I have not used Zulip much I do use Discourse daily and find that searching for info with in Discourse is much more effective.

#### Patrick Massot (Jan 10 2021 at 10:24):

EricGT said:

Perhaps they might come here but with a fantasy name. Using Fantasy Name Generator at the top click Real Names and then pick a specialization. If they do this they should stick with one name and not use a new name each time.

We strongly discourage this. Real names are simply much much more convenient. Even people GitHub pseudonyms are annoying.

#### Kevin Buzzard (Jan 10 2021 at 10:36):

Whenever someone on the Discord suggests asking on Zulip I always tell them to use their real name. Right now it's like mathoverflow with most people doing this but not all, but I definitely agree with Patrick that real names are better here

#### EricGT (Jan 10 2021 at 11:23):

Patrick Massot said:

EricGT said:

Perhaps they might come here but with a fantasy name. Using Fantasy Name Generator at the top click Real Names and then pick a specialization. If they do this they should stick with one name and not use a new name each time.

We strongly discourage this. Real names are simply much much more convenient. Even people GitHub pseudonyms are annoying.

I would agree that using false names here should be discouraged. However the use of separate sites doing the same IMHO feels like the start of a division in the community.

In other words, is there a way to get the users that are afraid to ask questions here to ask them here? I know this is not a problem unique to this site, idea, etc.

Personally I would like to see such questions and replies being a beginner myself trying to learn LEAN starting with LEAN 4.

#### Mario Carneiro (Jan 10 2021 at 12:28):

I would guess that whatever it is that makes people afraid to ask questions here has little to do with usage of real names. If we're talking unconfident undergraduates, generally it isn't a problem to use real names but they might feel they are "imposing" by asking questions. The folks who deliberately avoid using their real name either do it by habit from other parts of the internet or have a strong information privacy mentality

#### Mario Carneiro (Jan 10 2021 at 12:29):

The latter type are just as likely to balk at the need to sign up for an account to get into zulip in the first place

#### Marc Huisinga (Apr 18 2021 at 18:59):

Induction, and inductive types

Induction on equality

Last updated: May 06 2021 at 20:13 UTC