Last year I participated in a project whose goal was to record at low cost my lectures on video and put them on-line. Since the most expensive parts of recording are having a camera man and manual post production, we set up a static camera and just uploaded raw video online at videolectures.net. As you can see for yourself, the sound is good (I wore a microphone) but the whiteboard is mostly illegible. In addition, it took about two weeks for the lectures to show up on-line because there were men-in-the-middle. So that got me thinking whether there was a better way.

Continue reading Video lectures as screencasts

# Category Archives: General

# Video tutorials for the Coq proof assistant

Next week I am going to a meeting where I am supposed to give a tutorial on the Coq proof assistant. Inspired by the Catsters, I decided to prepare the material in the form of screencasts. You can find the first few tutorials on Youtube in my “Coq tutorials” playlist. So far I have:

- Obtaining and installing the Coq proof assistant
- How to use CoqIDE
- How to use Coq with Proof General
- A first proof with Coq (Frobenius rule)
- The dual Frobenius rule, part 1
- The dual Frobenius rule, part 2
- Currying and uncurrying, part 1
- Currying and uncurrying, part 2

You should turn on the high quality HD stream when you watch these. Feedback is welcome (and easy to provide on Youtube). I find it very, very difficult to listen to my own voice. I hope to have many more lectures soon, but I am starting to feel out of my depth, so if anyone wants to help they are welcome!

Continue reading Video tutorials for the Coq proof assistant

# Subgroups are equalizers, constructively?

[**Edit 2010-11-12: **Given the gap in my “proof”, I am changing the title of the post to a question.]

I would like to record the following fact, which is hard to find on the internet: *every subgroup is an equalizer, constructively*. In other words, all monos in the category of groups are regular, constructively. It is interesting that this fact fails if we work in a meta-theory with “poor quotients”.

# A new style for the blog

It was time I changed the old blog style to something a bit more modern. I hope you like it.

Now I just have to figure out how to port 60 blog posts from ASCIIMathML notation to something a bit friendlier that can use MathML but does not require it. What is out there? I know about jsMath. I am open to suggestions.

# Constructive gem: irrational to the power of irrational that is rational

The following argument is often cited as an example of the necessity of the law of excluded middle and classical logic. We are supposed to demonstrate the existence of two irrational numbers $a$ and $b$ such that their power $a^b$ is rational. By the law of excluded middle, $\sqrt{2}^{\sqrt{2}}$ is rational or not. If it is rational, take $a = b = \sqrt{2}$, otherwise take $a = \sqrt{2}^{\sqrt{2}}$ and $b = \sqrt{2}$. In either case $a^b$ is rational. Let us think about this for a moment, from constructive point of view.

Continue reading Constructive gem: irrational to the power of irrational that is rational