Zulip Chat Archive

Stream: Lean for the curious mathematician 2020

Topic: Previous discussions on Lean and HoTT


Johan Commelin (Jul 17 2020 at 10:30):

@Thomas Eckl There have been several discussions on Zulip about this topic, which you might find entertaining: https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/what.20is.20wrong.20with.20HoTT

Johan Commelin (Jul 17 2020 at 10:30):

https://leanprover.zulipchat.com/#narrow/stream/116395-maths/topic/Univalence

Johan Commelin (Jul 17 2020 at 10:31):

https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/HoTT.20in.20Lean

Johan Commelin (Jul 17 2020 at 10:33):

@Thomas Eckl That doesn't mean that we shouldn't have another discussion/chat in the future (-;

Thomas Eckl (Jul 17 2020 at 15:00):

The threads made interesting reading. I discovered Gabriel Ebner's project porting the Lean 2 HoTT library to Lean 3 - I will try to use it asap.

I also liked how Kevin Buzzard and you insist that the ordinary working mathematician does not want to be bothered with type theory, let alone homotopy type theory. But the point for me is something else to what Kevin alludes: Type theory, and then homotopy type theory allows to do maths in a way that working mathematicians are much more used to than proofs in ZFC. There are more mathematical objects than just sets; types are sets "done right", with proper objects as elements; and with univalence you can argue up to isomorphism. That's what allured me to (homotopy) type theory, not some perverse interest in foundations. And that's why I also don't care if homotopy type theory does not make formalizing easier (a comment of Mario Carneiro), it just should not get more difficult (and unfortunately, there is a possibility for that, as Floris van Doorn pointed out). My hope is that it feels more natural, and that's what will attract mathematicians.

Actually, there is a fascinating parallel to the change from 19th to 20th century mathematics: The reason why mathematicians followed the more formal ways of doing mathematics paved by Hilbert and leading up to Bourbaki, despite the rage of the old and influential guard around Felix Klein and Henri Poincare, was not thatbthey cared so much about foundations, but becuase it was easier to do mathematics that way. Frank Quinn wrote a lot about this era and what conclusions we should draw from it nowadays : https://www.ams.org/notices/201201/rtx120100031p.pdf . I think that's also a point against Kevin's dismissal of "implementation issues":They play a decisive role, but often in a way not consciously recognized.

I think for the next time I will continue to formalize localization in my little project (and maybe extend it to the formalization of schemes, which Kevin would like to see). Then I will have a better idea whether my hopes are realistic and will be ready for a more substantial discussion.

Johan Commelin (Jul 17 2020 at 16:16):

@Thomas Eckl Those are very good points, and I think I mostly agree with what you say. I find HoTT (as a general principle, not 1 implementation, so also cubical stuff, etc) very enticing as a mathematician.

But right now I do not see what it buys me when I try to formalise things. And this is probably mostly a technical issue. Currently, the univalence principle is an extremely nice idea, but the implementations in current provers are such that in practice you avoid it. (This is what I learnt explicitly during my brief experiment in Coq.)

I also think that the burden of proof for usability rests with the proponents of HoTT. But it seems that the community around HoTT is (mostly) more interested in pushing the foundations, rather than demonstrating that you can do "real-world maths" in proof assistants using HoTT.

And that's totally fine. Because maybe by pushing those foundations, they will solve the problems I was talking about 2 paragraphs up. And maybe it will just take some time before enough mathematicians jump on the bandwagon.
But I'm not the right person for developing these foundations. So right now, I'm happy to use Lean, because that's where the maths is happening, and that's what I care about.

In the end, and that's also what Kevin has stressed before, lots of people should just try lots of systems. That's the best way to push their boundaries, and the best way to figure out what we really need.

Kevin Buzzard (Jul 17 2020 at 16:45):

I think that if we can finally get mathematicians using these systems there will be a lot of things we will learn about their pros and cons when it comes to mathematics.

Heather Macbeth (Jul 17 2020 at 17:06):

Thank you for linking to the article by Quinn, it makes for interesting reading.

Johan Commelin (Jul 17 2020 at 18:46):

Wow, that was an interesting read indeed!

Johan Commelin (Jul 17 2020 at 18:47):

The last page suggests that we should redesign NNG (kids don't like walls of text), and give some really precise and clear explanations. And then just make 8 year old kids play the game.

Johan Commelin (Jul 17 2020 at 18:48):

We've seen that some of our own kids are actually capable of playing it. Can we scale from 5 kids to 5000 kids?

Johan Commelin (Jul 17 2020 at 18:48):

(Maybe the most important thing would be to have a professional web-designer have a look at the project.)

Kevin Buzzard (Jul 17 2020 at 21:27):

Yeah I've said this before -- the NNG could really benefit from being looked at by someone who actually knows what they're doing. If we could get it working on mobile it would be awesome but maybe this is just asking too much.

Anatole Dedecker (Jul 17 2020 at 21:31):

Typing code on mobile is terrible because of automatic correction

Kevin Buzzard (Jul 17 2020 at 21:32):

My kids are always on their phones. It would be great to get lean onto mobile somehow

Dan Stanescu (Jul 17 2020 at 21:33):

Anatole Dedecker said:

Typing code on mobile is terrible because of automatic correction

Unless you turn automatic correction off.

Alex J. Best (Jul 17 2020 at 21:36):

Yeah for mobile it seems there would need to be a remote lean server, rather than actually running lean on the phone. Perhaps this is something that should be thought about in conjunction with the https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/cloud.20computing.20possibilities/near/197868435 cloud computing thread. How feasible is it to have a lean server that everyones app connects to (probably to one lean instance each) that then runs 10 sessions of the nng at once?

Dan Stanescu (Jul 17 2020 at 21:39):

Notwithstanding the beauty of a dedicated general server, the NNG is actually run on an Imperial College server AFAIK. So on the phone all you'd need would be a web browser-:)

Alex J. Best (Jul 17 2020 at 21:39):

Wait whattttt

Dan Stanescu (Jul 17 2020 at 21:40):

I mean this:

https://wwwf.imperial.ac.uk/~buzzard/xena/natural_number_game/

Dima Pasechnik (Jul 17 2020 at 21:43):

Perhaps, find a way to pay William Stein et al. to run NNG off cocalc.com - surely they'd take care of scalability very well indeed.

Kevin Buzzard (Jul 17 2020 at 21:46):

The web pages are hosted at Imperial but I think the way it works is that the lean server is hosted on your own computer

Bryan Gin-ge Chen (Jul 17 2020 at 21:47):

The issue with mobile and the NNG is that the web editor uses Monaco, which has terrible mobile support. In fact, most Javascript text editors are pretty awful on mobile devices at the moment. I'm hoping that Codemirror 6 will solve all our issues, but it's still not ready for primetime (and we'd have to write some new integration code as well).

Bryan Gin-ge Chen (Jul 17 2020 at 21:48):

We've discussed this before and I don't think anything has changed since then https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/online.20leanprover/near/170927874

Bryan Gin-ge Chen (Jul 17 2020 at 21:49):

Hmm, actually Codemirror 6 is further along than I expected. Maybe I'll take a closer look when I have time... (at least a week from now, unfortunately).

Dima Pasechnik (Jul 17 2020 at 21:51):

Kevin Buzzard said:

The web pages are hosted at Imperial but I think the way it works is that the lean server is hosted on your own computer

hmm, no, NNG works from any computer with a web browser, and no Lean in sight. I'm sure a Lean instance is running at Imerial.
(unless you can embed Lean in Javascript, which I highly doubt)

Kevin Buzzard (Jul 17 2020 at 21:52):

You can embed Lean in Javascript.

Bryan Gin-ge Chen (Jul 17 2020 at 21:54):

Lean can be compiled to webassembly and then run from javascript.

Dan Stanescu (Jul 17 2020 at 21:55):

OK, so that's the solution to the puzzle.

Bryan Gin-ge Chen (Jul 17 2020 at 21:55):

The NNG and the lean-web-editor are already statically hosted. There are no "backend" servers running Lean. When your browser visits those pages, it downloads a webassembly version of Lean and runs that on your computer.

Dan Stanescu (Jul 17 2020 at 21:55):

Can any smartphone execute javascript? Or webassembly.

Bryan Gin-ge Chen (Jul 17 2020 at 21:55):

Most can; the issue with the NNG on phones is that the input interface hardly works.

Bryan Gin-ge Chen (Jul 17 2020 at 21:56):

See the thread I linked above.

Dan Stanescu (Jul 17 2020 at 21:57):

OK, so aside from that it should work. Does it only mean "harder to type", or is there more to it?

Dima Pasechnik (Jul 17 2020 at 21:57):

OK, I stand corrected. Webassmebly is hard, I am very impressed!

Bryan Gin-ge Chen (Jul 17 2020 at 21:58):

Different issues on Android and iOS, I think. I can't test with Android, but on my iPad / iPhone, (last time I tried, months ago) typing in Lean code leads to weird zooming-in issues. Maybe it's better now, not sure.

Bryan Gin-ge Chen (Jul 17 2020 at 21:58):

In the thread I linked above, @Wojciech Nawrocki said that backspace doesn't work on Android.

Dan Stanescu (Jul 17 2020 at 22:04):

For what I can see right now from a brief test, it works on my iPad. Modulo the many characters/inputs I didn't check, of course.

Dima Pasechnik (Jul 17 2020 at 22:04):

perhaps, a CS student project to fix this mobile thing is possible. Probably fullblown javascript editor is not needed, either.

Bryan Gin-ge Chen (Jul 17 2020 at 22:05):

I guess one thing we could figure out what's the best way to have mobile users trigger unicode conversion, since it's harder to hit "tab" (at least on iPhones and iPads). While hitting "space" works, it's kind of annoying if you have to backspace away those extra spaces all the time.

Bryan Gin-ge Chen (Jul 17 2020 at 22:08):

A full blown editor with some extension support certainly makes it much easier to work with Lean, since the editor should be able to display the info / warning / error diagnostics, be able to provide completions, as well as support hover for doc strings, etc. And this is even before trying to implement the new widget functionality, which greatly increases usability of the tactic state...

Dan Stanescu (Jul 17 2020 at 22:10):

Bryan Gin-ge Chen said:

I guess one thing we could figure out what's the best way to have mobile users trigger unicode conversion, since it's harder to hit "tab" (at least on iPhones and iPads). While hitting "space" works, it's kind of annoying if you have to backspace away those extra spaces all the time.

I think just about anything one could use for an escape character would be harder to type on a mobile.
But on the iPhone at least you can store your favorite character/escape sequences.

Bryan Gin-ge Chen (Jul 17 2020 at 22:11):

Yeah, I was thinking we could potentially pop up a floating panel with some useful icons on it. Sort of like how mobile games sometimes pop up a little directional control, since mobile keyboards lack arrow keys and such.

Dima Pasechnik (Jul 17 2020 at 22:18):

people use smartphones differenly from computer keyboards, what works well on a keyboard is often awful on a touchscreen, and the other way around. IIRC, Jupyter does not use a full-blown js editor, it has something built-in. And Jupyter works on smartphones reasonably well, I think

Dima Pasechnik (Jul 17 2020 at 22:19):

I just tried NNG on a ChromeOS tablet (probably very close to a typical Android tablet), and there was just no <tab> to hit on the onscreen keyboard.

Bryan Gin-ge Chen (Jul 17 2020 at 22:24):

Are you able to get backspace to work?

(Hitting <space> will also do the conversion, but it also adds a space.)

Dima Pasechnik (Jul 17 2020 at 22:28):

no, hitting space to get \lambda properly displayed just didn't work. On an Android phone it's even worse, as the onscreen keyboard covers too much of the screen.

Bryan Gin-ge Chen (Jul 17 2020 at 22:29):

Ah, that's too bad.

Heather Macbeth (Jul 17 2020 at 22:30):

Dima Pasechnik said:

people use smartphones differenly from computer keyboards, what works well on a keyboard is often awful on a touchscreen, and the other way around. IIRC, Jupyter does not use a full-blown js editor, it has something built-in. And Jupyter works on smartphones reasonably well, I think

Maybe the experience needs to be radically re-thought, to be touchscreen-friendly and reduce typing. For example little buttons saying "rw" and "intros" and so on. When you type a lemma name, underscores appear, and when you tap one, new buttons for any of the existing hypotheses whose type matches that of the underscore.

Heather Macbeth (Jul 17 2020 at 22:31):

(Of course, this would be an implementations headache with a combinatorics problem wrapped inside.)

Dima Pasechnik (Jul 17 2020 at 22:46):

Heather Macbeth said:

Dima Pasechnik said:

people use smartphones differenly from computer keyboards, what works well on a keyboard is often awful on a touchscreen, and the other way around. IIRC, Jupyter does not use a full-blown js editor, it has something built-in. And Jupyter works on smartphones reasonably well, I think

Maybe the experience needs to be radically re-thought, to be touchscreen-friendly and reduce typing. For example little buttons saying "rw" and "intros" and so on. When you type a lemma name, underscores appear, and when you tap one, new buttons for any of the existing hypotheses whose type matches that of the underscore.

for NNG this kind of interface could be wonderful - the ability to type arbitrary text is more of an obstacle than a help there, IMHO.

Scott Morrison (Jul 18 2020 at 02:28):

Now that we have widgets, we really should remake http://incredible.pm/ in javascript, talking to a Lean server, and then pop-out that interface into a web-browser.

Heather Macbeth (Jul 18 2020 at 02:35):

Wow, that's great, and perfect for a phone (I would think).

Heather Macbeth (Jul 18 2020 at 02:35):

Well, maybe a phone with a very large screen.

Kevin Buzzard (Jul 18 2020 at 06:20):

Or a tablet

Kyle Miller (Jul 18 2020 at 06:28):

In this vein, something like Scratch for tactic proofs would be cool. I once looked into whether something like this existed when I taught a discrete math course a couple years ago, but I don't remember anything turning up.

Thomas Eckl (Jul 18 2020 at 15:49):

This thread drifetd away from the original topic; I opened a new topic continuing the discussion of Quinn's article under
https://leanprover.zulipchat.com/#narrow/stream/113488-general/topic/Lessons.20from.20History .


Last updated: Dec 20 2023 at 11:08 UTC