Zulip Chat Archive

Stream: general

Topic: Will lean support HoTT in the future?


Keyao Peng (Jul 21 2020 at 09:39):

I find HoTT or CuTT would be more convenient to the mathematicians, would Lean support this in the future?
And I heard of another new language Arend that supports CuTT, would this be a potential proof assistant?

Johan Commelin (Jul 21 2020 at 09:46):

@Keyao Peng you might be interested in reading through previous discussions on the topic. See https://leanprover.zulipchat.com/#narrow/stream/238830-Lean-for.20the.20curious.20mathematician.202020/topic/Previous.20discussions.20on.20Lean.20and.20HoTT/near/204191082 and the posts below it for a bunch of links.

Johan Commelin (Jul 21 2020 at 09:48):

Summary:

  1. Lean 2 supported HoTT
  2. Lean 3 has a HoTT mode
  3. Several mathematicians on this chat are completely unconvinced that HoTT brings useful features
  4. Several other mathematicians have played a bit with HoTT and think it looks very cool and has a lot of promise, but in practice it currently, right now doesn't seem to help with actual formalisation of mathematics. This could change in the future, but it requires fundamental improvements of the proof assistents.

Johan Commelin (Jul 21 2020 at 09:48):

Finally, yes, Arend looks cool.

Thomas Eckl (Jul 26 2020 at 19:41):

@Johan Commelin How do you activate the HoTT mode in Lean 3?

Bryan Gin-ge Chen (Jul 26 2020 at 19:44):

Lean 3 doesn't have a HoTT mode built in. The Lean 3 HoTT repository uses some tricks to "disable" singleton elimination which is inconsistent with HoTT.


Last updated: Dec 20 2023 at 11:08 UTC