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 threadConor Titania Mc Bride
In particular, the professionals tend to work solo, or in tight teams, solving problems they hope are fresh. In education-land, the weans are getting to grips with old chestnuts, so there are more interesting ways to address failed proof attempts, in a cohort.
Mar 27 at 10:12pmWeb
Show threadPhilippa Cowderoy2d ago
@pigworker Amongst other things, that sounds like something you could legitimately throw machine learning techniques at over time! Though any chatbot-like UI should have clear indications of being "ELIZA with domain expertise and a log"...