## Archive for the ‘news’ Category

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

Tags:IsarMathLib releases

Posted in announcements, news | Leave a Comment »

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.

Tags:Coq, formalized mathematics, proof market

Posted in news | Leave a Comment »

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 is continuous in the natural topology on the space of -element sequences of a topological group.

Tags:IsarMathLib releases

Posted in announcements, IsarMathLib releases, news | Leave a Comment »

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:

Here, is the collection of neighborhoods of zero (sets whose interior contains the neutral element of the group), and for two sets we define as .

(more…)

Tags:Haskell, IsarMathLib, IsarMathLib releases, topology

Posted in Haskell, IsarMathLib releases, news | 22 Comments »

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

Tags:HLM, I3P, Isabelle, IsarMathLib, jEdit, Metamath, ProofPower, ZPC

Posted in announcements, news | Leave a Comment »

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.

Tags:I3P, Isabelle interface, ProofGeneral

Posted in news, reviews | Leave a Comment »