Archive for the ‘news’ Category

FMM 2018 and IsarMathLib release 1.9.7

August 26, 2018

I gave a talk on IsarMathLib at the Third workshop on Formal Mathematics for Mathematicians (FMM 2018) on August 13. The workshop was part of 11th Conference on Intelligent Computer Mathematics (CICM 2018). The slides for my talk are available online on the CCIM page. The paper (an “extended abstract”) can be also found there, but they somehow cut the pictures from it, so it’s better to look at the original.

In other news I updated IsarMathLib to Isabelle 2018 which was released about a week ago.

Advertisements

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

 

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…)