Henry Story

Stream: new members

[Henry Story]

Hi, I am exploring the space of proof assistants and got pointed to Lean from the category theory zulip channel via a youtube presentation by Scott Morison. (That's all I now at present). It looks very nice.
The Lean Doc says

A prior version, Lean 2, had special support for homotopy type theory.

which of course raises the question if that has been integrated into Lean 3, or if that is a dead end project, or if something even better was planned (e.g. Modal HoTT)? I was just curious.

[Scott Morrison]

There is a project doing some HoTT in Lean3: https://github.com/gebner/hott3, but it is not particularly active.

[Scott Morrison]

It demonstrates that it is possible, but there doesn't appear to be much interest in pursuing it at the moment.

[Henry Story]

I had just found that, following a link from this page. :-)

[Scott Morrison]

Most of the community of mathematicians working with Lean are very happy to work in classical foundations (well, if "classical" includes dependent type theory), and are more interested in doing "mathematics" as usually practiced.

[Scott Morrison]

That said, for a mathematician to learn the basics of dependent type theory, the first few chapters of the HoTT book are great, even if you have no interested in univalence.

[Henry Story]

yes, I agree, the first few chapters of the HoTT book are great.
I am actually coming from programming background in Scala (Odersky pointed me to HoTT 6 years ago) and so I have made a detour through Category Theory.

[Scott Morrison]

I'm a mathematician, but my programming background is partially in scala. A bit of a strange language, but I do like it. Lean is better, though, and Lean4 will actually be a proper programming language (not just a proof assistant), so all the scala folks should come join us. :-)

[Henry Story]

Very cool! When will that come out?
Two key features would be compiling to JavaScript and I believe to Web Assembly (I have not used WAssembly yet - and know little of it - but as I understand it could allow one to write very efficient reasoners for the browser, something I am interested for the semantic web. My understanding is that Web Assembly can be thought of as a new type of bytecode. As I understand it also allows one to compile existing c programs to it).

[Patrick Massot]

Lean3 itself compiles to Wasm, this is what you see at https://leanprover-community.github.io/lean-web-editor/

[Patrick Massot]

(Lean 3 is a C++ program)

[Patrick Massot]

There is no release date for Lean 4, but the first alpha version seems pretty close.

[Patrick Massot]

And indeed the situation with HoTT is: many people here would love to see it usable, but it currently isn't, so we play with what works today. This is not proof assistant specific. There is no sizable library of general mathematics formalized in HoTT, in any proof assistant. General mathematics here means what you learn in an undergrad math degree. Existing HoTT-based libraries are all about category theory and even more about HoTT for its own sake.

[Patrick Massot]

About Wasm, don't expect your web browser to execute Lean at any speed comparable to the native speed of course.

[Henry Story]

It's very helpful to know that the browser version is running wasm. That's helping me see what wasm is capable of :-)
I am very interested in proofs mostly for security reasoning. That's also why I have been looking to Modal HoTT as security reasoning can be seen as a form of modal logic. See e.g. Martin Abadi's work (An MS fellow) such as Access Control in a Core Calculus of Dependency. That should be doable with CoC based tools as it only requires Indexed Strong Monads, but I like to know what I may be missing :smile: .

[Scott Morrison]

Modal logic per se doesn't need any HoTT, of course, and has various partial formalizations in standard proof assistants.

[Henry Story]

yes, David Corefield who wrote the (philosophically oriented) book Modal HoTT only gets to the latest HoTT work in the last chapter of the book. But his key point as I understand is that modalities arise out of adjunction of slice categories.
As I understand the Modal HoTT work is showing how all modalities such as linearity, ... can be brought under one roof. But it's over my head at present. I need to become fluent in proof assistants to get to understand that first :-)