Previous discussions on Lean and HoTT

Stream: Lean for the curious mathematician 2020

[Johan Commelin]

@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]

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

[Johan Commelin]

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

[Johan Commelin]

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

[Thomas Eckl]

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]

@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]

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]

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

[Johan Commelin]

Wow, that was an interesting read indeed!

[Johan Commelin]

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]

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]

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

[Kevin Buzzard]

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]

Typing code on mobile is terrible because of automatic correction

[Kevin Buzzard]

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

[Dan Stanescu]

Anatole Dedecker said:

Typing code on mobile is terrible because of automatic correction

Unless you turn automatic correction off.

[Alex J. Best]

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]

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]

Wait whattttt

[Dan Stanescu]

I mean this:

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

[Dima Pasechnik]

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]

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]

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]

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]

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]

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]

You can embed Lean in Javascript.

[Bryan Gin-ge Chen]

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

[Dan Stanescu]

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

[Bryan Gin-ge Chen]

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]

Can any smartphone execute javascript? Or webassembly.

[Bryan Gin-ge Chen]

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

[Bryan Gin-ge Chen]

See the thread I linked above.

[Dan Stanescu]

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

[Dima Pasechnik]

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

[Bryan Gin-ge Chen]

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]

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

[Dan Stanescu]

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]

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

[Bryan Gin-ge Chen]

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]

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]

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]

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]

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]

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]

Are you able to get backspace to work?

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

[Dima Pasechnik]

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]

Ah, that's too bad.

[Heather Macbeth]

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]

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

[Dima Pasechnik]

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]

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]

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

[Heather Macbeth]

Well, maybe a phone with a very large screen.

[Kevin Buzzard]

Or a tablet

[Kyle Miller]

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]

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 .