## Java, Mockito and ArgumentCaptor

September 3, 2013

I knew that day would come at some point. I am programming in Java. One thing that took me longer that I think it should was to figure out how to use Mockito‘s ArgumentCaptor to verify arguments with which methods are called. In this post I share some code snippets that do that, for my reference and hopefully to help other Java beginners.

## IsarMathLib 1.9.0 released

July 26, 2013

I have released version 1.9.0 of IsarMathLib. This is a quite large release with 10 new theory files and 155 new theorems, all contributed by Daniel de la Concepción Sáez. The first of the files contributed by Daniel (released in 1.8.0), Topology_ZF_4 about nets, filters and convergence in topological spaces is now presented on the isarmathlib.org site. The rest of Daniel’s contributions for now can be viewed in the proof document and the outline.

Here is a short description of what is in the new theories:

## Gowers and Ganesalingam

May 12, 2013

There is a series of posts at the Timothy Gowers’s blog about software that can “solve mathematical problems” which he has been working on with Mohan Ganesalingam for the last three years. The word “problems” is used here in the way a mathematician would use it – it’s really about software that can support a mathematician trying to write a proof of a theorem. The goal is for the program to write proofs that look like ones produced by a human. The experiment Gowers sets up on his blog presents several theorems with proofs written by two humans (an undergraduate and a graduate student) and one created by the program and asks the readers to guess which proofs are written  by whom. The results are truly remarkable – while I, and most of the audience, could have a good guess which proof is written by the software, I believe I could guess it only because I had known one of the three proofs was such. If a student submitted such proof as homework to me, I would have no suspicion at all.

## IsarMathLib 1.8.0 released

February 25, 2013

I have released the 1.8.0 version of IsarMathLib. This version works with the new Isabelle2013 (released about two weeks ago). The new material in this release mostly comes from contributions by Daniel de la Concepción Sáez, who added 5 theory files with about a hundred theorems about general topology. The subjects range from convergence of nets and filters and related continuity properties of functions, through some generalized notions of compactness and connectedness, to rather abstract (like, category theory abstract) subjects of heredity and spectra of topological properties. Unfortunately, it will take some time before those theories will be presented on the FormalMath.org site, as my parser is not good enough to parse Daniel’s advanced Isar style.  I will work on this though and in the meantime an interested reader can have a look at the Isabelle generated full proof document or the outline.

As for myself, I have finished the proof that the function $(x_0, x_1,...,x_{n-1})\mapsto \sum_{i=0}^{n-1}x_i$ is continuous in the natural topology on the space of $n$-element sequences of a topological group.

## Scala

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”.

## 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 Russion) that describes Russell. Unfortunately I don’t have access to the journal where it was published.

## 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 »