Seeking Lean users for an observation study

Stream: general

[Joachim Breitner]

That sounds like a fun and useful exercise. I often have the impression that we (FRO and community) try hard to improve the usability of lean, but we do so often based on gut feeling and anecdotal evidence. I don't know how much of that is part of the design of the study, but would hope we get some useful insight out for how we can further improve lean UX. Therefore I hope many of you will take part!
(Conflict of interest disclaimer: I did my post doc at that group and think they and what they are do are pretty cool :-))

[Luigi Massacci]

When would this be approximately?

[Jessica Shi]

Luigi Massacci said:

When would this be approximately?

The study is ongoing and will likely continue at least for the next few weeks, and possibly longer. If you're interested, there's an option on the form to indicate any scheduling constraints you might have!

[Alex Kontorovich]

I think this is a very interesting idea; on the few rare occasions that I've gotten to watch other people actually work in Lean, I've learned a lot! Most "Lean/Mathlib" talks are about what people have managed to prove, not really how they got from one line to the next, what their "tricks" were for finding the right theorem names, or big picture approaches, etc. By contrast, I've sat through thousands of hours of mathematicians explaining how such and such theory is built, and working through explicit examples... I keep thinking that more people should just be posting their Lean sessions to YouTube; I think that would be more valuable than how it sounds... (I tried to do a (very) little bit of that, e.g., here, it would be great to have more...)

[Brendan Seamas Murphy]

I did this with someone a while ago, pair programming in lean 3 https://youtu.be/L6gTyG31QvY?si=-w-BAdWQf15QsG1u

[Kevin Buzzard]

Usually we don't encourage discussions of announcements in #announce , perhaps this discussion should be moved to #general by someone who can do that sort of thing (Edit: thanks Rob!)

[Notification Bot]

6 messages were moved here from #announce > Seeking Lean users for an observation study by Rob Lewis.

[Bolton Bailey]

Alex Kontorovich said:

... I keep thinking that more people should just be posting their Lean sessions to YouTube

Between prerecorded videos and livestreams, I have around 48 hours of recorded Lean programming on my YouTube channel, @BENJAMIN PIERCE should feel free to use it for his study if he thinks it's of a suitable format to study.