Zulip Chat Archive

Stream: general

Topic: Lean + LaTeX?


Kevin Buzzard (Jan 23 2019 at 11:23):

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 ε ,
  -- 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 (Jan 23 2019 at 11:41):

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

Johan Commelin (Jan 23 2019 at 11:43):

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

Kevin Buzzard (Jan 23 2019 at 11:56):

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 (Jan 23 2019 at 14:43):

@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 (Jan 23 2019 at 14:46):

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 (Jan 23 2019 at 14:50):

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 (Jan 23 2019 at 16:08):

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 (Jan 23 2019 at 16:21):

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

Patrick Massot (Jan 23 2019 at 16:58):

Which version? Interactive or read-only?

Kevin Buzzard (Jan 23 2019 at 17:32):

read-only would be a good start.

Neil Strickland (Jan 23 2019 at 17:54):

@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 (Jan 23 2019 at 17:58):

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 (Jan 23 2019 at 18:01):

Thanks, I'll fix that.

Mohammad Pedramfar (Jan 23 2019 at 18:39):

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

Mohammad Pedramfar (Jan 23 2019 at 18:40):

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

Mohammad Pedramfar (Jan 23 2019 at 18:48):

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

Patrick Massot (Jan 23 2019 at 21:53):

read-only would be a good start.

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

Mohammad Pedramfar (Jan 24 2019 at 15:03):

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 (Jan 24 2019 at 15:09):

@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 (Jan 25 2019 at 10:00):

@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 (Jan 27 2019 at 20:41):

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

Patrick Massot (Jan 27 2019 at 20:45):

do you have a live demo somewhere?

Mohammad Pedramfar (Jan 27 2019 at 20:48):

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

Patrick Massot (Jan 27 2019 at 20:48):

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

Wojciech Nawrocki (Jan 27 2019 at 20:49):

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

Patrick Massot (Jan 27 2019 at 20:49):

(deleted)

Mohammad Pedramfar (Jan 27 2019 at 20:49):

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

Mohammad Pedramfar (Jan 27 2019 at 20:50):

is there an easy way to run it locally ?

Patrick Massot (Jan 27 2019 at 20:50):

You may be able to redirect something there

Mohammad Pedramfar (Jan 27 2019 at 20:55):

I don't know how to do that

Patrick Massot (Jan 27 2019 at 21:00):

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

Mohammad Pedramfar (Jan 27 2019 at 21:03):

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 (Jan 27 2019 at 21:04):

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

Mohammad Pedramfar (Jan 27 2019 at 21:07):

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 (Jan 27 2019 at 21:11):

Nice!

Patrick Massot (Jan 27 2019 at 21:14):

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 (Jan 27 2019 at 21:15):

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

Patrick Massot (Jan 27 2019 at 21:16):

wait, the LaTeX doesn't work there

Patrick Massot (Jan 27 2019 at 21:16):

I used to work when served locally

Mohammad Pedramfar (Jan 27 2019 at 21:20):

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 (Jan 27 2019 at 21:22):

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 (Jan 27 2019 at 21:23):

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

Mohammad Pedramfar (Jan 27 2019 at 21:24):

Thanks

Kevin Buzzard (Jan 27 2019 at 21:54):

Hey that's very cool!

Mohammad Pedramfar (Jan 28 2019 at 00:20):

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

Kevin Buzzard (Jan 28 2019 at 22:30):

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

Mohammad Pedramfar (Feb 01 2019 at 21:57):

Sure, I'll sort it out this weekend

Mohammad Pedramfar (Feb 04 2019 at 00:35):

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 (Feb 04 2019 at 07:21):

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 (Feb 04 2019 at 21:18):

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 (Feb 04 2019 at 21:20):

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

Mohammad Pedramfar (Feb 04 2019 at 22:12):

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 (Feb 04 2019 at 22:49):

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

Scott Morrison (Feb 04 2019 at 22:49):

(but otherwise pretty great!)

Scott Morrison (Feb 04 2019 at 22:55):

@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 (Feb 04 2019 at 22:57):

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 (Feb 04 2019 at 23:00):

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

Scott Morrison (Feb 04 2019 at 23:00):

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

Kevin Buzzard (Feb 05 2019 at 07:31):

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 (Feb 05 2019 at 07:34):

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 (Feb 05 2019 at 07:36):

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 (Feb 05 2019 at 07:38):

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 (Feb 05 2019 at 08:36):

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 (Feb 05 2019 at 08:42):

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 (Feb 05 2019 at 19:31):

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 (Feb 05 2019 at 19:32):

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 (Feb 05 2019 at 19:33):

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

Johan Commelin (Feb 05 2019 at 19:33):

So to bad for rw [foo, bar].

Patrick Massot (Feb 05 2019 at 19:34):

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

Patrick Massot (Feb 05 2019 at 19:35):

UI is hard

Patrick Massot (Feb 05 2019 at 19:36):

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

Johan Commelin (Feb 05 2019 at 19:48):

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 (Feb 05 2019 at 19:58):

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 (Feb 05 2019 at 20:07):

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 (Feb 05 2019 at 21:14):

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 (Feb 05 2019 at 21:14):

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

Patrick Massot (Feb 05 2019 at 21:15):

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 (Feb 05 2019 at 21:21):

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 (Feb 05 2019 at 21:22):

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 (Feb 05 2019 at 21:26):

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

Patrick Massot (Feb 05 2019 at 21:52):

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

Bryan Gin-ge Chen (Feb 05 2019 at 22:02):

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 (Feb 05 2019 at 23:44):

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 (Feb 06 2019 at 01:00):

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

Kevin Buzzard (Feb 09 2019 at 12:47):

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 (Feb 09 2019 at 12:48):

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 (Feb 09 2019 at 15:57):

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 (Feb 09 2019 at 15:59):

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 (Feb 09 2019 at 16:00):

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 (Feb 09 2019 at 16:00):

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

Patrick Massot (Feb 09 2019 at 16:00):

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

matt rice (Feb 09 2019 at 16:02):

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 (Feb 09 2019 at 16:05):

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

Patrick Massot (Feb 09 2019 at 20:31):

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 (Feb 09 2019 at 21:13):

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

Patrick Massot (Feb 09 2019 at 21:14):

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

Scott Morrison (Feb 09 2019 at 21:24):

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 (Feb 09 2019 at 21:25):

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 (Feb 09 2019 at 21:25):

Increasing expectations of readability would be a reasonable first step.

Mario Carneiro (Feb 09 2019 at 21:27):

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 (Feb 09 2019 at 21:50):

@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 (Feb 09 2019 at 21:55):

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 (Feb 09 2019 at 21:55):

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

Kevin Buzzard (Feb 09 2019 at 23:12):

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 (Feb 10 2019 at 00:47):

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 (Feb 10 2019 at 00:48):

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 (Feb 10 2019 at 01:24):

This is not a tool for teaching people Lean.

Kevin Buzzard (Feb 10 2019 at 01:24):

This is a tool for teaching people analysis.

Kevin Buzzard (Feb 10 2019 at 01:25):

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 (Feb 10 2019 at 01:26):

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 (Feb 10 2019 at 01:27):

Stuff they learnt at school and can hence assume.

Mario Carneiro (Feb 10 2019 at 01:27):

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

Kevin Buzzard (Feb 10 2019 at 01:28):

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 (Feb 10 2019 at 01:28):

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

Kevin Buzzard (Feb 10 2019 at 01:28):

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 (Feb 10 2019 at 01:29):

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 (Feb 10 2019 at 01:29):

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 (Feb 10 2019 at 01:30):

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 (Feb 10 2019 at 01:31):

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 (Feb 10 2019 at 01:31):

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 (Feb 10 2019 at 01:32):

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

Kevin Buzzard (Feb 10 2019 at 01:32):

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 (Feb 10 2019 at 01:33):

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 (Feb 10 2019 at 01:33):

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 (Feb 10 2019 at 01:33):

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 (Feb 10 2019 at 01:34):

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 (Feb 10 2019 at 01:35):

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

Kevin Buzzard (Feb 10 2019 at 01:36):

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 (Feb 10 2019 at 01:36):

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 (Feb 10 2019 at 01:37):

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 (Feb 10 2019 at 01:37):

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

Kevin Buzzard (Feb 10 2019 at 01:37):

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

Mario Carneiro (Feb 10 2019 at 01:38):

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

Kevin Buzzard (Feb 10 2019 at 01:38):

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 (Feb 10 2019 at 01:41):

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 (Feb 10 2019 at 01:42):

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 (Feb 10 2019 at 01:43):

right now lean is much closer to the first approach

Mario Carneiro (Feb 10 2019 at 01:43):

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

Patrick Massot (Feb 10 2019 at 08:44):

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

Kevin Buzzard (Feb 11 2019 at 12:02):

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

Kevin Buzzard (Feb 11 2019 at 12:03):

sandwich.png

Kevin Buzzard (Feb 11 2019 at 12:17):

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 (Feb 11 2019 at 12:20):

There is weird typesetting in so for all n ≥ N

Johan Commelin (Feb 11 2019 at 12:21):

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

Kevin Buzzard (Feb 11 2019 at 12:21):

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

Kevin Buzzard (Feb 11 2019 at 12:22):

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

Kevin Buzzard (Feb 11 2019 at 12:23):

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

Patrick Massot (Feb 11 2019 at 12:49):

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 (Feb 11 2019 at 20:55):

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 (Feb 11 2019 at 20:56):

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 (Feb 11 2019 at 20:58):

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 (Feb 11 2019 at 21:47):

@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 (Feb 12 2019 at 00:57):

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 (Feb 12 2019 at 09:13):

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 NNaN \ge N_a and NNcN \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 (Feb 12 2019 at 09:14):

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

Johan Commelin (Feb 12 2019 at 09:17):

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 (Feb 12 2019 at 09:21):

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

Johan Commelin (Feb 12 2019 at 09:22):

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

Johan Commelin (Feb 12 2019 at 09:23):

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

Mario Carneiro (Feb 12 2019 at 09:23):

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

Johan Commelin (Feb 12 2019 at 09:23):

Hahaha

Mario Carneiro (Feb 12 2019 at 09:23):

but I guess I'm not the target audience

Patrick Massot (Feb 12 2019 at 12:08):

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 (Feb 12 2019 at 13:23):

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 (Feb 15 2019 at 22:24):

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 (Feb 22 2019 at 22:39):

@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 (Feb 22 2019 at 22:42):

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 (Feb 22 2019 at 22:43):

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 (Feb 23 2019 at 05:20):

Wow! That looks very slick. Congratulations!

Johan Commelin (Feb 23 2019 at 05:22):

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 (Feb 23 2019 at 08:34):

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 (Feb 23 2019 at 08:40):

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 (Mar 03 2019 at 19:44):

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 (Mar 03 2019 at 20:19):

I completely missed this! That's beautiful Patrick!

Patrick Massot (Mar 03 2019 at 21:15):

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 (Mar 03 2019 at 21:15):

oh wait

Patrick Massot (Mar 03 2019 at 21:15):

you need more

Patrick Massot (Mar 03 2019 at 21:15):

I'm sorry

Patrick Massot (Mar 03 2019 at 21:15):

I forgot some pieces

Scott Morrison (Mar 03 2019 at 21:16):

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 (Mar 03 2019 at 21:17):

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

Scott Morrison (Mar 03 2019 at 21:18):

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 (Mar 03 2019 at 21:18):

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

Patrick Massot (Mar 03 2019 at 21:19):

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

Patrick Massot (Mar 03 2019 at 21:19):

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

Scott Morrison (Mar 03 2019 at 21:22):

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 (Mar 03 2019 at 21:22):

In any case, this is cool stuff!

Patrick Massot (Mar 03 2019 at 21:23):

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 (Mar 03 2019 at 21:24):

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

Patrick Massot (Mar 03 2019 at 21:25):

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 (Apr 15 2019 at 05:05):

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 (Apr 15 2019 at 05:07):

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 (Apr 15 2019 at 05:18):

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

Scott Morrison (Apr 15 2019 at 05:21):

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 (Apr 15 2019 at 05:22):

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 (Apr 15 2019 at 06:43):

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 (Apr 15 2019 at 06:57):

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 (Apr 15 2019 at 06:57):

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

Mohammad Pedramfar (Apr 15 2019 at 08:15):

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 (Apr 15 2019 at 08:18):

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

Mohammad Pedramfar (Apr 15 2019 at 18:18):

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.


Last updated: Dec 20 2023 at 11:08 UTC