## Stream: general

### Topic: Lean talk for mathematicians

#### Johan Commelin (Sep 03 2018 at 09:20):

I've been asked to talk about Lean in our colloquium. Still freaking out... what should I put in such a talk? How do I manage expectations, so that they become realistic (instead of "Blah, unusable crap" or "They'll use AI to prove millenium problems. They're stealing our jobs.")

#### Johan Commelin (Sep 03 2018 at 09:20):

Over lunch I only ever hear these extremes.

#### Johan Commelin (Sep 03 2018 at 09:20):

Any tips or tricks are very welcome.

#### Patrick Massot (Sep 03 2018 at 09:25):

When will you give this talk?

#### Patrick Massot (Sep 03 2018 at 09:25):

I will also probably try that

#### Patrick Massot (Sep 03 2018 at 09:26):

I hope the perfectoid project will be completed before

#### Johan Commelin (Sep 03 2018 at 09:26):

I can still choose the date, but it could be as early as mid-October.

#### Johan Commelin (Sep 03 2018 at 09:27):

This is another reason why we should have easy installers and/or code browsers...

#### Johan Commelin (Sep 03 2018 at 09:27):

In some sense freshmen students will have a lot more patience and persistence then tenured staff. If it doesn't work out of the box, we've lost them for a couple of years again.

#### Johan Commelin (Sep 03 2018 at 09:28):

Still, the fact that I was asked to give a talk shows that there is some interest among them. And I want to capitalize on that.

#### Patrick Massot (Sep 03 2018 at 09:33):

If you want to attract mathematicians, I think the best you can do is to work on perfectoid spaces. Look at how we hooked people. If I understand correctly, Bryan, Soham and you came here because you heard about either schemes or perfectoid spaces in Lean. It would be interesting to compare with what happened in Coq. @Assia Mahboubi how many mathematicians or advanced maths students showed up in Coq forums or mailing lists when the odd order theorem proof was announced?

#### Patrick Massot (Sep 03 2018 at 09:34):

If we manage to complete the definition, you'll be able to show nice dependency graphs displaying how much maths goes into this definition.

#### Johan Commelin (Sep 03 2018 at 09:39):

Right! We want dependency graphs and such! We want boatloads of visualisation tools.

#### Johan Commelin (Sep 03 2018 at 09:39):

Scott had really cool visualisations! We need more of those (-;

#### Johan Commelin (Sep 03 2018 at 09:39):

Yes... but not enough

#### Johan Commelin (Sep 03 2018 at 09:40):

The code browser is also a form of visualisation (in my eyes)

#### Patrick Massot (Sep 03 2018 at 09:40):

during your talk you can use VScode

#### Johan Commelin (Sep 03 2018 at 09:41):

Sure, I was planning to do that.

#### Kevin Buzzard (Sep 03 2018 at 09:47):

I wanted to concentrate on preparing my course in September but lots of things are happening. I just need to work harder. I don't think mid-October is an unreasonable target for perfectoid spaces. Sometimes when I look at the definition I think "this is easy, there's nothing left apart from a bunch of standard stuff which should be easy", and at other times I remember that I watched Mario take three hours to prove the math-trivial fact that the two standard definitions of Noetherian module are equivalent and then the realisation hits me. Another concern I have is that people are appearing out of the woodwork, either here or in my inbox, saying "can I help?" and currently I just seem to be saying "Sure! Just join in!". I meant to spend some time yesterday getting on top of the perfectoid project (like I did with the scheme project in Paris -- getting it to compile again!) but all I managed to do was remove some of the errors we get when compiling.

#### Kevin Buzzard (Sep 03 2018 at 09:48):

Most of my summer students have finished now though, so I will hopefully be far more active in Sept in the project than I have been in July and Aug (I've spent a lot of time talking to undergraduates about UG level maths in Lean recently).

#### Patrick Massot (Sep 03 2018 at 09:48):

Right now I'm working on getting the project to compile

#### Patrick Massot (Sep 03 2018 at 09:48):

But it's lunch time

#### Patrick Massot (Sep 03 2018 at 09:49):

Can you give me two hours, and then I'll hopefully PR some progress?

#### Johan Commelin (Sep 03 2018 at 09:51):

Kevin, I think pointing people to Zulip is a very good idea.

#### Johan Commelin (Sep 03 2018 at 09:52):

We'll usually be able to get people started.

#### Johan Commelin (Sep 03 2018 at 09:52):

Also, like I said, I haven't fixed a date for my talk yet. So it could also be 3 weeks later.

#### Kevin Buzzard (Sep 03 2018 at 10:00):

It's nice to have deadlines though.

#### Kevin Buzzard (Sep 03 2018 at 10:00):

If there's flexibility, why not ask for November? :-)

#### Johan Commelin (Sep 03 2018 at 10:01):

Because I don't have as many deadlines as you (-;

#### Johan Commelin (Sep 03 2018 at 10:01):

I don't want to pressure you. But I'dd certainly wait till November if that means that the perfectoid project will likely be ready.

#### Kevin Buzzard (Sep 03 2018 at 10:06):

I am being funded to run a Lean course which starts on Oct 1st, with 250 students, and out of the 100 formalised maths questions and solutions which I need to prepare to run this course, I have so far finished 1. On the other hand my kids go back to school on Wednesday and life gets a bit saner after that. I think what I currently need is a clearer view of the route to the finish line. Occasionally I look at the point in Wedhorn's paper that we're up to, and it's the line "let V_pre denote the category of topological spaces endowed with a presheaf of topological rings having some properties" and I always think "I wonder if Scott's library can help me here?". @Scott Morrison I can easily make this category "by hand" -- if I want perfectoid spaces done by mid-Oct should I do so?

#### Kevin Buzzard (Sep 03 2018 at 10:09):

Right now I'm working on getting the project to compile

Compile modulo sorries, of course.

#### Johan Commelin (Sep 03 2018 at 10:14):

Scott is working on sheaves with values in arbitrary types. So I think we can soon have a reasonable clean definition of this category. @Scott Morrison I don't want to put words in your mouth. Did I say that right?

#### Kevin Buzzard (Sep 03 2018 at 10:17):

Right, but the question is whether in practice "soon" means "by January" or "by next week".

#### Kevin Buzzard (Sep 03 2018 at 10:18):

I keep looking at the definition and thinking "he's taking a directed limit to construct the stalk -- I did all that by hand in the schemes repo, I wonder whether I should just sit and wait this time". But actually I guess all I need is a direct limit of rings anyway shrug -- the topology plays no role.

#### Scott Morrison (Sep 03 2018 at 10:27):

@Kevin Buzzard, I think I can have "the category of sheaves of rings on a topological space" in pretty short order.

#### Scott Morrison (Sep 03 2018 at 10:27):

In order to be able to talk about the stalk, we'd need to add least get the definition of tensor product of commutative rings into mathlib.

#### Scott Morrison (Sep 03 2018 at 10:27):

This should be easy now that Kenny has pushed tensor products of modules?

#### Kevin Buzzard (Sep 03 2018 at 10:28):

To get the stalk of the structure sheaf we only need direct limits I guess

#### Scott Morrison (Sep 03 2018 at 10:28):

In order to be able to usefully talk about stalks, we'd need to have filtered colimits of rings.

#### Scott Morrison (Sep 03 2018 at 10:29):

(The difference between direct and filtered is pretty small, I think; filtered should be barely harder.)

#### Scott Morrison (Sep 03 2018 at 10:29):

This is definitely doable, in the sense that I started writing it, and didn't see any obvious obstructions besides me being slow.

#### Johan Commelin (Sep 03 2018 at 10:30):

Please don't say that you are slow... I already reserved that word for my tempo...

#### Scott Morrison (Sep 03 2018 at 10:31):

It would be nice to write direct/filtered colimits in a way that makes it easy to see how to generalise. Reid was talking about eventually writing some machinery (possibly having to involve some tactics, I'm not sure) that would construct limits and filtered colimits just from knowing properties of the forgetful functor.

#### Scott Morrison (Sep 03 2018 at 10:31):

But I don't think we need to wait on that. :-)

#### Scott Morrison (Sep 03 2018 at 10:32):

A general question: where do people think particular categories should go?

#### Scott Morrison (Sep 03 2018 at 10:32):

i.e. should I make a category_theory/examples/ folder, and put Ring and Top etc there?

#### Scott Morrison (Sep 03 2018 at 10:33):

Or do that categories go all spread out through the repository, close to their natural homes?

#### Scott Morrison (Sep 03 2018 at 10:34):

And if they go all spread out, should I just put them in as soon as they are definable, requiring category_theory/ as a dependency, or just have one extra file per theory that imports category_theory and does the assembly work there, and people who need it can import that?

#### Kenny Lau (Sep 03 2018 at 10:42):

while you're busy characterising direct limit... I'm building direct limit :P

#### Soham Chowdhury (Sep 03 2018 at 16:28):

If you want to attract mathematicians, I think the best you can do is to work on perfectoid spaces. Look at how we hooked people. If I understand correctly, Bryan, Soham and you came here because you heard about either schemes or perfectoid spaces in Lean.

This is true; I write a good amount of Haskell and so I've been aware of, e.g. work in Coq/Agda/Idris (and Liquid Haskell) on proving data-structures or algorithms correct, or space/time-complexity bounds, and so on, but was never motivated to jump into that sort of thing.

Before I became aware of the work on formalising mathematics I know/am learning/care about, I had resigned myself to waiting until I understood enough homotopy theory to take a stab at HoTT.

#### Soham Chowdhury (Sep 03 2018 at 16:29):

btw, @Patrick Massot thanks for pointing me the right way, I worked through some of the tutorial today

#### Patrick Massot (Sep 26 2018 at 12:11):

I've been asked to talk about Lean in our colloquium. Still freaking out... what should I put in such a talk? How do I manage expectations, so that they become realistic (instead of "Blah, unusable crap" or "They'll use AI to prove millenium problems. They're stealing our jobs.")

Johan, did you give that talk already? I also took up the challenge. Actually I was asked to give a colloquium about any topic, and I proposed the title "Can mathematicians use proof verification software?". Somewhat surprisingly, this was accepted. We now have a new deadline for the perfectoid project: October 18th...

#### Kevin Buzzard (Sep 26 2018 at 12:33):

or October 17th if you count my colloquium in Sheffield in front of Neil Strickland...

#### Scott Morrison (Sep 26 2018 at 12:39):

Haha, I'm on October 5, for a colloquium at Adelaide. :-)

#### Patrick Massot (Sep 26 2018 at 12:43):

Nice, let's finish it before October 5th! My colloquim will (presumably) be in front of Sébastien and Assia. It sounds a bit ridiculous but the point is exactly to discuss how much is doable by a normal clueless mathematician

#### Patrick Massot (Sep 26 2018 at 12:44):

Of course I'm cheating since I'm currently waiting for Johannes to unlock my completion stuff...

#### Kevin Buzzard (Sep 26 2018 at 12:46):

...and Hilbert Basis is on hold too. Who knows if I will have time to look at this stuff before October. The annual pile of reference letter requests has begun to appear...

#### Patrick Massot (Sep 26 2018 at 12:47):

Reference letters are easy to write those days: "Dr. XXX claims nice result, but I haven't seen a formalized proof, so who knows what he/she is talking about?"

#### Johan Commelin (Sep 26 2018 at 14:23):

Ok, I don't have a date yet. But I think I will be last in row.

#### Sebastien Gouezel (Sep 26 2018 at 16:03):

As a further data point in the question of usability of proof assistants in real-life (well, mathematical real-life), you can have a look at http://www.math.sciences.univ-nantes.fr/~gouezel/articles/morse_lemma.pdf (preliminary version).

Some time ago, I mentioned that I found a gap in a published paper while formalizing it in Isabelle. This gap is now corrected, and the new proof is completely formalized. The above paper explains the corrected proof, for mathematicians, but it also mentions the formalized proof. By the way, it raises interesting questions on the way to write a math papers when you have a formalized proof (when we need a lemma that is related, but not exactly the same, to results already in the literature, should we give the proof or just point the reader to the formalized proof?) We have tried to find some middle ground here, but I guess our way to write papers will have to change. Comments welcome!

#### Patrick Massot (Sep 26 2018 at 18:20):

Amazing! Do you intend to submit this to a traditional math journal? I'd be very interested to see what happens.

#### Sebastien Gouezel (Sep 26 2018 at 18:42):

Yes, probably as a corrigendum to the journal where the initial paper was published (Journal of Functional Analysis, an excellent journal but published by Elsevier, which is a bit of a problem for ethical reasons but traditionally a paper and a corrigendum are in the same journal. We will see)

#### Patrick Massot (Sep 26 2018 at 18:44):

It seems pretty clear to me that "our way to write papers will have to change" when we have formalized proofs. Writing technical details in TeX is pointless of you have a formal proof. You should rather spend the energy on explaining what's going on

#### Reid Barton (Sep 26 2018 at 18:45):

This is very cool!

#### Reid Barton (Sep 26 2018 at 18:46):

Is there something like a "Journal of Formalized Mathematics", but not particular to any one theorem proving system?

#### Mario Carneiro (Sep 26 2018 at 18:48):

CPP is something like that

#### Patrick Massot (Sep 26 2018 at 18:50):

I'm impressed by the Isabelle snippets: it seems Isabelle allows the user to use lambda as a constant real number

#### Johannes Hölzl (Sep 26 2018 at 18:53):

huh where do you see this? I just see the names lambda and delta?

#### Patrick Massot (Sep 26 2018 at 18:54):

hausdorff_distance (f{a..b}) G ≤ 92 * lambda^2 * (C + deltaG(TYPE('a)))

#### Sebastien Gouezel (Sep 26 2018 at 18:54):

lambda as a sequence of letters, yes. But probably not λ, this is reserved for function definitions.

ah...

#### Patrick Massot (Sep 26 2018 at 18:55):

I'll stick to Lean then

#### Patrick Massot (Sep 26 2018 at 18:55):

Reading the introduction doesn't allow me to understand why optimizing the constant is worth the trouble

#### Mario Carneiro (Sep 26 2018 at 18:56):

I think bold lambda gets used somewhere...

#### Johannes Hölzl (Sep 26 2018 at 18:58):

@Reid Barton w.r.t "Journal of Formalized Mathematics" there is also the Journal of Automated Reasoning (https://link.springer.com/journal/10817), the "Journal of Formalized Reasoning" https://jfr.unibo.it/, and the ITP the conference on interactive theorem proving.

#### Patrick Massot (Sep 26 2018 at 18:59):

Sébastien, I think you should explain a bit more how to read Isabelle code. It's not easy to map the traditional statement to Isabelle statement

#### Reid Barton (Sep 26 2018 at 19:02):

Is a $(\lambda, C)$-quasi-isometry the same as a $(\lambda, C)$-quasi-geodesic? Is a geodesic the same as a $(1, 0)$-quasi-geodesic?

#### Sebastien Gouezel (Sep 26 2018 at 19:10):

a (λ,C)-quasi-geodesic is a (λ,C)-quasi-isometry defined on an interval. A geodesic is a (1,0)-quasi-geodesic, yes. All these terms are supposed to be standard in the domain. As for the explanations of Isabelle code, since the math statement is given just before the Isabelle statement, I was hoping that the correspondance would be easy to make for people interested in the formalization, but maybe I am too optimistic. If you have a hard time reading the statement, I should definitely add some details (or maybe this is because you are too used to Lean syntax...)

#### Patrick Massot (Sep 26 2018 at 19:17):

I guess it would be much easier if notation matched. Thinking about the main statement, I guess that 'a = X and f = Q but I don't understand why the notation changes.

#### Reid Barton (Sep 26 2018 at 19:18):

Oh I'm sure that they are standard--but the article is also nearly readable for someone like me who has almost no relevant knowledge beyond the definition of a metric space.

#### Patrick Massot (Sep 26 2018 at 19:19):

I wonder if you should include more background for people who read this paper because of the formalization

#### Askar Safin (Sep 26 2018 at 19:21):

hi. is lean based on pts?

#### Mario Carneiro (Sep 26 2018 at 19:45):

@Askar Safin I don't think it fits into the definition of a PTS; it is dependently typed but most PTSs I have seen are simply typed

#### Sebastien Gouezel (Sep 26 2018 at 19:58):

I guess it would be much easier if notation matched. Thinking about the main statement, I guess that 'a = X and f = Q but I don't understand why the notation changes.

'a is the Isabelle name for a type (in the same way that, in Lean, your X would be called alpha). Q is the quasi-geodesic and f is its parametrization. Thanks for the comments, I will try to make it more self-contained.

#### Patrick Massot (Sep 26 2018 at 20:03):

In Lean, you can actually call a group G if you insist enough. See Johannes recent commits in https://github.com/leanprover-community/mathlib/tree/completions He cleaned a lot of things, but didn't write alpha everywhere :smile:

#### Chris Hughes (Sep 26 2018 at 20:06):

There's even a group called G in master, in group_theory/quotient_group

#### Kenny Lau (Sep 26 2018 at 20:20):

we have reclaimed our land!

#### Sebastien Gouezel (Sep 26 2018 at 20:21):

In Isabelle, as far as I know, it has to be 'a.

#### Patrick Massot (Sep 26 2018 at 20:21):

Sébastien, you should really switch to Lean now that this project is done

#### Patrick Massot (Sep 26 2018 at 20:22):

And then your metric spaces will be X again

#### Sebastien Gouezel (Sep 26 2018 at 20:36):

Of course I should switch to Lean, the future is there. But a rough estimate for me is that proving in Isabelle is probably 20 times faster than in Lean.
Look at these lines:

  also have "... = lambda^2 * (11/2 * C + (3200*exp(-459/50*ln 2)/ln 2 + 83) * delta)"
unfolding Kmult_def K_def L_def alpha_def D_def using ‹delta > 0› ‹lambda ≥ 1› by (simp add: algebra_simps divide_simps power2_eq_square mult_exp_exp)
also have "... ≤ lambda^2 * (11/2 * C + 91 * delta)"
apply (intro mono_intros, simp add: divide_simps, approximation 14)
using ‹delta > 0› by auto


Is there an automatic way in Lean to prove that 3200*exp(-459/50*ln 2)/ln 2 + 83 is bounded by 91?

#### Sebastien Gouezel (Sep 26 2018 at 20:40):

(This is a rhetorical question, I know that expjust made it into Lean). And the true value is 90.959, so the estimates can not be too rough...

#### Sebastien Gouezel (Sep 26 2018 at 20:46):

More seriously, I would really be interested by the feeling of someone who is proficient both in Lean and in Isabelle, for instance Johannes, as to how quickly he proves things in both systems.

#### Chris Hughes (Sep 26 2018 at 20:50):

What are the drawbacks to Lean? Is it just that the libraries aren't big enough yet?

#### Johannes Hölzl (Sep 26 2018 at 20:52):

Hm, I still miss some things from Isabelle, like most simp procs are just not available. But this is something I'm sure we get with Lean 4 (or we implement it ourselves). A prover for simple logical statements like auto is missing. Type (class) inference in Isabelle is more predictable.
But my general feeling is that I'm now faster in Lean than in Isabelle. Lean also feels more responsive.

#### David Michael Roberts (Sep 27 2018 at 08:23):

@Scott Morrison

Oh, nice! I have a student from Comp Sci who was interested in working on something over summer and I casually mentioned Lean. If he's free around the time you're here I could get him to come by

#### Scott Morrison (Oct 02 2018 at 09:42):

Hi all .... I need help selecting an example. I want to actually prove something during my talk. I just recorded myself proving there are infinitely many primes, and even going too fast it took 20+ minutes.

#### Scott Morrison (Oct 02 2018 at 09:42):

I have at most 10... What should I do?

#### Patrick Massot (Oct 02 2018 at 09:42):

by obviously!

#### Scott Morrison (Oct 02 2018 at 09:44):

I'll talk a little about automation at the very end. I want something much more basic for this.

#### Patrick Massot (Oct 02 2018 at 09:46):

I'm called for lunch, but I'll tell you more later

#### Johan Commelin (Oct 02 2018 at 09:47):

Hmmm... I'm on the fence about this. If you do something too basic you risk that mathematicians will think this stuff is stupid, and only usable for 1st stuff.

#### Kevin Buzzard (Oct 02 2018 at 09:47):

If you were allowed an import which did the boring bits behind the scenes, then I reckon irrationality of sqrt(2) would fit into 10 minutes, if you formalised it as the assertion that there were no positive nats a and b with a^2=2b^2, or something close to that. But why not go with infinitely many primes? Just hide the tedious work behind an import which you wrote earlier.

#### Scott Morrison (Oct 02 2018 at 09:47):

Hmm, okay, it hadn't occurred to me to cheat.

#### Scott Morrison (Oct 02 2018 at 09:47):

I like that a lot. :-)

#### Kevin Buzzard (Oct 02 2018 at 09:47):

I am absolutely cheating with my 1st year maths example sheets, because they are much too hard otherwise.

#### Kevin Buzzard (Oct 02 2018 at 09:48):

For a 1st year undergrad, $x^2-3x+2=0\iff x=1\lor x=2$ is "trivial by the formula for a quadratic"

#### Scott Morrison (Oct 02 2018 at 09:49):

The other things I was considering was doing something basic with nat (but this requires way too much talking about inductive types for what I'm trying to do), or proving something completely elementary about groups or group homomorphisms (but this is lame and unexciting).

#### Kevin Buzzard (Oct 02 2018 at 09:49):

And they need this on sheet 1, but the proof uses the fact that the reals are an integral domain and blah blah blah. So I prove it in the import file and just offer them that theorem and tell them to rw with it.

#### Kevin Buzzard (Oct 02 2018 at 09:50):

If you want to not cheat, then you could prove something like "A binary relation is an equivalence relation if and only if it is reflexive and Euclidean".

#### Kevin Buzzard (Oct 02 2018 at 09:51):

I would strongly recommend not proving that if a function is surjective then it has a one-sided inverse, because the axiom of choice is not pretty :-)

#### Scott Morrison (Oct 02 2018 at 09:56):

It occurs to me that my recent PR to solve_by_elim lets me cheat outrageously in the proof of infinitude of primes. I can just tag a few lemmas with attributes and have solve_by_elim do large chunks.

#### Scott Morrison (Oct 02 2018 at 09:57):

I'm a little dubious about showing people a proof that only works in a private branch of mathlib. :-)

#### Kevin Buzzard (Oct 02 2018 at 10:23):

I just think that you should tell them that this is actual work in progress and this is what can be done now, and later on it will work in proper mathlib. Or actually just not bore them at all with technical details like this, if time is tight. Who is the actual audience? Does mathlib have something like translation invariance of Lebesgue measure on the reals? What do these people want to see? Existence of complicated things, or proofs of simple things?

#### Scott Morrison (Oct 02 2018 at 10:27):

This is a (maths) colloquium audience at a random Australian university. I really don't know what is worth doing as an example. I definitely want to give some realistic flavour of "writing code", but given everything else that needs to be said in a talk it really can't take more than 10 minutes.

#### Scott Morrison (Oct 02 2018 at 10:28):

I've just written a much shorter proof using a slightly fictional backwards_reasoning, and I'll time it later to see if it's viable.

#### Kevin Buzzard (Oct 02 2018 at 10:54):

Colloquium talk -- I don't think I'd care at all about whether it worked in core mathlib or not. Anyone who wants to try and join in will have 100 simpler things to worry about before they're able to prove that there are infinitely many primes. A lot of them might not get past installing the software.

#### Patrick Massot (Oct 02 2018 at 10:55):

Last week I spend some time showing Lean to a collaborator, using https://github.com/PatrickMassot/lean-scratchpad/blob/master/src/demo.lean that I wrote a while ago for that kind of explanation. It shows basic reasoning, as well as crushing things using automation, using axiom of choice, a calc proof, and a proof by induction. Nothing exciting but he was really surprised by how natural it felt

#### Patrick Massot (Oct 02 2018 at 10:56):

I think it's important to show that we have no trouble with axiom of choice, since many mathematicians heard false rumors of proof assistant being limited to constructive math

#### Patrick Massot (Oct 02 2018 at 10:56):

I should really PR that into mathlib

#### Scott Morrison (Oct 02 2018 at 11:06):

Thanks, Patrick, that's a nice demo file.

#### Patrick Massot (Oct 02 2018 at 11:06):

It makes me think: is anyone working on https://mathoverflow.net/a/311159/58618?

#### Kevin Buzzard (Oct 02 2018 at 11:27):

" If anyone wants to send me Lean code then I would be grateful." says Neil. He's the guy who invited me to speak in Sheffield in 2 weeks' time.

#### Scott Morrison (Oct 02 2018 at 11:28):

Neil was at the Dagstuhl meeting

#### Scott Morrison (Oct 02 2018 at 11:28):

He gave a talk about his library of "semi-formalised" mathematics.

#### Scott Morrison (Oct 02 2018 at 11:28):

and had someone from every theorem prover sit down and show him the basics.

#### Patrick Massot (Oct 02 2018 at 11:39):

What about using the kbb repository to collaborate on Leaning this wishlist?

#### Johan Commelin (Oct 02 2018 at 12:07):

I think it would be really good if we could answer Neil's question quickly on MO.

#### Johan Commelin (Oct 02 2018 at 12:08):

It would make a good impression if we can actually show the community: look we took this issue seriously, and Lean became a bit more usable.

#### Johan Commelin (Oct 02 2018 at 12:09):

With all the other answers, I think it is also a good idea that we don't forget about them, but mark them as done when we get there.

#### Johan Commelin (Oct 02 2018 at 12:09):

People will be scrolling through that list about 4 years from now, and they should see that everything got done.

#### Johan Commelin (Oct 02 2018 at 12:23):

We could reuse kbb, but we could also setup a new project. Alternatively, we create a tutorial branch on the community fork.

#### Johan Commelin (Oct 02 2018 at 12:24):

We could put Neil's ideas into the tutorial branch. And also Patrick's demo, translating it to English and annotating it with some comments.

#### Johan Commelin (Oct 02 2018 at 12:25):

I really like your demo file, @Patrick Massot. Thanks!

#### Reid Barton (Oct 02 2018 at 12:31):

I like the idea of putting the tutorial in mathlib itself, as an ordinary .lean file--then we will have to keep it working with current mathlib.

Agreed

#### Johan Commelin (Oct 02 2018 at 12:36):

bitrot is too easy

#### Johan Commelin (Oct 02 2018 at 12:36):

@Johannes Hölzl @Mario Carneiro What do you think of a tutorial/ folder in mathlib?

#### Johan Commelin (Oct 02 2018 at 12:36):

Or possible docs/tutorial?

#### Patrick Massot (Oct 02 2018 at 12:43):

I like the docs/tutorial idea, although it may lead to disappointment for people expecting a fully fledged tutorial. I also PR'ed my choice tactic.

#### Johan Commelin (Oct 02 2018 at 12:53):

Ok, how about docs/demo/

#### Johan Commelin (Oct 02 2018 at 12:54):

And then a bunch of files called demo_1.lean etc...

#### Kevin Buzzard (Oct 02 2018 at 12:55):

+1 from me. Three times now people have asked here "how do quotients work in Lean?" and amongst the answers has been me saying "I wrote this random bit of code which is dumped somewhere on github probably in the xena repo -- maybe it helps?"

#### Kevin Buzzard (Oct 02 2018 at 12:56):

I am writing stuff like this http://wwwf.imperial.ac.uk/~buzzard/xena/html/source/ch1_and_or_props/prop_exercises.html by the way. By the end of term there will definitely be a whole lot more of that stuff.

#### Scott Morrison (Oct 02 2018 at 21:55):

I'm certainly in favour of docs/demo/ and docs/tutorials/ (plural tutorials might lessen the blow when people realise it isn't a top-to-bottom tutorial encompassing everything!)

#### Scott Morrison (Oct 02 2018 at 21:56):

I was thinking to record a screen capture of doing the infinitude of primes proof, which may contribute towards answering Neil.

#### Johan Commelin (Oct 05 2018 at 14:29):

Your Presheaf misses an op (-;

#### Johan Commelin (Oct 05 2018 at 14:29):

By the way, I really like the typography of the slides!

#### Johan Commelin (Oct 05 2018 at 14:54):

@Scott Morrison Thanks for sharing this talk! It's a wonderful resource for the rest of us will be giving similar talks in the next few weeks.

#### Bryan Gin-ge Chen (Oct 05 2018 at 14:57):

Fun talk so far! I keep thinking your mouse cursor on the slides is mine though...

#### Patrick Massot (Oct 05 2018 at 20:37):

@Scott Morrison I'd be curious to know whether you had any reactions to your talk. I would have never dared to start explaining Types vs Sets without first showing how it works in the software

#### Scott Morrison (Oct 05 2018 at 21:32):

No one directly complained about the types vs. sets things. I did talk to a quite a few people afterwards (drinks in the department, then drinks at the faculty bar...). From those discussions, I realised the thing I should have been clearer about was the distinction between automatic and interactive theorem proving.

#### Scott Morrison (Oct 05 2018 at 21:33):

It seemed a number of people were aware of the idea of automatic theorem proving, but hadn't realised what you could do interactively.

#### Scott Morrison (Oct 05 2018 at 21:35):

On a side note, I would love to make a fake screen capture sometime, of an interaction with emacs, writing a proof in LaTeX, and occasionally hitting C-:hammer: and having emacs fill in a few sentences for you.

#### Scott Morrison (Oct 05 2018 at 21:35):

Just to demonstrate what we're aspiring to. :-)

#### Scott Morrison (Oct 10 2018 at 06:11):

I gave another talk today, this time in the local "logic" seminar at ANU, which has quite a few participants who use/develop interactive theorem provers. (Notably Michael Norrish, who was involved, I think, in Sledgehammer.)

#### Scott Morrison (Oct 10 2018 at 06:11):

I recorded it, but unfortunately the screen capture part didn't work, so the video is just me getting in the way of an unreadable projector screen.

#### David Michael Roberts (Oct 10 2018 at 06:12):

No slides at https://tqft.net/web/talks yet :-P

#### Scott Morrison (Oct 10 2018 at 06:12):

The notes are at https://tqft.net/web/notes/load.php?name=talks/20181010-experiments-in-Lean, and the video, if you're _really_ keen, is at https://youtu.be/Ldhw4WfXELQ

#### David Michael Roberts (Oct 10 2018 at 06:12):

I was too fast...

#### Kevin Buzzard (Oct 10 2018 at 06:20):

So Scott -- you just recorded yourself when you gave the Adelaide colloquium? I am giving a colloquium in Sheffield a week today and I conjecture that these are not recorded in general. You got louder and quieter as you moved nearer and further from your laptop but I was quite happy to live with this minor issue because the advantages of seeing your talk far outweighed it.

#### Scott Morrison (Oct 10 2018 at 06:20):

Yeah, I just plonked my laptop on the table, and used "Camtasia 2", which is a very usable video recording/editing program.

#### Scott Morrison (Oct 10 2018 at 06:21):

It can capture the screen and camera simultaneously, and then arrange them as you like later.

#### Scott Morrison (Oct 10 2018 at 06:21):

It's the same software I used to make the installation videos.

#### Scott Morrison (Oct 10 2018 at 06:23):

If you decide to use it, let me know and I can tell you a few tricks.

#### Patrick Massot (Oct 10 2018 at 09:19):

It's nice to get these recordings but I guess they explain why Lean is always slower than you expect during your talk (in addition to the standard fact that computer misbehave when anyone is doing a demo)

#### Scott Morrison (Oct 10 2018 at 09:20):

Ugh, it was worse than that today. Some serious bug has crept into rewrite_search in the last few weeks...

#### Johannes Hölzl (Oct 10 2018 at 17:49):

Michael Norrish wasn't involved in Sledgehammer (AFAIK) but he is the maintainer of HOL4.

#### Patrick Massot (Oct 11 2018 at 14:30):

As a further data point in the question of usability of proof assistants in real-life (well, mathematical real-life), you can have a look at http://www.math.sciences.univ-nantes.fr/~gouezel/articles/morse_lemma.pdf (preliminary version).

See https://arxiv.org/abs/1810.04579. I post this link primarily to point out that everyone can now use this example which has been publicly released.

#### Patrick Massot (Oct 14 2018 at 11:15):

I need to start actually preparing my Thursday talk. Mario, do you think there is any hope we could get modules by, say, Tuesday? Or should I completely give up the hope to talk about how the perfectoid project is doing?

#### Sebastien Gouezel (Oct 14 2018 at 11:29):

At what time are you planning to arrive in Nantes?

#### Mario Carneiro (Oct 14 2018 at 11:33):

I've got a paper deadline by thursday, so I doubt it

#### Patrick Massot (Oct 14 2018 at 11:33):

Around lunch time

#### Mario Carneiro (Oct 14 2018 at 11:34):

primitive recursion

#### Mario Carneiro (Oct 14 2018 at 11:35):

you know, all that useless stuff in computability

#### Mario Carneiro (Oct 14 2018 at 12:13):

don't give me that frowny face, it's my day job that supports all this mathlib stuff

#### Kevin Buzzard (Oct 14 2018 at 13:02):

Patrick: who cares when modules are done. Perfectoids are not going to be done for a while yet, however all of us know that perfectoids can be done (which is the main claim) and will be done soon, although the actual path to nirvana involves Mario, Johannes, you, Johan, Me and Scott, at least, and we all have other things to do, so sometimes progress is slow.

#### Patrick Massot (Oct 14 2018 at 13:03):

My dream was to have a connected perfectoid project (with sorry) for my talk

#### Patrick Massot (Oct 14 2018 at 13:03):

not a completed project

#### Kevin Buzzard (Oct 14 2018 at 13:04):

https://mathoverflow.net/a/312661/1384 by the way

#### Patrick Massot (Oct 14 2018 at 13:04):

(well, completed was my initial dream, but I understood a long time ago that it was hopeless)

#### Kevin Buzzard (Oct 14 2018 at 13:07):

I think I take a more pragmatic view. I'll talk about perfectoids in my talk on Wednesday but I don't expect anyone to be racing to download and install Lean and then immediately cloning our project to see how it all works. Any newcomers face a mountain before they can even understand the complex current status of the perfectoid project properly, and anyone who doesn't download Lean (i.e. 99% of my audience) can just know that it's "work in progress with light very much at the end of the tunnel".

#### Patrick Massot (Oct 16 2018 at 18:44):

I tried my Thursday talk on a mostly innocent colleague today. @Sebastien Gouezel I need urgent confirmation that Nantes' colloquium last at least three hours...

#### Johan Commelin (Oct 16 2018 at 18:46):

O.oo... did the innocent colleague feel abused?

He seemed ok

#### Patrick Massot (Oct 16 2018 at 18:48):

I tried to demonstrate too much, and I had no reference point about how fast you can live code during a talk

#### Johan Commelin (Oct 16 2018 at 18:49):

Ok, well. Then it's good that you practiced!

#### Patrick Massot (Oct 16 2018 at 18:49):

Yes. Of course I usually don't practice my talks, but this time I new it was necessary

#### Sebastien Gouezel (Oct 16 2018 at 20:40):

I tried my Thursday talk on a mostly innocent colleague today. @Sebastien Gouezel I need urgent confirmation that Nantes' colloquium last at least three hours...

Yes, three hours from 17h15 to 18h15.

Thanks.

#### Patrick Massot (Oct 16 2018 at 20:42):

I'll be able to sleep then

#### Sebastien Gouezel (Oct 16 2018 at 20:42):

Once, we had a one hour colloquium by Laurent Lafforgue, that lasted almost two hours. And the chairman didn't dare to interrupt him. Maybe you can try this.

#### Patrick Massot (Oct 16 2018 at 20:43):

Please hold on, let me grab a Fields medal first...

#### Patrick Massot (Oct 16 2018 at 20:45):

However I guess I'll give a similar flavor talk: let me tell you about what could be a revolution in mathematics, but is currently completely useless...

#### Kevin Buzzard (Oct 16 2018 at 20:53):

My talk on Wed has changed quite a bit. I would say I learnt quite a lot in the last few weeks about what is going on here. Computer scientists and mathematicians have two different definitions of pure mathematics. They meet at the bottom with proofs that sqrt(2) is irrational etc, but after some point the sociological aspects of mathematics start influencing our tribe, and not theirs, and this makes some things quite different. Our experts proclaim what is proved and what is not proved; we try to choose the appropriate experts for each theorem, and our experts do not always get it right. However we have things that the CS world view does not have, like a very fluid understanding of techniques, and guiding principles such as the global Langlands reciprocity "principle", which is not even a well-defined statement but which seems to have well-defined consequences (for example functoriality, which can certainly be made into a formal statement (in more than one way, depending on how optimistic you want to be)). We also have very different opinions on what comprises beautiful mathematics. Both communities have a lot to offer each other in the future, I believe, and the main issue stopping this from happening is that there are very few experts in one area who know any more than epsilon about the modern tools available in the other area. That's what we have to change.

#### Sebastien Gouezel (Oct 16 2018 at 21:07):

However I guess I'll give a similar flavor talk: let me tell you about what could be a revolution in mathematics, but is currently completely useless...

I think I will be more convinced by your talk than his...

#### Kevin Buzzard (Oct 16 2018 at 21:08):

You [Sebastien] are a piece of evidence in my talk :-)

#### Patrick Massot (Oct 17 2018 at 07:22):

Yes, I thought about saying "proof assistants are nice and easy, anyone can use them, look at what Sébastien did!". But that works only with people who never heard of Sébastien, and I fear there won't be many of them in the audience tomorrow.

#### Kevin Buzzard (Oct 17 2018 at 07:33):

My talk is today. I'm going to say just that there are two different ways of doing pure mathematics and over the last year I have realised how little the two groups of people doing them are communicating with one another, and that both have a lot to offer the other side.

#### Kevin Buzzard (Oct 17 2018 at 07:35):

I don't think I'm going to make any claims about how using these tools is easy. In fact saying "I took a year of doing number theory research and learnt mathematics from scratch starting with undergraduate level, then graduate, then research" is not a particularly good advert for how easy they are. But this can be fixed. All we need is a good book.

#### Patrick Massot (Oct 17 2018 at 15:36):

Tomorrow at that time I'll be talking about Lean, and I may quickly show this website. Everybody, please refrain from emphasizing pain and bugs at that time :wink:

#### Johan Commelin (Oct 17 2018 at 16:39):

@Kevin Buzzard We are all desperately longing to hear your experience!

#### Kevin Buzzard (Oct 17 2018 at 16:43):

It went fine. About 100 people (including @Neil Strickland ), but I spent most of my talk talking about the "mess" that mathematics was in, and just the last 15 minutes suggesting that mathematicians and computer scientists should talk more. I met a computer scientist who said "I use Isabelle and the fact that there are no dependent types is problematic for mathematicians", which was not what Paulson said, but I need to figure out who is right.

#### Patrick Massot (Oct 17 2018 at 16:59):

Makes me think: @Kevin Buzzard and @David Michael Roberts, do you have news from the abc war?

#### Kevin Buzzard (Oct 17 2018 at 17:07):

Nothing from me. I don't think it's a war. The community have decided it's not a proof and everything else is now probably noise unless M actually decides to attempt to engage with the criticism.

#### Scott Morrison (Oct 17 2018 at 21:38):

You didn't record, did you?

I didn't.

#### Kevin Buzzard (Oct 17 2018 at 22:38):

I spent over half the talk giving what I thought was a fairly level-headed summary of things like the current status of the classification of finite simple groups and Arthur's work on the trace formula -- parts of maths where there are holes in the literature. I then talked a little bit about errors in the literature and also in the first half spent a bit of time philosophising about the nature of mathematics as done by humans and talking about various sociological issues which interfere with a formalist's viewpoint of what mathematics should be (I've been reading books by Bruno Latour). I then showed them Lean and some code that @Chris Hughes wrote, stressing that he had no computing experience when he arrived at Imperial 1 year ago (I did no live coding, for tedious technical reasons -- a minor system failure there) and showed off some of my summer students' work, and finished with a plea that mathematicians and computer scientists should work together more closely in the future on a common vision for pure mathematics, because we both have things to offer the other "tribe".

#### Kevin Buzzard (Oct 17 2018 at 22:59):

PS I'm speaking to 20 bright high school kids next week

#### Adam Kurkiewicz (Oct 18 2018 at 00:59):

@Scott Morrison great talk, it's a real shame that audio gets a lot worse halfway through the talk. Loved the joke about old mathematicians dying out :D (you guys do get a lot of freedom in what you can say at work!). I think what could have been valuable (maybe you said it and I missed it) was that regardless of how the proof is written, it gets compiled down to a simplified form checked by a trusted kernel. Otherwise using the backwards reasoning tactic seems a bit like a cheat!

#### David Michael Roberts (Oct 18 2018 at 02:31):

I emailed Mochizuki and he clarified a couple of things in response to some direct questions about his Report. I will continue to probe as I get time. For example: he discusses "gluing two [char 0] fields along their common subfield Q" in the Report. I imagined this to be some kind of formal colimit, or the pushout of rings or similar, and so asked what it really was: he said he meant the pushout of sets. I suspect there's a lot of these details that are in fact quite crucial to the category-theoretic constructions that are not very explicit.

#### Reid Barton (Oct 18 2018 at 03:42):

PS I'm speaking to 20 bright high school kids next week

What's your plan for this talk? I imagine it's easier to get a bright high school student to try out Lean than the average mathematician.

#### Kevin Buzzard (Oct 18 2018 at 05:17):

Plan for high school kids talk: definition of nat and addition; proof that addition is commutative on nat.

#### Johan Commelin (Oct 19 2018 at 06:58):

@Patrick Massot How did it go?

#### Patrick Massot (Oct 19 2018 at 07:31):

I think it was ok. Of course I rushed at the end and live coding doesn't work so well when you are already 5 minutes over time. But I think people were happy. I'll know more today because I'll spend the day in the department. There should be a video recording available at some point (but the talk was in French)

#### Johan Commelin (Oct 19 2018 at 19:42):

So, what kind of feedback did you get? @Patrick Massot

#### Patrick Massot (Oct 19 2018 at 20:26):

I got excellent feed-back. Several people thanked me for this talk today (but of course people who don't like talks rarely say it)

#### David Michael Roberts (Oct 19 2018 at 23:28):

Well, I have one small further insight: for Mochizuki, a diagram in a category is a subcategory, not a functor from a diagram shape. This probably stems from his desire to only ever use isomorphism classes of functors. I will write up a blog post when I can get all I sensibly can.

#### Johan Commelin (Oct 25 2018 at 03:33):

@Scott Morrison Do you have a quick list of lemmas that you added to back to enable the nice proof of infinitude of primes that you demoed in your talk?

#### Floris van Doorn (Oct 25 2018 at 04:22):

<deleted, I posted in wrong topic>

#### Scott Morrison (Oct 25 2018 at 05:01):

If you look at the back pull request, you’ll find that proof as the test case.

#### Kevin Buzzard (Oct 25 2018 at 05:10):

So I gave a school talk yesterday (to bright 17 year olds who had elected to go on a maths camp -- it's "half term" here so kids have a week off). It went better than my last school talk, it has probably got as far as "OK" but I am still not at "brilliant". One thing I have learnt is that even these bright schoolkids do not know what induction is which is a real problem when trying to do anything. However they do know what the complex numbers are! Here was what I did, and I think it went OK:

1) Observation that $1+2+3=6$ but they did make a choice about which addition to do first, because with $9-2-1$ it really matters which subtraction you do first. [NB this part of the talk is irrelevant because of what happened later]

2) Observation that $a+b=b+a$ is intuitively obvious if we think about addition as "getting more stuff" or "moving further in one direction", but that $0.999999999...<1$ is also kind of intuitively obvious, as is $0.999999999...=1$ (and we can't just argue about which one is right -- we need rules and definitions -- "pictures are not enough").

3)

inductive thing
| stop : thing
| tick : thing -> think


and a long time talking about what this meant, culminating in a general understanding that every thing looked like tick (tick (tick ...(tick (stop)))...

4) thing -> nats, stop -> zero, tick -> succ (there were giggles about the "suck" word, maybe there are better words). one := succ zero, two := succ (succ zero), two' := succ (one)

5) Proof that two = two' by rfl

6) Definition of induction as "proof by knocking over the first domino and watching the rest fall over" (note: kids these days have never seen a domino).

7) Definition of addition on nats and no attempt to prove anything like associativity because I realised it would simply be too hard. [rendering (1) obsolete]. Basically I bailed on associativity. I think that internalising the "two rules for addition" (the equation lemmas) and then using them to prove what is quite a complex thing (it's a good few lines) is too hard for schoolkids.

8) Proof that one + one = two from the axioms. This worked. Students could attempt to unravel what one + one = two means and see that the proof was rfl.

9) Now questions. I tell them that we prove a+b=b+a next, and ask what happens after that. "Definition of multiplication" says one. Eventually I get them to come up with the following plan: define + and * on nat, define int (because someone says "define subtraction!" and I say "We can't! How do we do 2 - 3?"), define +-* on int, define rat (because we can't do division until we do), define +-*/ on rat, define real, define +-*/ on real. Then define complex.

10) Show them the definition of complex as a pair of reals, invent stupid notation [x,y] for complexes because I tell them x+yi is not allowed because we didn't define + or i yet, then challenge them to define addition and multiplication, challenge them to prove on paper that multiplication is commutative.

So essentially no induction at all, and I get to show them random bits of Lean, and I think that this is just about a level which works. Still needs work, but a much more positive experience than last time when I was telling people that induction on false was false -> P.

#### Mario Carneiro (Oct 25 2018 at 05:27):

Re: "suck" giggles, I find that you can avoid some of that by pronouncing it "sook"

#### Mario Carneiro (Oct 25 2018 at 05:27):

at least you didn't have to talk about coq

#### Kevin Buzzard (Oct 25 2018 at 05:30):

I might just give up and call it nextone or something. Coq uses S I think, which is probably not good for a school talk either.

#### Andrew Ashworth (Oct 25 2018 at 06:47):

is pronouncing it in full as "successor" not an option :)?

#### Johan Commelin (Oct 25 2018 at 06:51):

It becomes tedious when you want to say 4 = succ (succ (succ (succ zero))), I guess...

#### Chris Hughes (Oct 25 2018 at 07:12):

How about a CS flavour with "increment". I think thinking about definitions of functions as computer programs is easier than talking about axioms, particularly because the distinction between axioms and definitions made in Lean is not made everywhere else. I certainly didn't have a clear idea about what an axiom was a year ago.

#### Kevin Buzzard (Oct 25 2018 at 07:41):

How about a CS flavour with "increment". I think thinking about definitions of functions as computer programs is easier than talking about axioms, particularly because the distinction between axioms and definitions made in Lean is not made everywhere else. I certainly didn't have a clear idea about what an axiom was a year ago.

I like inc! It's sort of obvious what it means, inc (inc zero) means increment zero twice.

#### David Michael Roberts (Oct 26 2018 at 03:05):

OR even add_one`

#### Adam Kurkiewicz (Oct 28 2018 at 13:06):

Kevin, how much time did it take you? When I did my workshop on commutativity of addition, I didn't get any giggles on succ, but it could be because by the time we got there, it was already 2 hours (with a single short break), and I had to give up on interactivity and fall back from workshop-style to lecture-style. I was still getting quite a lot of questions, and they at least saw me do the proofs, but some were getting really tired towards the end.

#### Kevin Buzzard (Oct 31 2018 at 11:50):

As a further data point in the question of usability of proof assistants in real-life (well, mathematical real-life), you can have a look at http://www.math.sciences.univ-nantes.fr/~gouezel/articles/morse_lemma.pdf (preliminary version).

Some time ago, I mentioned that I found a gap in a published paper while formalizing it in Isabelle. This gap is now corrected, and the new proof is completely formalized. The above paper explains the corrected proof, for mathematicians, but it also mentions the formalized proof. By the way, it raises interesting questions on the way to write a math papers when you have a formalized proof (when we need a lemma that is related, but not exactly the same, to results already in the literature, should we give the proof or just point the reader to the formalized proof?) We have tried to find some middle ground here, but I guess our way to write papers will have to change. Comments welcome!

https://mathoverflow.net/a/312661/1384 @Sebastien Gouezel

#### Johan Commelin (Oct 31 2018 at 11:54):

It's really cool that this is now the accepted answer!

#### Kevin Buzzard (Oct 31 2018 at 13:04):

Indeed -- that's what prompted me to post here.

Last updated: May 14 2021 at 07:19 UTC