Archive for the ‘news’ Category

IsarMathLib 1.9.4 and other news

April 17, 2016

I updated IsarMathLib to work with Isabelle 2016 a couple of weeks ago. The distribution and the proof document are available in the usual places.

In other news, back in October 2015 Daniel De La Concepción, an IsarMathLib contributor, published an informal version of some of his contributions in a paper titled “New equivalences to axioms weaker than AC in topology”.

 

Advertisements

ProofPeer

February 1, 2014

ProofPeer is a project to create a cloud-based social network interactive theorem proving system. I wrote about it a year ago. The project looked dormant since about July, but now it got funding and is accepting PhD studentship applications.

(more…)

Proof market

January 11, 2014

Yoichi Hirai has created a site where one can submit bounties for proofs of theorems in Coq formal proof management system.  Currently the bounties are sent to a Bitcoin address that is under the control of the site owner. This requires of course  some trust in the site owner, although reducing the trust requirements is under discussion. I don’t think it is possible to implement a Coq checker in Script though (as Yoichi suggests) as Script is not Turing complete. Something like what is described in the Using external state chapter of the Bitcoin wiki page on contracts is more realistic.

There are currently bounties for proving False (i.e showing inconsistency of Coq) and a couple of theorems that seem quite involved. The funny thing is proving False is also on the list of solved problems. Someone has earned 0.999 BTC by submitting four lines that just change the meaning of False and state a trivial theorem using that changed meaning, thus showing Pollack-inconsistency of Coq.

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.

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

(more…)

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 Wikiproofs.org!

(more…)

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.

(more…)

Goodbye ProofGeneral, again

April 4, 2010

A couple of weeks ago Holger Gast announced the first release of the new interactive interface for Isabelle theorem prover. I was planning to write its review, but I decided not to as Jesus Aransay’s wrote a post on the Isabelle mailing list that  pretty much summarizes what would be in that review.

For me the lack of proper display of mathematical symbols and subscripts is a show stopper. You can’t write mathematics without that. I hope that will be resolved soon and I3P will be an excellent replacement for ProofGeneral.

Formalpedia

June 15, 2009

Formalpedia is an “editable online repository of code and formal math”. It is on its way to become the first formalized mathematics wiki that goes online. (more…)

MathWiki project is hiring

March 10, 2009

Apparently the formalized mathematics project at Radboud University Nijmegen (NL) that I wrote about previously did get some funding after all and they are hiring two people to work on it. The PhD position is for 4 years and the postdoc position is 3 years. I hope that a usable formalized mathematics wiki will be available earlier.

The postdoc position pays a “maximum salary”  of 3755 Euro per month. Such wording immediately makes me curious what is the minimum … .