It seems to me that people think I am a constructive mathematician, or worse a constructivist (a word which carries a certain amount of philosophical stigma). Let me be perfectly clear: it is not decidable whether I am a constructive mathematician.
Continue reading Am I a constructive mathematician?
|
|||||
|
This is an advertisement for two great meetings we are organizing in Ljubljana from June 15 to June 20, 2012: Fourth workshop on formal topology (June 15—19) There are many reasons why you should come: Ljubljana is lovely in June, with many cafes and restaurants on the Ljubljanica river [...] I remember how hard it was to assimilate category theory when I was a student. A beginning student on math.stackexchange.com is asking for a solution to a basic lemma about pullbacks. It really is the sort of thing one should do by oneself. Nevertheless, here it is, in gory [...] 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. 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:
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 [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”. 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 [...] 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 In a recent post I claimed that Python’s lambda construct is broken. This attracted some angry responses by people who thought I was confused about how Python works. Luckily there were also many useful responses from which I learnt. This post is a response to comment 27, which asks me to say more about my calling certain design decisions in Python crazy. I quite like Python for teaching. And people praise it for the |
|||||
|
|
|||||