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 [...]]]> http://math.andrej.com/2010/01/08/a-new-style-for-the-blog/ Already a while ago videolectures.net published this tutorial on Computer Verified Exact Analysis by Bas Spitters and Russell O’Connor from Computability and Complexity in Analysis 2009. I forgot to advertise it, so I am doing this now. It is about an implementation of exact real arithmetic whose correctness has been verified in Coq. Russell also [...]]]> http://math.andrej.com/2010/01/07/tutorial-on-videolecturesnet/ With Davorin Lešnik.

Abstract: We investigate the relationship between the synthetic approach to topology, in which every set is equipped with an intrinsic topology, and constructive theory of metric spaces. We relate the synthetic notion of compactness of Cantor space to Brouwer’s Fan Principle. We show that the intrinsic and metric topologies of complete separable metric [...]]]> http://math.andrej.com/2010/01/06/metric-spaces-in-synthetic-topology-2/ 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 [...]]]> http://math.andrej.com/2009/12/28/constructive-gem-irrational-to-the-power-of-irrational-that-is-rational/ In the last constructive gem we studied the exponential `2^NN` and its isomorphic copies. This time we shall compute the double exponential `2^(2^NN)` and even write some Haskell code.

By `2` we mean the set `{0,1}` of the Boolean values. First note that there is a difference between `(2^2)^NN` and `2^(2^NN)`. The former is isomorphic to [...]]]> http://math.andrej.com/2009/10/12/constructive-gem-double-exponentials/