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
Conversation
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
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
3
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
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
3
This is the bit I was referring to, fwiw (time stamp 1:06:51):
2
3
You’re unable to view this Tweet because this account owner limits who can view their Tweets. Learn more
I hate it, this is the sort of thing that scares people away from contributing to projects and approaching researchers
3
6
Yeah, it's really not really my style to be honest - like I'd rather try to figure out how to use those people if I can. That said I've consistently failed to upskill new contributors on my projects… probably because I am so disorganised and confused all the time. 🤦♂️
With a coherent enough community you can just get them in touch with the right people
1
1
IDK what I love about the Coq community is that I've always felt so respected within it, at least in France. They are actively trying to make contributing as approachable as possible, recognizing for example gender imbalances in open source contributions
1
2
Show replies