Lean + LaTeX?

Stream: general

[Kevin Buzzard]

I've been reading work of Lamport about structured proofs. Here's an extract from https://github.com/ImperialCollegeLondon/M1P1-lean/blob/master/src/limits.lean :

-- We now prove that if aₙ → l and bₙ → m then aₙ + bₙ → l + m.
theorem tendsto_add (a : ℕ → ℝ) (b : ℕ → ℝ) (l m : ℝ)
  (h1 : is_limit a l) (h2 : is_limit b m) :
  is_limit (a + b) (l + m) :=
begin
  -- let epsilon be a positive real
  intros ε Hε,
  -- We now need to come up with N such that
  -- n >= N implies |aₙ + bₙ - (l + m)| < ε.
  -- Well, note first that epsilon / 2 is also positive.
  have Hε2 : ε / 2 > 0 := by linarith,
  -- Choose large M₁ such that n ≥ M₁ implies |a n - l| < ε /2,
  cases (h1 (ε / 2) Hε2) with M₁ HM₁,
  -- and similarly choose M₂ for the b sequence.
  cases (h2 (ε / 2) Hε2) with M₂ HM₂,
  -- let N be the max of M1 and M2
  let N := max M₁ M₂,
  -- and let's use this value of N.
  use N,
  -- Of course N ≥ M₁ and N ≥ M₂.
  have H₁ : N ≥ M₁ := le_max_left _ _,
  have H₂ : N ≥ M₂ := le_max_right _ _,
  -- Now say n ≥ N.
  intros n Hn,
  -- Then obviously n ≥ M₁...
  have Hn₁ : n ≥ M₁ := by linarith,
  -- ...so |aₙ - l| < ε /2
have H3 : |a n - l| < ε / 2 := HM₁ n Hn₁,
...

and so on and so on. The point is that I am spelling out the proof I would tell mathematicians in comments, and writing Lean code, which is sometimes self-evident (intros n Hn) and sometimes much harder for beginners to understand (e.g. using le_max_left -- a student could look up what this did, but it's much harder for them to find this function for themselves, and there are far more contrived lines in other parts of this repo).

I would like to make this look really sexy and I am almost sure that this should be possible with known technology. My dream would be to have what looks like a LaTeX document (perhaps viewed through a web browser) and when you hover over e.g. "Then obviously n >= M_1" you get some transient box which says have Hn₁ : n ≥ M₁ := by linarith,, and if you click on it then you somehow end up viewing a Lean file, or part of a Lean file, where you can look at the goal and change / edit things and play around (and then hit the "reset" button when you've screwed everything up).

In other words, I'd like to have some sort of thing which I can present as a "formally verified, but looks like LaTeX, proof that the limit of the sum is the sum of the limits".

I have no doubt that this sort of thing is possible. I've learnt sphinx but I am not quite sure if it is the tool for the job. Does anyone have any suggestions as to how one might be able to do this? There is no particular time frame and if it involves writing a bunch of code then maybe I can find people who will write this code for me. @Edward Ayers @Patrick Massot do either of you know about this kind of thing?

When it comes to writing Lean code I am 100% convinced that I could write code in the above style which could become "online notes" for a beginning analysis course (such as, let's say, the beginning analysis course in Imperial's new curriculum which starts in October). The notes would have the advantage that they are formally verified. But I do not understand enough about how to build the app I envisage and I would dearly like to hear some suggestions!

[Johan Commelin]

Do you remember Neil Stricklands demo? That might be a first approximation of what you want.

[Johan Commelin]

I meant this one: http://neil-strickland.staff.shef.ac.uk/dagstuhl/Systems/Lean_mathlib/Tasks/primes/

[Kevin Buzzard]

Ooh -- thanks for digging that up! @Neil Strickland how did you make this? My plan would be to hide the Lean completely and just have standard maths proof prose visible initially, but one can somehow open up the Lean to see it if one wants to.

[Joseph Corneli]

@Kevin Buzzard As a quick mockup in Emacs, I used Outshine mode to achieve the following (I realise this doesn't address the LaTeX side of things at all). This required changing the comment syntax a little bit. Screen-Shot-2019-01-23-at-14.41.33.png

[Joseph Corneli]

pressing TAB at the start of the buffer, or on a "headline", cycles between showing or not showing headlines / all content below that level.

[Joseph Corneli]

Maybe there's a similar plugin to Outshine for VS Code?

For presentation purposes, a related setup for Jupyter is described here:
http://chris-said.io/2016/02/13/how-to-make-polished-jupyter-presentations-with-optional-code-visibility/
with a clickable demo here:
https://nbviewer.jupyter.org/github/csaid/polished_notebooks/blob/master/notebook_polished.ipynb

[Patrick Massot]

Indeed this is something we can already mostly do with current technology, although we should be able to do it much better with the Lean 4 parser. Without the possibility to modify the Lean code, we could make something very easily (maybe only after thinking a bit more about the expected output with nested subproofs). In order to get a truly interactive version we could reuse Gabriel's work on the documentation view.

[Kevin Buzzard]

Right. Nothing you say surprises me. Now how do I actually _do_ it?

[Patrick Massot]

Which version? Interactive or read-only?

[Kevin Buzzard]

read-only would be a good start.

[Neil Strickland]

@Kevin Buzzard there is a new version of my examples now which you can find by following the links at http://bim.shef.ac.uk/lean.
At the moment they are not packaged in a way that makes it super-easy for anyone else to use the same framework, but it is not all that sophisticated either. The key ingredients are the files
1. http://bim.shef.ac.uk/lean/viewer.js
2. http://bim.shef.ac.uk/lean/viewer.css
3. http://bim.shef.ac.uk/lean/lean_task_index.html (which is a kind of template)
4. Libraries http://bim.shef.ac.uk/js/jquery.js and http://bim.shef.ac.uk/js/he.js
For each example you need
1. A copy of lean_task_index.html with the name, title and description filled in.
2. A lean file with comments delineated by the strings
"/-~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ "
and
"~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~-/"

Let me know if you want further details.

[Patrick Massot]

Neil, I just had a look at the very first example and something is not quite correct. apply refl is not using the refl tactic, it's using a lemma called refl (use F12 to see it). Use refl alone if you want the refl tactic.

[Neil Strickland]

Thanks, I'll fix that.

[Mohammad Pedramfar]

There is an old code here https://github.com/leanprover/lean.js

[Mohammad Pedramfar]

below in the examples. It's using lean interactively in the browser.

[Mohammad Pedramfar]

This seems to be exactly what you'd need to have an interactive lean webpage
https://github.com/leanprover/lean-client-js/

[Patrick Massot]

read-only would be a good start.

I'll try to find time over the week-end to build some demo

[Mohammad Pedramfar]

Using the libraries that I mentioned doesn't seem to be very easy. On the other hand, directly manipulating the online lean website seems to be doable. I'll try to make a small interactive example in a few days.

[Bryan Gin-ge Chen]

@Mohammad Pedramfar I played around with trying to get a custom version of the web editor working a while back in this thread: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/online.20leanprover . I didn't get too far though.

[Mohammad Pedramfar]

@Bryan Gin-ge Chen Thanks. Hopefully this will be easier, since here we only need to play around with the reactjs code to to something in the frontend without touching other parts.

[Mohammad Pedramfar]

I changed a few things in the online lean editor and turned it into this : lean-web-editor-with-latex.tar.gz

[Patrick Massot]

do you have a live demo somewhere?

[Mohammad Pedramfar]

I'm now running it at http://192.168.43.31:8080/

[Patrick Massot]

Firefox can’t establish a connection to the server at 192.168.43.31:8080.

[Wojciech Nawrocki]

That's a local-network IP :) It's not publicly accessible

[Patrick Massot]

(deleted)

[Mohammad Pedramfar]

I don't know why I thought http-server would run it on the web

[Mohammad Pedramfar]

is there an easy way to run it locally ?

[Patrick Massot]

You may be able to redirect something there

[Mohammad Pedramfar]

I don't know how to do that

[Patrick Massot]

Maybe you can explain how we could run it locally then, and what there is to see

[Mohammad Pedramfar]

sure, you'd need to follow the instructions in the readme. run these first :
npm install
./fetch_lean_js.sh
./node_modules/.bin/webpack

[Mohammad Pedramfar]

then you can into the "dist" folder and run "http-server"

[Mohammad Pedramfar]

At the moment the content is hardcoded, I have yet to add some kind of editor for the latex part. For any line in the latex, if you click on it, you'll see the corresponding lean code. You can change it and see the goals and warnings etc. but if you click on another line, the changes won't be saved. You can also see all the lean code at the same time, which would be like the normal online editor.

[Patrick Massot]

Nice!

[Patrick Massot]

People who want to know what we are talking about can go to http://pat.perso.ens-lyon.org/lean/ (it probably won't stay there for long)

[Patrick Massot]

I can't see any error message when I edit the Lean code

[Patrick Massot]

wait, the LaTeX doesn't work there

[Patrick Massot]

I used to work when served locally

[Mohammad Pedramfar]

The error messages didn't show up at all or were they late ? because the code is probably not the most efficient code possible !

[Mohammad Pedramfar]

You're right about the LaTeX. I think it works only if things are loaded in the correct order. It shouldn't be difficult to fix.

[Patrick Massot]

I don't have time to play with this (I have lectures to prepare) but it looks like a nice try

[Mohammad Pedramfar]

Thanks

[Kevin Buzzard]

Hey that's very cool!

[Mohammad Pedramfar]

Glad you liked it. I'll make it a bit more usable this week.

[Kevin Buzzard]

Could you try something from https://github.com/ImperialCollegeLondon/M1P1-lean/blob/master/src/limits.lean?

[Mohammad Pedramfar]

Sure, I'll sort it out this weekend

[Mohammad Pedramfar]

I worked on it a little bit and there's a bug that I haven't solved yet. I'll put it here as soon as I figure out how to make it work.

[Patrick Massot]

I also worked on a prototype of a read-only online viewer this week-end (no Lean running in the browser). I hope I'll have something to show later today.

[Patrick Massot]

I think I'll stop with my experiment for now. @Kevin Buzzard could you tell me if https://www.math.u-psud.fr/~pmassot/lean/ looks like what you wanted? You should mouse over everything to see what happens. This file is auto-generated from https://www.math.u-psud.fr/~pmassot/lean/source.html

[Patrick Massot]

In particular, tactic lines begin and end with an active zone that is currently not so easy to spot

[Mohammad Pedramfar]

That looks much cleaner than what I have here ! Could you send its code so I can add the interactive part to it ?

[Scott Morrison]

The UI to inspect the current tactic state is a bit confusing (invisible regions that highlight when you mouse over?)

[Scott Morrison]

(but otherwise pretty great!)

[Scott Morrison]

@Patrick Massot, I see in the source file that you've introduced your own mini mark-up language, e.g. things like:

/- Sub-section
Basic definitions
-/

I wonder if it might be better to just use markdown for this.

[Rob Lewis]

This is really cool! It looks like, if a line in the source has both code and a comment, only the comment is printed in the HTML, is that right? This means you see a bunch of } but no {.

[Scott Morrison]

I was about to say exactly the same thing! :-)

[Scott Morrison]

Having a link that pops out a proof into an interactive lean session would be pretty nice, too.

[Kevin Buzzard]

I'll show this to the kids today (I give an optional analysis lecture Tuesday 1-2 every week). It's really nice!

[Patrick Massot]

Allowing Markdown syntax for title is trivial, except that I put the constrain that the Lean file should compile, so the markdown has to be wrapped in a Lean comment. Would you like:

-- # My title

Of course one could also builds a tool which starts with a combined file and independently spits out a valid Lean file and a valid html file. But I really like to be able to write the source file in VScode with real time Lean compilation.

[Patrick Massot]

About lines like { -- We assume... : This is indeed handled as a special case. I know the result is a bit weird but I don't know what we want here. Does anyone has a clear idea of what the source and rendered result should look like?

[Patrick Massot]

I warned that the UI for showing tactics would be weird. Again I need suggestions. I don't want to have buttons shown permanently around each Lean line. Maybe I could show two buttons when the mouse is over the Lean line. This would be very touch unfriendly, but the interface is currently oriented towards wide screens anyway (although it would be trivial to but tactic state below the main view on narrow screens)

[Rob Lewis]

I think that having shading permanently around each Lean line would be fine. It doesn't have to look like a button, you could make it only slightly different from the background color.

[Johan Commelin]

Could you just make the entire line clickable? As soon as I click somewhere on a line of Lean code, the tactic state updates to that point. That would be quite intuitive, I think.

[Patrick Massot]

I could do that of course. I don't know whether it would become much longer to generate the file. I guess the Lean server responds pretty quickly to VScode, but here it means the lean to html conversion would ask for the Lean state at every single character of the proofs

[Patrick Massot]

This is useful only in case of rewrite with a list of lemmas or equalities. Otherwise the tactic state doesn't change in the middle of a line

[Johan Commelin]

Aah, no, I just meant to update to after that line.

[Johan Commelin]

So to bad for rw [foo, bar].

[Patrick Massot]

The problem is you also want to see the state before a line, especially the first line of a proof

[Patrick Massot]

UI is hard

[Patrick Massot]

I pushed what I think is Rob's suggestion (clickable areas are permanently slightly darker)

[Johan Commelin]

UI is hard

Definitely. And after >10 years of fooling around I've discovered that I'm not right person for that job (-;

[Mohammad Pedramfar]

I think it wouldn't be that difficult to add the interactive part to it. So that one can double click on a line and go into edit mode and play around.

[Mohammad Pedramfar]

Fixing the latex part in the interactive code that I sent only needed a few lines, but it took me a while to figure out what was wrong. And it seems like the lean server doesn't like firefox very much. It seems to be working in Chrome. Making a good UI on the other hand is gonna take some time. It would be much easier to add the interactive part to this UI.

[Patrick Massot]

I think I'm done removing all the hard-coded paths in my script, so that other people could play with it (I hope). It's not the same thing as claiming I've cleaned the code...

[Patrick Massot]

You can find it at https://github.com/leanprover-community/format_lean

[Patrick Massot]

The main thing is a very simple finite state machine. It's based on functions, so it's functional programming, right? The two main principles are:

• every function should take every opportunity to modify its arguments
• every function should use the state of the environment at the time it was defined

[Patrick Massot]

Every line from the source file is read, and falls into one of three categories: blank line, normal line and special line. Each reader registers a number of special lines handlers, as in https://github.com/leanprover-community/format_lean/blob/master/src/format_lean/lecture.py#L307-L311 which is the reader used in my demo. Each handlers has a regex that is match against the current line. If it matches, the handlers has the opportunity to inspect the current state of the file reader, and change it. It particular it will most probably change how normal lines and blank lines will be interpreted. The simplest case is https://github.com/leanprover-community/format_lean/blob/master/src/format_lean/lecture.py#L103-L109 which discards the Lean header. Of course it can say that normal lines will be somehow added to the output, maybe after querying a Lean server for tactic state. Then the collected output is passed to a renderer. The renderer I've defined in https://github.com/leanprover-community/format_lean/blob/master/src/format_lean/renderer.py in based on Jinja2.

[Patrick Massot]

People who only want to play with the UI can tweak the CSS at https://github.com/leanprover-community/format_lean/tree/master/sass (you need to know tiny bit if SASS) and the templates at https://github.com/leanprover-community/format_lean/tree/master/templates (you may need a tiny bit of Jinja2)

[Patrick Massot]

Of course I can try to write proper documentation if someone actually wants to modify all this

[Patrick Massot]

I should use the VScode regex for tactic state highlighting instead of pygment

[Bryan Gin-ge Chen]

VS Code's syntax highlighting uses "textMate" grammars, and when I looked before, I wasn't able to find any standalone syntax colorizers that accept that format. (The online lean demo pages get this functionality via the Monaco editor). I was only looking for JS packages though, it's possible there are some in python.

[Patrick Massot]

I used pygments, which is a python lib (actually I used Gabriel's fork which is more suitable for Lean). But the VScode extension does not use textMate for the tactic state view, see https://github.com/leanprover/vscode-lean/blob/master/src/infoview.ts#L412-L418

[Bryan Gin-ge Chen]

Ah, of course. I missed the most important part "tactic state".

[Kevin Buzzard]

Just to say publically what I said to Patrick yesterday -- on Friday I showed this to some students who I meet weekly and who went to my lectures last term (so know what Lean is) but have no interest in Lean. They were really interested in this though, and wanted more. It's like this (Coq) but infinitely nicer-looking. I'll try and work on some more of this today. I have a bunch of basic analysis formalised here and it would be great to get it into Patrick's format.

[Kevin Buzzard]

One of them was complaining that they couldn't follow the proof given by the lecturer for one of the theorems, and I pointed out that this could never happen with a formalised version because you can always chase back.

[matt rice]

I guess my main quibble with it would be the format, I have been looking at the various 'literate programming' tools around, which take a different approach, instead of encoding the documentation in the source comments, they embed the sources in a documentation format, and then extract the sources. I guess perhaps that would be useful if you wanted to e.g. embed excercises, and extract stand alone snippets from the book.

[Patrick Massot]

This is really two different point of view on the same thing. In my version the focus is on writing documented Lean code, not writing documentation containing Lean code

[Kevin Buzzard]

I know nothing about "literate programming" -- I want to write a "book" here, a companion to our undergraduate analysis course at Imperial College which will be part of our new curriculum.

[Patrick Massot]

In particular my version allows to get the interactivity of Lean while writing.

[Patrick Massot]

Matt, the thing you want already exists, it's used to write TPIL for instance

[matt rice]

Patrick: Thanks, will look, i had looked at the sources for Logic & Proof, but hadn't seen a mechanism for extracting the sources from it

[matt rice]

One other thing to note about css, i ran across https://github.com/edwardtufte/tufte-css yesterday which looks really nice

[Patrick Massot]

I've added Mardown support. Now any text comment

/-
My comment
-/

is run through https://github.com/miyuchina/mistletoe I chose this markdown python library a bit at random, let's see if it works

[Patrick Massot]

I just added a command line client, see https://github.com/leanprover-community/format_lean/blob/master/README.md#usage

[Patrick Massot]

Now I'll stop for one week again, waiting for Kevin to write example Lean files.

[Scott Morrison]

One of them was complaining that they couldn't follow the proof given by the lecturer for one of the theorems, and I pointed out that this could never happen with a formalised version because you can always chase back.

I'm pretty unconvinced of this. There are many proofs in mathlib which are only human decipherable with enormously more effort than would be required for a good textbook proof, _even if_ you already read Lean well.

[Scott Morrison]

The solution, of course, is for us all to have more time on our hands, and to improvement human comprehensibility of mathlib proofs. :-)

[Scott Morrison]

Increasing expectations of readability would be a reasonable first step.

[Mario Carneiro]

This is another thing I miss with metamath - you can actually say that and be correct. Most proof assistants, including lean, do too much behind the scenes work so that it is not really comprehensible to a human even in relatively simple cases

[Patrick Massot]

@Scott Morrison did you see the proofs we are talking about? There are nothing like mathlib proofs. There are written specifically for students, and heavily commented.

[Scott Morrison]

Absolutely! Those proofs are fantastic. I was only disagreeing with Kevin's suggestion that one could always drill down until you understood everything. Drilling down probably means descending into mathlib, and understanding becomes increasingly difficult.

[Patrick Massot]

Oh yes, you shouldn't drill too deep, that's notoriously dangerous

[Kevin Buzzard]

Oh I see what you mean. I have been thinking about this a little -- it would be nice if ultimately we could guide some drilling to the library which will hide all our dirty work (e.g. tactics such as "apply le_max_left <|> linarith") and then put big warning signs in there not to drill any more!

[Chris Hughes]

I'm not convinced hiding dirty work is a good idea for teaching Lean. As soon as someone tries to write their own proof, they'll find they need to know how to do the dirty work. Maybe it is a good idea for teaching analysis though.

[Mario Carneiro]

strong agree on this. If you actually expect to teach people how to use the tool, they have to feel the "typical experience", not the "rose-colored talk version of lean"

[Kevin Buzzard]

This is not a tool for teaching people Lean.

[Kevin Buzzard]

This is a tool for teaching people analysis.

[Kevin Buzzard]

I absolutely agree that you can't teach Lean this way. Neil tried it with his write-ups and I think they're too long and complicated. This is a different thing. This is for students who know no Lean but want to pass a basic analysis exam. The Lean code is intimidating but the tactic state is not. The tactic state, and in particular the goal, often make a lot of sense here.

[Kevin Buzzard]

If you want to teach mathematicians Lean you have to start with 2+2=4 and (a+b)^2=a^2+2ab+b^2.

[Kevin Buzzard]

Stuff they learnt at school and can hence assume.

[Mario Carneiro]

I am not sure about that. The solution to the first one is DTT magic and the second is lean magic

[Kevin Buzzard]

Well, you have TPIL to teach your tribe how to use Lean. Teaching my tribe is harder and maybe I still haven't worked out how to do it.

[Mario Carneiro]

examples like that just leave people bewildered as to what just happened

[Kevin Buzzard]

But I've got 150 feedback forms and I am now convinced that I want to teach people analysis and have Lean ticking away in the background

[Kevin Buzzard]

We teach people mathematics in high school in a completely non-rigorous way; arguments like limit of sin(x)/x is 1 is proved by "draw a picture". Then students go to university and see how it's done rigorously.

[Mario Carneiro]

I think it's great for demos, to show that lean has a chance of really getting to the hard problems by making the easy problems easy, but that's not the same thing

[Mario Carneiro]

I'm quite dubious as to the actual long term success of this approach. The people who last are the ones who dive into the details

[Kevin Buzzard]

Maths lectures are one level of rigour up. We present proofs which we claim are rigorous, at least most of the time. But arguments are still sometimes handwavey. Chris was told in 2nd year lectures the other day that the proof of some theorem about two integrals being equal was "draw the obvious picture".

[Mario Carneiro]

For first introductions, you really want to get that spark of interest, and these approaches work well. But after that, once they are committed, you want to step back and do it systematically

[Mario Carneiro]

you can't handwave at lean, no matter how much you want to

[Kevin Buzzard]

Maths students don't have enough time to learn Lean properly but I want them to engage with it at some level anyway.

[Kevin Buzzard]

Just like last year, it's past Christmas and my 1st years realise that in a few months they have a bunch of exams to deal with. I get 6-7 people at Xena and they're all dedicated people who can actually write Lean code. But there are literally 100 other people who would be interested in that web page.

[Mario Carneiro]

I think for a formalizer or budding formalizer, the most valuable skill is being able to deconstruct a mathematician's argument. When they say draw the obvious picture, draw it, convince yourself, and go back over why you are convinced and work it down to something precise

[Kevin Buzzard]

I can't make them learn the details of how it all works. But they can see the goals changing and the hypotheses appearing -- that stuff is easy to understand and they have never seen anything like it before.

[Kevin Buzzard]

I have to work with what I have, and what I have is people who can't get over the learning curve but who i want to engage anyway. This is a good half way house for them; I've tried it and I have had very positive results.

[Mario Carneiro]

I think it's similar to the difference between a textbook for a foreign language and a phrasebook

[Kevin Buzzard]

I know exactly who I'm teaching and what I want to teach them -- and at the end of the day, I want to make sure they can do an epsilon-delta argument correctly. That's the important thing. They're paying £9000 or £28000 and at the end of it they have to pass an exam with epsilon-delta questions in. That's what they're interested in.

[Mario Carneiro]

the phrasebook will help you out on the spot, let you get around, and so on. But it's not building a foundation for the dedicated, and while it's not really harmful you will still need to go back and cover the basics if you decide to go all in

[Kevin Buzzard]

If they look at the material presented like in Patrick's html file, then at any stage they can see a completely rigorous assertion. This is what many of them need to see at this stage -- because this is what the exam will be in. They want to pass the exam -- that is what they are mainly motivated by. This will teach them what they want to learn.

[Kevin Buzzard]

I say again -- I am not attempting to teach them Lean.

[Kevin Buzzard]

I am attempting to show them that Lean can be used as a good learning tool for mathematics.

[Mario Carneiro]

I am not saying you are doing it wrong, even. There are different learning objectives in play

[Kevin Buzzard]

They come here from school and they think very vaguely, many of them. They struggle in pure maths. Next year the syllabus is being completely revamped and it will be much harder. The new students next year will need even better teaching materials, and I think I am looking at them in Patrick's html file.

[Mario Carneiro]

I think the isabelle style statement chaining + heavy automation approach is good as an antidote to vague thinking in that it can spot check your assertions, before you go too far off the rails

[Mario Carneiro]

For the ones who ask how does math work it's better to have a more explicit metamath style where they can drill down until their heads explode (or they are satisfied, whichever comes first)

[Mario Carneiro]

right now lean is much closer to the first approach

[Mario Carneiro]

although you can use it in the second way, like TPIL does

[Patrick Massot]

I really think we should create that "Lean for teaching" stream in order to clear this confusion.

[Kevin Buzzard]

I got Patrick's formatter working :D http://wwwf.imperial.ac.uk/~buzzard/xena/analysis_stuff/sandwich.html

[Kevin Buzzard]

sandwich.png

[Kevin Buzzard]

Source is http://wwwf.imperial.ac.uk/~buzzard/xena/analysis_stuff/sandwich.lean -- a Lean file which compiles (for me -- there are local imports)

[Johan Commelin]

There is weird typesetting in so for all n ≥ N

[Johan Commelin]

Otherwise, this confirms that Patrick created something cool (-;

[Kevin Buzzard]

Yeah, in the png? I fixed it in the html. I'm still figuring out what one can get away with.

[Kevin Buzzard]

it confirms that Patrick created something which someone other than Patrick can run, which is a useful thing to know.

[Kevin Buzzard]

Perhaps I won't mention that I had to move my import limits.lean into mathlib to get it to compile :joy:

[Patrick Massot]

Currently the tool allows only one supporting library, but this is easy to fix. First I need to teach RSA, but then I'll fix that tonight

[Scott Morrison]

I wonder if we could extend the usefulness of these non-interactive literate formalisations. Given that the goal state is so helpful for someone following along but perhaps having difficulty seeing what a step achieves, we could try to make the goal state even more understandable. What if we turned every name appearing in the goal state into a hyperlink, that links back to the source code of mathlib where it is defined? (Ideally, this would be a html-ified copy of the source code, that in turn has hyperlinks everywhere.) More complicated, as an optional extra names that have been defined in the current document could be have relative hyperlinks, that revealed that fragment of Lean code.

[Scott Morrison]

Independently, merely having a fully crosslinked html version of the mathlib source code would be pretty helpful. I'm not sure if our current tooling lets us write this, yet.

[Patrick Massot]

In principle this is already possible. I'm a bit hesitant to work on this because it should become much easier with the Lean 4 parser. But, in principle, we can ask Lean for information at every single location of the source file, and create the links

[Patrick Massot]

@Kevin Buzzard I just pushed a new commit adding the possibility to handle full projects (see README). The nice thing is everything setup you need can be read from leanpkg.toml so you can simply go to the root of your project and type format_project. I also added a handler for theorems if lemmas are not good enough for you.

[Reid Barton]

In principle this is already possible. I'm a bit hesitant to work on this because it should become much easier with the Lean 4 parser. But, in principle, we can ask Lean for information at every single location of the source file, and create the links

I have a really clunky implementation of this lying around somewhere, I could dig it up at some point

[Johan Commelin]

Little styling-bug report for Lean formatter (@Patrick Massot). In Kevin's demo: http://wwwf.imperial.ac.uk/~buzzard/docs/lean/sandwich.html click on the line "Note that $N \ge N_a$ and $N \ge N_c$," in the proof. Then you get two Lean-lines of the same length; but the tactic-state-buttons don't align.

[Johan Commelin]

Also, low-urgency feature request: Can we get resizable tactic-state window? Like in VScode?

[Johan Commelin]

Also: I can't get to see "no goals" when I click on the last tactic-state-button of the proof (after split;linarith in Kevin's demo).

[Mario Carneiro]

Does putting a comma on the last line help with that?

[Johan Commelin]

Probably, but it would be nice if that is not part of the user manual of Lean-formatter...

[Johan Commelin]

Anyway, these are pretty low-urgency things, I would say.

[Mario Carneiro]

I'm sad that I can't click on obvious_ineq to find out what it is

[Johan Commelin]

Hahaha

[Mario Carneiro]

but I guess I'm not the target audience

[Patrick Massot]

Johan, the two styling issues you mention are straight from the Lean source. The lines that don't line up actually have different length in http://wwwf.imperial.ac.uk/~buzzard/xena/analysis_stuff/sandwich.lean (one of them ends with spurious spaces). I guess I could strip spaces at the end of lines, but it would remove some of the author liberty. The missing "no goals" comes straight from Lean. Adding a comma at the end of the line in the source would indeed fix that issue. The resizable tactic state is probably possible, I need to study more javascript and css

[Kenny Lau]

feedback from a guinea pig from imperial year 2:

It’s nice / The animations are smooth / But it’s not obvious that you need to press on the definitions to reveal the code / Lines, not definitions / Apart from that, it’s really nice

[Patrick Massot]

One other thing to note about css, i ran across https://github.com/edwardtufte/tufte-css yesterday which looks really nice

@matt rice I tried it in http://pat.perso.ens-lyon.org/math114/cours1.html and I agree it looks pretty nice. Here I also used other templates of lean-format to get inlined tactic state. This is part of lecture notes I'm writing for my logic and proof course. The source is at http://pat.perso.ens-lyon.org/math114/source.html for people who want to see how Markdown and LaTeX are handled.

[Patrick Massot]

@Kevin Buzzard I have a new iteration for you: http://pat.perso.ens-lyon.org/M1P1/ is your sandwich file, rendered in "no lean proof" mode, only tactic state. It also uses the new tactic state tampering feature, see the config file used for this render (beware my Firefox needs to be explicitly told to use UTF8 when opening that file)

[Patrick Massot]

I guess it's clearer if I post the config file here:

templates = "templates"
js = ["lean_tufte.js"]
css = ["tufte.css", "et-book.css", "with_tufte.css"]
assets = ["et-book", "tufte.css", "et-book.css"]
outdir = "M1P1"
only = ["sandwich.lean"]
tactic_state_filters = [
  ['is_limit ([^ ]+) ([^ ]+)', '\1ₙ tends to \2'],
  ['ℕ → ℝ', 'ℝ-valued sequence'],
  ['([a-z]) n([ ,\n])', '\1ₙ\2'],
  ['no goals', 'Current goal completed!'],
]

[Patrick Massot]

Of course this kind of regex tampering is very brittle, but we won't be able to do much more before Lean 4's customizable pretty printer :four_leaf_clover:

[Johan Commelin]

Wow! That looks very slick. Congratulations!

[Johan Commelin]

One little point of feedback. You have joined together the lines in the html output. I agree that this is a good move. But the result is that you have two grey boxes next to each other (1 end-of-line, 1 start-of-line) that have the same resulting tactic state. I think it would be even better if you could merge these boxes into one box.

[Patrick Massot]

Of course one problem is that, in more complicated proofs, those two boxes could lead to different states (in case of subproofs). We would need more examples of formatted proofs actually. Then we'll be able to decide whether something smarter should be done.

[Patrick Massot]

I'd like to also point out that everyone can play with this tool. Modifying CSS and template files doesn't even require any python knowledge

[Mohammad Pedramfar]

Kevin Buzzard I have a new iteration for you: http://pat.perso.ens-lyon.org/M1P1/ is your sandwich file, rendered in "no lean proof" mode, only tactic state. It also uses the new tactic state tampering feature, see the config file used for this render (beware my Firefox needs to be explicitly told to use UTF8 when opening that file)

This looks great! Is this compiled with the latest version on github ? There seems to be some bugs in the code, I couldn't run it.

[Kevin Buzzard]

I completely missed this! That's beautiful Patrick!

[Patrick Massot]

Yes, I can confirm this builds using the latest version on github. You need to put the config file I linked to in the project directory

[Patrick Massot]

oh wait

[Patrick Massot]

you need more

[Patrick Massot]

I'm sorry

[Patrick Massot]

I forgot some pieces

[Scott Morrison]

A suggestion for this tool --- I can see you're writing the types to give "human friendly" names in places (like "R-valued sequence").

[Scott Morrison]

I wonder if it might be better to give the human friendly name as a comment after the actual type.

[Scott Morrison]

This way reading the proof states is still a bridge towards learning Lean, and ensures consistency (I haven't seen an example, but I'm worried that these rewrites might not be uniformly applied when the types appear nested inside something else?)

[Patrick Massot]

I've put a standalone archive at www.math.u-psud.fr/~pmassot/M1P1.tar.gz

[Patrick Massot]

The human friendly type is clearly a horrible hack, waiting for :four_leaf_clover: pretty-printer

[Patrick Massot]

currently it's nothing more than a regex search and replace

[Scott Morrison]

Okay. Even with a better pretty printer, I like the idea of displaying types in a way that can be re-entered in Lean, with read-only versions for humans in comments.

[Scott Morrison]

In any case, this is cool stuff!

[Patrick Massot]

This style of rendering is designed to hide Lean as much as possible, there are other choices of templates that display also the Lean statement and proof. It's a different intent.

[Patrick Massot]

Anyway, if you like this you can use it. If people start using it I'll keep improving it.

[Patrick Massot]

Although I'd like to do some actual Lean this week (but I'm stuck until someone understands what happens with https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/uniform.20split/near/159860012)

[Mohammad Pedramfar]

I finally finished adding the interactive component to Lean formatter. The syntax is the same as before and I tried to keep the changes minimal. https://github.com/mpedramfar/format_lean.

[Johan Commelin]

Sounds good! :tada: I'll try to find some time to play around with this. But my time is a bit limited this week :sad:

[Scott Morrison]

I needed to run pip3 install ., not pip install ..

[Scott Morrison]

arguta:mathlib scott$ format_project --outdir my_dir
Traceback (most recent call last):
  File "/usr/local/bin/format_project", line 12, in <module>
    from format_lean.renderer import Renderer
  File "/usr/local/lib/python3.7/site-packages/format_lean/renderer.py", line 9, in <module>
    from pygments.lexers import LeanLexer
ModuleNotFoundError: No module named 'pygments'

[Scott Morrison]

After installing Gabriel's fork of pygments, I ran into

arguta:mathlib scott$ format_project --outdir my_dir
Traceback (most recent call last):
  File "/usr/local/bin/format_project", line 23, in <module>
    from interactive.server import interactive_server
ModuleNotFoundError: No module named 'interactive'

and will give up at this point. :-)

[Mohammad Pedramfar]

I needed to run pip3 install ., not pip install ..

If running pip is not the same as running pip3, then you might be working outside any virtual environment (the default python version of ubuntu is 2.7). This code needs python >= 3.
I also realised that in "INSTALL.md", in the instructions, I have a link to Patrick's Lean formatter. If you have installed that version of Lean formatter, then it makes sense for it to say it can't find the 'interactive' module. I fixed the typos.

[Scott Morrison]

Yes, I'm just running on a mac, where pip is for the python 2 installation, and pip3 is for the python 3. I don't think this is uncommon, and I think it's pretty uniform to have a pip3 available, so I'd just suggest changing the instructions to use that.

[Scott Morrison]

So... what do I do to fix this "No module named 'interactive'" problem?

[Mohammad Pedramfar]

So... what do I do to fix this "No module named 'interactive'" problem?

I just learned something new about how python installs packages. I'll fix it.

[Kevin Buzzard]

The dream of a fully interactive Lean/LaTeX book gets a step closer :-)

[Mohammad Pedramfar]

I think it should be working smoothly now. The installation process is also more straight-forward. It's a bit hacky, but it should do the job.