Archive for the ‘mathematics’ Category

FOM discussion

October 25, 2014

There is a very interesting discussion about formalized mathematics going on the Foundations of Mathematics mailing list. The most interesting part of it (at least to me) is the thread about relative merits of Homotopy Type Theory (HoTT) and set theory (ZFC) as foundations for formalized mathematics. I should probably write what is Homotopy Type Theory here, but since I know very little about it this is too much risk to say something stupid, so I suggest that interested readers have a look at the above link, or read at least the abstract of the recent article about this in the Bulletin of the American Mathematical Society. Replacing ZFC with HoTT as standard foundation for mathematics is an idea of Vladimir Voevodsky – a Fields Medalist from 2002. The main argument for the idea is that it is easier to create research level formalized mathematics (in a proof assistant) when the foundation is HoTT than when foundation is set theory.  So the story is interesting from this perspective – that a prominent mathematician is using a proof assistant (COQ) for research and that ease of formalization is an argument for some mathematical idea – for the first time, to my knowledge.

I am not really convinced by the discussion on FOM that HoTT is “better” than ZFC in any universal sense. To me it looks rather that HoTT approaches the body of mathematics from a different side, figuratively speaking. This puts certain areas with active research (some subjects in algebraic topology) closer to foundations and therefore makes them easier to formalize, but at the cost other areas being put farther away. It is not obvious that this trade off is worth abandoning the whole traditional style of doing (even informal) mathematics which is very set theory oriented.

There have been some quite amusing moments in the discussion. One participant, rather sceptical to formalized mathematics posed the following question:

Here is a very simple statement which I often give to students as a first exercise in iteration, and to practice formal mathematics.

Let f be a real-valued function on the real line, such that f(x)>x for all x.
Let x_0 be a real number, and define the sequence (x_n) recursively by x_{n+1} := f(x_n). Then x_n diverges to infinity.

What effort would be required to formalize this kind of statement using current technology?

The funny thing here is that the statement is false. To see this, just take any sequence x:\mathbb{N}\rightarrow\mathbb{R} that is increasing and bounded and for any y\in \mathbb{R} define f(y) = x_{x^-1(y)+1} if y\in x(\mathbb{N}) and, say f(y) = y+1 otherwise. Then we have x_{n+1} = f(x_n) and f(y)>y for all y\in\mathbb{R}, but we have chosen the sequence x to be bounded…

This was used by some to point out usefulness of checking proofs by a machine, which would catch a mistake like this. Freek Wiedijk was polite enough to add the missing assumption about continuity of f and provided a HOL Light verification script for a similar (but true) theorem. That didn’t work too well: Harvey Frieman called that script a “totally unacceptable ugly piece of disgusting garbage”. I think that was a bit too harsh – the second version written using Freek’s declarative miz3 language for HOL Light didn’t look that bad.

Isabelle/ZF on which IsarMathLib is based was mentioned in the discussion once – but only to say that it “hardly has any users”. Well, that was better than calling me “nobody” (as in “nobody uses it”) that I have seen before.

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


Isabelle 2009-1 and IsarMathLib

December 5, 2009

The Isabelle team has just released Isabelle 2009-1. The latest release 1.6.9 of IsarMathLib checks out without any modification, so there is no update needed.

The new installation instructions on the Isabelle web site and the bundle file that can be downloaded from there are specific for Isabelle/HOL. To install Isabelle/ZF for IsarMathLib on x86 Linux one needs to download Isabelle2009-1.tar.gz, polyml-5.3.0.tar.gz,  ProofGeneral- and ZF_x86-linux.tar.gz and do tar -C /usr/local -xzf on each of them. The installation can be finished by running

./bin/isabelle install -p /usr/local/bin

from /usr/local/Isabelle2009-1.

Markov chains – simulation

August 1, 2009

I have to say it took me considerable effort to figure out how to use the part of Haskell’s probability library that deals with randomness and simulation. The intuition developed by programming in imperative languages is especially harmful here. (more…)

Probability monad

May 31, 2009

My favourite programming language Haskell has a nice library for doing calculations with probablility distributions, called probability.
The library was originally written by Martin Ewig and Steve Kollmansberger and then extended and packaged for convenient installation by Henning Thieleman. Its main idea for the implementation is to use the fact that “probability distributions form a monad” (from a paper by the authors of the library ). This post aims at translating this claim into standard probability notation and showing how it is used in the library. (more…)

Interval arithmetic in groups – pass 2

March 1, 2009

This is a continuation of the Interval arithmetics in groups: Pass 1 post.

Let f: \mathcal{V}\times\mathcal{V} \rightarrow \mathcal{V} be a binary operation on a set \mathcal{V}. We will write this operation additively as f\langle x,y \rangle = x + y. Such operation defines another binary operation f^\mathcal{P} on on the powerset \mathcal{P}(\mathcal{V}) (set of subsets) of \mathcal{V} in a natural way: f^\mathcal{P} \langle X, Y \rangle = \{ x + y | x\in X, y\in Y\} for X,Y \subseteq \mathcal{V}.  The nice thing about f^\mathcal{P} is that it inherits interesting properties of f: if f is commutative, then so is f^\mathcal{P}, if ( \mathcal{V},f) is a semigroup, then (\mathcal{P}( \mathcal{V}), f^\mathcal{P}) is also a semigroup, if ( \mathcal{V},f) is a monoid, then (\mathcal{P}( \mathcal{V}), f^\mathcal{P}) is also a monoid, if ( \mathcal{V},f) is a group. then … well, never mind, we don’t need that anyway.

This means that all theorems about adding finite (indexed) collections of semigroup elements (and there are quite a couple in the Semigroup_ZF theory) can be reused for the operation on subsets of \mathcal{V} at little additional cost.

The setup for adding group subsets in the Gyula Lakos’s paper is different in that it assumes the existence of neutral element and defines how to add an infinite number of subsets of \mathcal{V}.

b.) More generally, suppose \{ A_\lambda \}_{\lambda \in \Lambda} is a countable indexed family of subsets of \mathcal{V}. Assume that 0 \in A_\lambda for all \lambda \in  \Lambda except for finitely many. Only in that case we define the algebraic sum \sum_{\lambda \in \Lambda } A_\lambda as \{ \sum_{\lambda \in \Lambda } a_\lambda : a_\lambda \in A_\lambda , a_\lambda = 0 \text{ for all } \lambda  \in \Lambda except for finitely many \}.

We can do something in that spirit for f^\mathcal{P} as well. Namely suppose that
(\mathcal{V}, f) is a monoid and A: \Lambda \rightarrow  \mathcal{P}(\mathcal{V}) is a an indexed collection of subsets of \mathcal{V} such that all but finitely many contain the neutral element (denoted 0). We can split the index set  \Lambda into two subsets, one called \Lambda_0 consisting of those \lambda\in \Lambda for which A_\lambda contains the neutral element, and the rest. Then we can define the sum of the family \lambda \mapsto A_\lambda of subsets of \mathcal (V) as follows:

\sum_{\lambda \in \Lambda} A_\lambda := \left(\sum_{\lambda \in \Lambda \setminus \Lambda_0} A_\lambda\right) + \left(\bigcup_{F \in Fin\mathcal{P}(\Lambda_0)} \sum_{\lambda \in F} A_\lambda\right),

where Fin\mathcal{P}(\Lambda_0) is the set of finite nonempty subsets of \Lambda_0 and +, \sum are interpreted as the additive notation for f^\mathcal{P}. So what we do is we add all sets that do not contain 0, but for sets that do contain 0 we sum every finite subcollection and take the union of all sums obtained this way.

This nicely generalizes the concept of adding finite collections of sets of semigroups (where the \Lambda_0 is empty and there is only the first component of the sum above) and (in contrast to the Lakos’ approach) does not require selecting monoid elements from infinite collections of subsets of \mathcal{V}, i.e. does not require the axiom of choice.

Interval arithmetic in groups: Pass 1

December 6, 2008

Gyula Lakos’s paper that I plan to formalize for IsarMathLib uses a natural generalization of interval arithmetic to abelian group setting. In this post I will go over section 2.A “Algebraic sums” in this paper, quoting it as needed and tell how I want to formalize the notions defined there.


1/0 = 0, really!

October 14, 2008

Let (K, +, \cdot ) be a field. We can define division as a function in K\times  K\setminus  \{ 0\} \rightarrow K in the obvious way. Now, what is the value of that function on the pair \langle 1, 0\rangle? In general, what is f(x) if f : X \rightarrow Y and x\notin X? Is it undefined? How do we define “undefined” ? Surprisingly, in ZF f(x) = \emptyset in such case. In Isabelle/ZF this is lemma apply_0 in func.thy theory. Metamath also proves this as Theorem ndmfv. To see why this is true, look at the Metamath’s definition of the value of function at a point and think what happens when F“{A} there is empty.

So 1/0 = \emptyset because the pair \langle 1,0 \rangle is not in the domain of division. Why then we can write 1/0 = 0? We are cheating a bit here. In ZF set theory the empty set and the zero of natural numbers are the same thing. So really 1/0 = 0, but the zeros on both sides denote different things.