XenaProject blog posts

Stream: general

[Marc Huisinga]

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.
link to the blog: https://xenaproject.wordpress.com/

[Marc Huisinga]

newest post: Equality, specifications, and implementations

[Bryan Gin-ge Chen]

Thank you!

[Sebastian Ullrich]

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]

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]

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]

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

[Kevin Buzzard]

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]

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]

(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]

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]

no, we could certainly do that

[Mario Carneiro]

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]

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

[Mario Carneiro]

@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]

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]

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]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

how so?

[Mario Carneiro]

no more than currently

[Patrick Massot]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Patrick Massot]

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

[Mario Carneiro]

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]

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

[Patrick Massot]

Nice

[Mario Carneiro]

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]

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]

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]

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

[Mario Carneiro]

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]

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]

maybe a special variant of import that triggers this behavior?

[Mario Carneiro]

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

[Kevin Kappelmann]

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

[Sebastian Ullrich]

Yes, the default import would most likely be unchanged

[Mario Carneiro]

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]

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]

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]

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

[Sebastian Ullrich]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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

[Sebastian Ullrich]

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]

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]

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]

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]

You can't subtract them though :-)

[Jason Rute]

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]

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]

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

[Jeremy Avigad]

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]

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]

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]

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]

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]

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]

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]

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]

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

[Jeremy Avigad]

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

[Mario Carneiro]

by looking at them

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

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]

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

[Jeremy Avigad]

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]

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

[Mario Carneiro]

that is enough to eliminate a large fraction of spurious uses

[Mario Carneiro]

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]

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]

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]

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]

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]

yes, just like that

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

Maybe we could use an attribute to flag such definitions?

[Mario Carneiro]

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

[Mario Carneiro]

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

[Jeremy Avigad]

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]

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]

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

[Mario Carneiro]

yes

[Johan Commelin]

Of course it is...

[Johan Commelin]

If it quacks like a duck...

[Mario Carneiro]

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]

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]

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

[Mario Carneiro]

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

[Mario Carneiro]

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]

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]

Given that this topic is about my blog posts, I may as well give you some stats. In the same week that Rob announced that there had been as much mathlib activity in 2020 as there had been in the whole of 2019 (I forget how he measured it, perhaps commits or lines of code), I made it to 42000 views on the blog, beating the 41000 views I got in all of 2019. I'll make it to 50K within the next few days I think. The general pattern seems to be that if I post something which either hacker news or reddit r/math or twitter likes, then I get 1000+ views per day for the next couple of days, e.g. the "mathematics in type theory" post from two weeks ago got 1000+ views for three days from Twitter and then 2000+ views for two days, when hacker news got excited about it. These sorts of posts seem to be the most popular ones -- where a general computer scientist or mathematician who doesn't know anything about Lean can at least read and understand the post and think "hmm, I learnt something about how doing mathematics in type theory / Lean works from reading this".

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]

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

[Gabriel Ebner]

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]

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

[Gabriel Ebner]

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.

[Floris van Doorn]

See discussion below this post for the discussion about this topic: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/37/near/202221745

[Jasmin Blanchette]

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]

It would certainly make some mathematicians happy

[Gabriel Ebner]

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]

What's a simple meadow?

[Chris Hughes]

Found the definition

[Gabriel Ebner]

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]

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]

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]

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]

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

[Kyle Miller]

(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]

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

[Kevin Buzzard]

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

[Kevin Buzzard]

And it's about such a ridiculous subject!

[Kyle Miller]

(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]

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

[Kyle Miller]

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
  exact nat.sub_add_cancel h,
end

[Johan Commelin]

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

[Johan Commelin]

LFTCM post mortem: https://xenaproject.wordpress.com/2020/07/17/lean-for-the-curious-mathematician-2020/

[Jasmin Blanchette]

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.

[Johan Commelin]

This was a fun read: https://xenaproject.wordpress.com/2020/07/23/two-types-of-universe-for-two-types-of-mathematician/

[Kevin Buzzard]

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]

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

[Kevin Buzzard]

(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]

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

[Scott Morrison]

We need some appropriate efficiency measure.

[Reid Barton]

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

[Bryan Gin-ge Chen]

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

[Johan Commelin]

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]

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

[Marc Huisinga]

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

[Adam Topaz]

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

[Riccardo Brasca]

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

[Marc Huisinga]

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

[Patrick Massot]

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]

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

[Jesse Michael Han]

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

:thinking:

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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

[David Michael Roberts]

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]

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]

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]

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]

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]

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]

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]

That's why we have universes, I think.

[David Michael Roberts]

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

[David Michael Roberts]

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]

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

[Marc Huisinga]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

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]

Induction, and inductive types

Induction on equality

[Marc Huisinga]

Half a year of the Liquid Tensor Experiment: Amazing developments (guest post by Peter Scholze)

[Johan Commelin]

https://news.ycombinator.com/item?id=27405693

[Adam Topaz]

How long before it hits the front page of HN?

[Kevin Buzzard]

I think it's a bit mathsy for hacker news

[Eric Rodriguez]

also on Reddit! https://www.reddit.com/r/math/comments/nsyebd/half_a_year_of_the_liquid_tensor_experiment/

[Marc Huisinga]

Kevin Buzzard said:

I think it's a bit mathsy for hacker news

I think with the right title it might be popular on HN, but the current one is certainly not sensationalist enough :)

[Marc Huisinga]

Teaching formalisation to mathematics undergraduates

[Kevin Buzzard]

@Zhangir Azerbayev 's post about Lean Chat on my blog is getting some traction on Hacker news if people want to vote it up...