bulleting / browers questions

Stream: general

[Paige North]

Hi! I'm looking at the current version of Lean in the browser. I have two questions:

1. Is there a way to bullet cases like in Coq?

2. It seems to not work perfectly in Safari, but it seems to work in Firefox from what I can tell. Can people recommend which browsers work well with Lean? I'm thinking of using it for teaching this semester (in a discrete math course) so I'd like as much information as possible about this to pass on to my students.

Thanks!

[Kevin Buzzard]

There is more than one version of Lean in the browser -- are you using 3.4.1 or 3.5.0?

[Paige North]

I'm using 3.4.1 since that's linked by the tutorial.
I didn't realize there was a newer version. Are there any significant differences?

[Bryan Gin-ge Chen]

Here's a link to the community Lean web editor.; the main differences are:

• It uses a newer version of Lean and the mathlib library. For the moment it uses the latest nightly versions of both, though at some point we may decide to do version pinning.
• The UI has been changed (hopefully for the better?).
• You can input a URL to a Lean file at the top and the editor will start with that file open (provided the file is available via a cross-origin request, e.g. if you link to a "raw" file on github).
• It uses a different strategy for caching the Lean library files.

Unfortunately, both versions of the Lean web editor are broken in recent versions of Safari due to an issue in WebKit's handling of WebAssembly. Both Firefox and Chrome should work decently well for both.

As for "bulleting", I only have a little bit of experience with Coq, but I think the equivalent in Lean is using curly braces to "focus" on a goal; e.g.:

example (A B : Prop) (ha : A) (hb : B) : A ∧ B :=
begin
split,
{ exact ha, },
{ exact hb, },
end

(Here's a web editor link.)

[Rob Lewis]

Depending on how you're organizing your course, you might want to consider using CoCalc. The downside is that the free version can be a little sluggish, although it didn't bother me that much. The upsides are that you get a lot of course management features, Lean runs on CoCalc's server instead of in JavaScript, and the editor feels more professional than the default Lean web editor. (I don't mean to insult the people working on the web editor. The CoCalc editor really serves a different purpose and is literally professional software.)

[Gihan Marasingha]

I'd like to try CoCalc, but it comes with a price tag I would have to justify: $3499 / year for the basic large course (250 projects) subscription. Is that the option most people go for?

[Kevin Buzzard]

Do you want all 250 students able to work on Lean and having the ability for multiple people to be able to edit files at once? If so, cocalc is your only option. I've only ever used it for smaller courses, because I was not sure I could justify making all of my large 1st year class engage with Lean.

If you just pay $14 per month, you can get an individual account which I believe will enable you to do multiplayer editing with no lag -- I believe you just get the interested students to get a cocalc account and then you can give them access to a shared project. Alternatively you could pay for a far smaller course and then offer the chance to the students to sign up -- you might find that many are not interested, or find it too hard. Lean is very hard to learn unless you put the effort in. It's easy to forget how difficult the learning curve is if you've played around with it and got the hang of it. One comment I heard from @Athina was that learning how to use Lean at the same time as learning new mathematics is very difficult, and people might fare better learning Lean with mathematics they already know.

@William Stein did I get that bit right about the individual account?

[William Stein]

@Kevin Buzzard @Gihan Marasingha yes, Kevin everything you said is right. You could start small and flexibly have only some students use CoCalc. It's easy to change how your cocalc project upgrades are allocated at any time. Also the price for a year is really a full 12-month year (not just a semester), in case that's not clear.

[Gihan Marasingha]

Thanks @Kevin Buzzard and @William Stein. Those are excellent suggestions. I could purchase a smaller course package and get the students to work in groups.

@William Stein : in case I get the money, do you have an option for an even larger course? My current 1st year course has >300 students. Of course, it may be that <=250 engage with Lean, but I'd rather know what the possibilities are.

Perhaps it's unrealistic, but I feel that the less able 1st year students would benefit most from Lean. When marking 1st year exams, I often see incorrect 'proofs' that the composite of two injective functions is injective. I suspect these students think their proof is correct, but have no mechanism to tell them otherwise (other than waiting for an unreliable human tutor).

@Athina : have you published your paper, or have a pre-print? I'm very curious to read your analysis of working with Lean.

[Kevin Buzzard]

@Athina loads of people asked me about your paper at the Lean conference in Pittsburgh last week! I told them they had to wait :-)

[William Stein]

@Gihan Marasingha -- you can combine subscriptions, e.g., you could buy a 250-student subscription and a 70-person subscription to cover more than 300 students. Just email help@cocalc.com and we can do anything, including working with invoicing/PO's/special terms of service/trials, etc. Also, yesterday I implemented our first version of site licenses (finally!), which provide for a lot more flexibility...

[Gihan Marasingha]

@William Stein Thanks very much for letting me know. (P.S. I love SageMath).