About increasing the user base. Ocaml has a nice mooc. Did anyone try to copy that to coq?

I guess the obvious choice of MOOC focus would be SF

I think that if somebody was willing to allocate time to creating a MOOC about Coq, @Michael Soegtrop would be happy to provide advice so that this MOOC is accessible to the engineering public that he has in mind.

I would be interested in running such a MOOC personally, but I have so many other things to do that it's not even something I'd put on my todo-list for later.

this could be relevant as well (database of formal methods courses): https://fme-teaching.github.io/#fm-courses

(I have personal doubts about whether the academic community should even be doing MOOCs at all, but am all for producing course materials that can be used for regular courses)

CC @Yves Bertot

It's hard to know if everybody that uses the word MOOC has the same thing in mind. One aspect is to gather training material that contains video material, another aspect is to gather a lot of interested people together, so that they can learn at the same time, benefit from the supervision of teaching assistants on line, but also benefit from enough collaborative rooms where they can learn from each other.

Personally, I tried to develop a video course in 2008. The material spanned over 8 hours of introductory course (cut into bits of at most 15mns) and was used by some colleagues as extra material. As a result, I received some positive feedback (especially because my colleagues complained when the course disappeared from its usual location after a few years). Unfortunately for this audience, this course was in French, but it can still be seen at this location: my video courses about Coq.

I plan to make a few more videos in the next few weeks, but the technology will be different. I will be using OBS this time, and the videos will mostly consist of sessions where I do some exercises live. I hope this can be useful.

On the subject of MOOCs, the top management at Inria has been bugging me to organize something along these lines (and to use some of their infrastructure for that).

erratum, my previous video course in French was actually in 2009.

the most "hip" thing in educational content these days is likely to livestream when working with a proof assistant, I found Kevin Buzzard's Lean numbers game session interesting: https://www.twitch.tv/videos/647824633

Ah ah, I was just writing about that and digging up the related tweet: https://twitter.com/XenaProject/status/1271094301062283266

In just over an hour (5pm UK time, 1600 UTC) I'll be playing through the natural number game https://github.com/ImperialCollegeLondon/natural_number_game live on Twitch https://www.twitch.tv/kbuzzard . Beginners welcome.

- The Xena Project (@XenaProject)Kevin apparently also holds what amounts to regular "office hours" through Discord.

the rage these days is to do "superchats" (audience paying for streamer to answer question or discuss something) - - it would be interesting if the audience asked someone to prove a theorem or verify function on the fly while streaming, not necessarily with money involved

the ideal would be if one also records the lower-level interaction with Coq at the same time as streaming the video, along the lines of what Talia and her colleagues did: http://tlringer.github.io/pdf/analytics.pdf

Karl Palmskog said:

the most "hip" thing in educational content these days is likely to livestream when working with a proof assistant, I found Kevin Buzzard's Lean numbers game session interesting: https://www.twitch.tv/videos/647824633

I heard a gazillion of times that silly proofs about Peano arith would bore mathematicians to death... and now I watch a mathematician teach that... I guess I understand nothing about mathematician ;-)

Enrico Tassi said:

I heard a gazillion of times that silly proofs about Peano arith would bore mathematicians to death... and now I watch a mathematician teach that... I guess I understand nothing about mathematician ;-)

I believe his audience here is math undergrads wanting to do hip stuff in Lean, so I can definitely see that Peano could go over relatively well in that particular context. Plenty of snarky stuff about CS limitations though...

in any case, I think the CS community can be grateful to Kevin for insight into the mindsets of pure mathematicians. For example, I once talked to a pure math PhD, and tried to explain a bit about the Coq odd-order proof... Didn't go well, since in his view, Feit-Thompson wasn't much of a theorem at all, its proof was too decomposed into to many places/papers for his liking. I couldn't really get through about the *concept* of a formal proof at all. Kevin's outline of how proofs in math are "ordained" by their cabal of elders (not his exact words, but the gist) explains a bit of that.

maybe @Rob Lewis can give us some more insight on this

I'm not quite sure which part of the conversation I'm expected to have insight on! I think Kevin has been successful at gamifying things. Instead of writing a tutorial that's trying to teach you something he wrote a game that you try to beat. His streams have a lot of that flavor to them too. Say what you want about the approach but he's certainly found an audience for it.

I'll take the opportunity to ask @Rob Lewis if/when you're going to make a "one-stop-shop" Lean resource/project list like this: https://github.com/coq-community/awesome-coq (getting it listed at https://github.com/sindresorhus/awesome was a real challenge)

We had something like that on our website at some point but it might have gotten lost when the website was redesigned? The mathlib repo + https://leanprover-community.github.io/papers.html + https://leanprover-community.github.io/learn.html pretty much covers it.

I'll investigate where that page went...

I disagree that our list is anything like the union of papers.html + learn.html though...

The list of Lean libraries is [mathlib] plus a few projects that were published. There are no frameworks, one UI, one package/build management system, no plugins, one or two tools. There's not much to populate a list like that.

Last updated: Jun 24 2024 at 14:01 UTC