October 26, 2012

One thing that I like working for my company is that it tries to evaluate new technologies from time to time. About a year ago I got a task to learn Scala by writing a small internally used tool in it and share my impressions. The main question I was supposed to answer was: “Should we use Scala (instead of Java) to implement the next iteration of one of our products?”.  I had a feeling that my boss would have liked me to answer enthusiastically “yes!” to that question. And I really liked the language. However, my answer was “probably not”.

Read the rest of this entry »


IsarMathLib 1.7.5

October 9, 2012

The 1.7.5 version of IsarMathLib has been released. The new formal math there consists of two theory files contributed by Daniel de la Concepción Sáez with over 70 theorems about various examples of topological spaces.

Installing Isabelle

September 17, 2012

I am recovering from a hardware failure that resulted in the loss of my encrypted home partition, so I had to install Isabelle. Here are quick notes on what is needed on Ubuntu 12.04.

1. Download Isabelle. The installation is just unpacking to the directory of your choice, I unpacked it to ~/bin. That created a directory ~/bin/Isabelle2012.

2. Edit ~/bin/Isabelle2012/etc/settings file to change the default logic to ISABELLE_LOGIC=ZF.

3. Run “build ZF” in the ~/bin/Isabelle2012 directory. This builds the ZF heap image. Isabelle ships with only HOL image precompiled.

4. Install openjdk-6-jre, texlive-latex-base and texlive-latex-extra packages. It’s the first time I am using openjdk instead of Sun Java, but so far I haven’t noticed any issues. The texlive-latex-extra package is for comment.sty file that is needed for LaTeX processing of proof documents.

5. Start Isabelle jEdit interface with  ~/bin/Isabelle2012/bin/isabelle jedit and correct the font size in Utilities/Global Options/jEdit/Text Area/Text font. Isabelle ships with the font size 18.

That’s pretty much all that is needed to have Isabelle ready for IsarMathLib contributions.

Update Aug 10th 2012: Turns out installing Java is not necessary as the bundle already contains a suitable JDK.

The Russell proof language

August 19, 2012

I have thought for a long time that it would be nice to have a high-level proof language with a prover that would compile that to an easy to verify and still readable low level language. A good candidate for the low-level part would be Metamath. I have recently found out about Russel – a high-level proof language created by Dmitri Yurievich Vlasov that compiles to (a simplified version of) Metamath. The Russell project on Sourceforge was last updated in February 2011, so it seems to be unused and abandoned. There is a paper (in Russian) that describes Russell. Unfortunately I don’t have access to the journal where it was published.

Read the rest of this entry »

IsarMathLib 1.7.4

June 30, 2012

I have released version 1.7.4 of IsarMathLib. The new formal math there is a mostly in the Topology_ZF_3 theory about  topologies on function spaces. This is needed to show that the function (x_0, x_1, ..., x_{n-1}) \mapsto \sum_{i=0}^{n-1}x_i is continuous on G^n where (G,+) is a topological group. This will be my goal for the next release. Read the rest of this entry »

Recently read

January 26, 2012

I haven’t updated this blog for a while, so I decided to try to break the writer’s block by posting a couple of quotes from the formalized mathematics stuff I read recently. Read the rest of this entry »

IsarMathLib 1.7.2

July 20, 2011

I have released a new version of IsarMathLib. It adds about 50 new lemmas, mostly in group theory and topology, leading to the following characterization of closure in topological groups:

\overline{A} = \bigcap_{H\in \mathcal{N}_0} A+H

Here, \mathcal{N}_0 is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets A,B\subseteq G we define A+B as A+B=\{a+b | a\in A, b\in B\}.

Read the rest of this entry »

IsarMathLib 1.7.1

May 13, 2011

I have released version 1.7.1 of IsarMathLib. There are two small topics I added, both in the “weird math” category.
The first is related to the “1/0=0” story that I talk about in another post. Proving the theorem that states that was a little bit more involved that I had thought. I had to define the notion of division in fields as a function on K\times K\setminus \{0\}, then notation for it. I don’t think I cheated here but the truth is I did make an effort to make the theorem look like the one I wanted to prove. This brings up the question: what if I made a little more effort and manipulate notation so that a theorem appears to mean something different that it really does? For example it is quite easy in Isabelle to change the notation to print “True” as “False” and prove a theorem that appears to show inconsistency in ZF.
Freek Wiedijk’s paper formalizes this question. Back in January there was also a long thread on the Isabelle mailing list where people expressed varying opinions on how serious the problem is.

Another small piece of formal math that I added in this release is a chapter in the Topology_ZF_2 theory on the pasting lemma. The classical pasting lemma states that if we have two topological spaces, say (X_1,\tau_1) and (X_2,\tau_2) and we partition X_1 into two sets U,V\subseteq X_1, \ U\cup V=X_1, both open (or both closed), and a function f:X_1\rightarrow X_2 is continuous on both U and V, then f is continuous. The version in IsarMathLib is bit different, stating that the collection of open sets \{U \in \tau_1 : f|_U \text{is continuous}\} forms a topology.
Surprisingly from this we can conclude that the empty set (which in ZF is the same as zero of natural numbers) is continuous. Here is how it happens: since the collection \{U \in \tau_1 : f|_U \text{is continuous}\} forms a topology, \emptyset belongs to it, i.e. f|_\emptyset is continuous. But f|_\emptyset is in fact \emptyset and we get that zero is continuous. Ha Ha.
I would like to emphasize that I do not consider facts like this as demonstrating that ZF set theory is not a suitable foundation for formalizing mathematics (as some people interpret). It is just fun and games that formal math allows and I am sure other foundations also have their unintuitive corner cases.

The first formalized math wiki is here

April 13, 2011

I have been wondering for a couple of years who will be the first in the race to set up a a publicly available, working and usable formalized math wiki. Now ladies and gentlemen we have the winner and the winner is!

Read the rest of this entry »

Isabelle2011, IsarMathLib 1.7.0 and other news

February 19, 2011

Isabelle team has released Isabelle 2011. The upgrade was not as smooth for me as the previous one. The new ProofGeneral didn’t work with Xemacs shipped with Ubuntu 9.10, giving a “file mode specification error”. I tried then the new jEdit interface that found that ZF logic is missing. Indeed, the Linux bundle does not contain precompiled ZF logic. It was not a big problem, I built it with “build ZF”.

The jEdit interface  (see the screenshot)  represents a new approach based on “continuous proving” concept. While I think it is very interesting technologically, it turned out extremely slow on my Athlon 64 1.8GHz with ony 512MB of RAM. Apparently all this proving in the background with keeping multiple versions of the document was just too much. It would be usable if it was possible to temporarily disable the continuous proving feature, but unfortunately this is not supported yet.

Read the rest of this entry »