Discussion of "Human factors of Lean"

Stream: general

[Kim Morrison]

@Will Crichton, I like your suggestions for the interface. Please open issues and PRs! :-)

[Notification Bot]

A message was moved here from #announce > Human factors of Lean by Kim Morrison.

[Kim Morrison]

Regarding the later point in your talk about looking for theorems:

import Mathlib

example (a b : Rat) (h : 0 ≤ b) : a ≤ a + b := by exact? -- suggests the right lemma
example (a b : Rat) (h : 0 ≤ b) : a ≤ a + b := by hint --  but this suggests the right tactic!
example (a b : Rat) (h : 0 ≤ b) : a ≤ a + b := by linarith

(An audience member (Cody?) had suggested that you use "ring or lia", and "lia" was on the right track: it's the Coq equivalent of linarith.)

hint is already pretty useful, but I would love to see someone work on making it better!

[Iocta]

As a novice Lean learner I found everything in this talk extremely relatable. I hope the lessons are heeded.

[𝚠𝚘𝚓𝚌𝚒𝚎𝚌𝚑 𝚗𝚊𝚠𝚛𝚘𝚌𝚔𝚒]

Nice talk @Will Crichton! I have two comments:

• (~10min) Most of your UI suggestions for the Natural Number Game seem like clear improvements, e.g. not showing locked tactics/lemmas. The one I am not sure about is hiding lemma names entirely and replacing them by their types. This is because mathlib has a very rigid naming convention, and in practice experienced mathlib users know this well enough to be able to guess theorem names without looking them up. One might question the sensibility of this practice, but insofar as it is established right now, you might want understanding the convention to be one of the learning outcomes of NNG, in which case you do want to show theorem names as well (though I agree that the types could be displayed more prominently than one-click-away).
• (~40min) Regarding the reification of information visualization principles into algorithms that produce the tactic state display shown in the infoview, while the order of local assumptions is partly chronological, it is also constrained by dependency order. That is, assumptions which don't depend on each other tend to be ordered by whichever-came-first (and could be moved past each other for purposes of information grouping), but you cannot move an assumption that depends on another one before that one; or rather, you could, but it might be quite confusing to see h : SomeProperty r appear first and then r : SomeType appear later.

[Will Crichton]

Wojciech Nawrocki said:

I have two comments: [...]

Agreed that it's worthwhile to teach the naming convention. Fwiw, using my proposed interface, learners would still see the names of the theorems when they appear in the editor. But it's worth trying an interface where both the theorem name and abbreviated definition are visible in the toolbox, if it doesn't consume too much space.

Personally, I don't think presenting assumptions out of dependency order would be that confusing. The important thing is that the interface affords finding the definition of a local variable referenced in an assumption.

[Will Crichton]

Kim Morrison said:

Regarding the later point in your talk about looking for theorems: [...]

Thanks for the pointers. After some investigating, I realized why I didn't end up using linarith in the context of the theorem -- because it doesn't seem to handle certain type conversions yet! Unless someone knows what I'm doing wrong here: #new members > linarith w/ NNRat

[Will Crichton]

Although notably the step I discuss in the talk (subtracting from both sides) can be expressed using a verbose suffices clause:

example {a b c d e f : ℚ} {g h : NNRat}
  (h1 : 0 ≤ c + d)
  (h2 : 0 ≤ e + f)
  : a + b ≤ a + b + c + d + e + f + g + h := by
  suffices _ : 0 ≤ c + d + e + f + g + h by
    linarith
  sorry

Playground link.

[Anand Rao Tadipatri]

An alternative to sorting the hypotheses in the local context might be highlighting the sub-terms in the context that match an expression selected by the user. This would have the advantages of preserving the chronological and dependency order and (possibly) being easier to compute.

[David Michael Roberts]

@Will Crichton On the slide "Calls to action", what is HCI? It wasn't explained verbally, that I heard.

[Daniel Weber]

I believe it's human-computer interface

[Miguel Marco]

I also found the talk very interesting, and definitely agree on the idea of hiding the locked items in the inventor: it not only shows the interface less cluttered, but could also add an extra satisfaction to see how your inventory grows as you advance the game.

And about showing the type of the theorems vs their name... what if we show the names, but the type appears when you hover the cursor over them?

And about theorem discovery, maybe the vscode extension could have a small window for that? That is: a small box that says "type a simple statement here to search for a theorem in the library that proves it", and when you type something there, exact? is called under the hood and the result is displayed.

[Will Crichton]

David Michael Roberts said:

On the slide "Calls to action", what is HCI? It wasn't explained verbally, that I heard.

Ah sorry, too much jargon. HCI is "human-computer interaction" and it refers to a subfield of CS research that you find at places like UIST and CHI. Generally speaking, most people who do "human-centered X" research where X is a computing topic will publish in HCI.

Miguel Marco said:

And about showing the type of the theorems vs their name... what if we show the names, but the type appears when you hover the cursor over them?

This would be an improvement over the current interface, but I would still strongly prefer showing the types by default. The tooltip approach still requires a user to hover over each theorem in sequence in order to find the right theorem.

And about theorem discovery, maybe the vscode extension could have a small window for that? That is: a small box that says "type a simple statement here to search for a theorem in the library that proves it", and when you type something there, exact? is called under the hood and the result is displayed.

Yes, I think something like this would be a great first step towards a "discovery toolbox".

[Yury G. Kudryashov]

Loogle.?

[Will Crichton]

Yep! Search tools like Loogle & Moogle should also be part of that toolbox. And that toolbox ought to be integrated into the Lean toolchain, e.g. the goal pane.

[Johan Commelin]

@Will Crichton I only got around to watching your talk now, but I'm really glad I did. This is a very cool topic, and you're POV on this topic is much appreciated!

[Johan Commelin]

I really like your first call to action, but (being a complete novice) I would love to get some concrete pointers into the literature. Are there some books, intros, overviews that you would strongly recommend reading besides the references that you already put in your talk?

[Johan Commelin]

Also, are your slides available somewhere? (Sorry if I missed a link that was already posted.)

[Will Crichton]

@Johan Commelin this was discussed a bit in the question section, but I can give links here. If you were only going to read one book, I would recommend:

Things That Make Us Smart, Don Norman, 1994

He also has a more widely-known book The Design of Everyday Things which is also great, but IMO it's less applicable to stuff like proof assistants.

For a deep dive, some more recommendations:

• Engineering Psychology and Human Performance: focuses on designing "mission-critical" components like vehicle interfaces or airport control systems.
• Information Visualization: Perception for Design: focuses on the relationship between human perception and utilities like charts or 3D visualizations
• How People Learn 1 and How People Learn 2: summary of actionable insights in learning science.
• Psychology of Programming: survey of research on how people program. Older book (1990), but still reasonably authoritative since not much work has been done in this vein since.
• The Programmer's Brain: a modern synthesis of programming psychology research that focuses on applications to an individual's programming practice.

Slides haven't been posted, I'll see if Topos can put them up.

[Julian Berman]

This is likely further off-topic but have you seen / do you have an opinion on this *In Their Own Words* book? (Or even more specifically do you have any of its chapters you particularly would recommend, I picked a few and wasn't immediately hooked even though it came heavily recommended by someone else.)

[Will Crichton]

@Julian Berman I haven't read that book specifically. Glancing at the contents, a few thoughts. These kinds of academic handbooks where researchers contribute individual chapters are necessarily chaotic. They resemble conference proceedings more than a coherent book. The chapters look good, but I doubt this book is best as a first-time introduction to these concepts. I would recommend a more holistically-designed book such as How People Learn (linked above), or The ABCs of How We Learn.

Learning is complicated, and so learning science is less developed than e.g. information visualization. On average, we just have less useful rigorously-validated knowledge about learning. Following "Delivering Cognitive Psychology to HCI", I find that learning science is most useful when it gives me concepts/vocabulary for thinking more deeply/precisely about learning and pedagogy. For example: conceptual metaphors, contrasting cases, concept inventories, item response theory, perceptual learning modules.

[Julian Berman]

I find that learning science is most useful when it gives me concepts/vocabulary for thinking more deeply/precisely about learning and pedagogy.

This is extra difficult for me as someone not in the field, I find... It's hard to turn off the part of the brain that says "well yes but I have no intuition for whether the concept is applicable relative to other things". I think you touched on something which referenced this in your talk when talking about how studies are usually about broccoli :) or something thereabouts.

But for instance, I found it hard not to be distracted when you proposed hiding theorem names in NNG by "it seems not obvious to me whether that might improve how fluidly someone moves through NNG but then perhaps they come out less familiar with the naming convention, which it seems like the NNG is trying to teach as a hidden skill by showing those"

[Julian Berman]

(I don't know what I'm asking -- but I guess I find it hard to trust any concept I learn without just wishing someone measured it in the specific case we care about)

[Julian Berman]

(And thanks for the extra links! Which I obviously haven't managed to digest yet.)

[Will Crichton]

Totally. That's why it's good to learn from psychology in two ways:

1. Gather ideas that inspire you to build new things, or design existing things in new ways.
2. Gather methods that empower you to evaluate the things you're building.

The latter is essential for testing whether ideas successfully transfer out of their original context and into yours. In the NNG case, I agree that hiding theorem names by default will probably impact a learner's ultimate understanding of Lean naming conventions. (I addressed this a bit earlier.) I intuitively believe that trade-off is worth it, but that's an empirical question which could be evaluated.

More broadly, any sufficiently complex artifact (Lean, NNG, etc.) is built out of thousands or even millions of tiny design decisions. You never get to rigorously explore the design space for every decision. The best you can do is sway your priors in a direction you hope is productive!

[Jon Eugster]

Thanks for the talk and the suggestions @Will Crichton! In terms of communication it would be really nice if you actively communicated your analysis and suggestions with the relevant parties, i.e. for the Lean environment, start Zulip topics about individual things or write on the relevant github repos, which are all open-source and should almost all be directly linked from the tool itself. It's somewhat unusual to be told by a third party to go watch a video when the suggestions (in particular the ones about the NNG) could basically be a one-sentence feature request each.

The suggestions are very valid though and certainly apprechiated!

One comment on the "locked tactics": originally they weren't displayed (as you suggest) and then it's been decided to add them as to convey the user's progress as they play. So having a github issue about how they negatively impact the learning experience would be useful in order to bring this up again for discussion! Working with colour might also address some of the concerns:

Screenshot_20240826_203438.png

Btw (especially @Kevin Buzzard as the authour of NNG) changing the theorem names in the NNG from names like add_comm to something like a + _ = _ + a is something the game author could just do, these names are specified manually in the game. I'm not sure it's the right thing for NNG... But other games might find this a valid option!

Miguel Marco said:

what if we show the names, but the type appears when you hover the cursor over them?

I already implemented exactly this a while ago! :blush: (just hasn't been released yet, but you can sneak peak at the in-development version!)

[Will Crichton]

Hi @Jon Eugster, to be clear, I'm not trying to launder my feature requests through the Topos Institute, and I'm sorry if someone forwarded the talk to you as if that were the intent. The primary goal of the talk is to use these suggestions as a lens by which to understand the general principles of human-centered design. I specifically didn't file feature requests because the ideas are all preliminary / underspecified, and in my experience in open source, it can be annoying to have people raise extremely broad suggestions that pollute your Github issues. (But I am happy to file feature requests if you'd like!)

Re: locked tactics, it makes sense why they are there. It's important to observe I am taking a strictly utilitarian approach in my suggestions, which doesn't really consider the affective components of design decisions (e.g., fun, satisfaction, anticipation, etc.). It's also valid to say "we're going to do something that trades-off utility for fun."

[Jon Eugster]

I definitely get that and your talk was covering some nice aspects about human-centered design!

Staying on the little details, I do have a question about the infoview sorting you briefly mentioned. In NNG for example we already do some custom sorting into "Objects" (Type-valued hyps.) and "Assumptions" (Prop-valued" hyps.). You mentioned syntactic distance. How would that concretely look like given that one has basically only one dimension to work with?

[Will Crichton]

If you have a similarity metric between pairs of propositions, then you could do something like spectral ordering to create a sort from the similarity matrix. Better yet, you could use a math-tuned language model to generate embeddings for each proposition and then sort them based on the embedding space. But that would be more involved and computationally intensive.