Conor Titania Mc Bride2d ago

So here's a thing.

The proof assistants we need for professionals advancing the frontiers of our understanding are not the proof assistants we need in the education of our youngsters.

The feedback they need and can have is wildly different.

I want to contribute to both projects, but perhaps I can help by observing that they're not the same project.

Show threadterru2d ago
@pigworker attempted to teach students how Isabelle works recently. Ran into trouble: “by simp” can do (almost) all the proofs in introductory things. how convenient! but nothing is learnt … 🙈
Show threadConor Titania Mc Bride
@stuebinm I can see how that's frustrating. My gadgets are both too stupid and too clever. It's worth thinking about how to adapt.
Mar 27 at 10:35pmWeb