Brendan Zabarauskas on Twitter: "@jonmsterling @TaliaRinger @kamatsu8 @samth From a talk I saw (recorded from a Lean users conference thing they had at the beginning of the year) they seemed like they were open to improvements, but wanted really clear, concrete proposals, ideally with realistic plans to implement." / Twitter

May 25, 2021

I think they put more thought into efficiency, but also some of the extra design involved was due to the fact that they don't get hcongr_ideal, which you do get in cubical

1

3

This Tweet was deleted by the Tweet author. Learn more

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Talia Ringer

@TaliaRinger

May 25, 2021

Yeah, but they now seem totally uninterested in converging. I'm happy to translate some of the ideas over to cubical, I'm generally good at that kind of thing, but it helps to have experts on both sides of the bridge interested

2

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Talia Ringer

@TaliaRinger

May 25, 2021

Fair, I just think for your every day humans, automation and usability are what will matter. Another thing I'm happy to help with is building search procedures that discover and prove type equivalences automatically

3

You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more

Replying to

From a talk I saw (recorded from a Lean users conference thing they had at the beginning of the year) they seemed like they were open to improvements, but wanted really clear, concrete proposals, ideally with realistic plans to implement.

2:44 PM · May 25, 2021Twitter Web App

Replying to

From what Leo said I get the feeling they are pretty overworked might have felt burned in the past with lots of people with ideas, but perhaps not following through. That said, this is all just going off a talk and I'm not privy stuff behind the scenes.

1

2