Jon Sterling, Is it time for a new proof assistant?

Stream: general

[Srayan Jana]

I saw this video pop up on my youtube recommended, and I figured it was pretty relevant to Lean (considering the presenter mentioned Lean multiple times)
https://youtu.be/7oBkEbKJvnE?si=CJhNG-6JmyawhoXf
https://hottest-seminar.github.io/hottestfiles/Sterling-2025-09-25-HoTTEST.pdf

[Srayan Jana]

I think the presenter is @Jonathan Sterling and seems to be part of this conference series: https://hottest-seminar.github.io/

[Chris Henson]

An additional piece of relevance is that the current prototype is implemented in Lean.

[Wrenna Robson]

@Jonathan Sterling I just wanted to say that I really enjoyed reading this!

[(deleted)]

I know that HoTT people really believe in their theory to the point where they invite teenagers who take part in olympiads to attend lectures on HoTT. But when will it be widely adopted by the formal verification community or will it remain something obscure

[(deleted)]

Yeah, I also enjoy reading the slides

[(deleted)]

I do feel that we do need a new proof assistant based on some new foundation. And if the HoTT community manages to make a good enough proof assistant this could convert many people to HoTT. I'm definitely not a fan of having to use native_decide just because decide is too weak

[(deleted)]

And if HoTT solves this problem then it could even offer a better user experience than Lean