Posts Tagged ‘formalized mathematics’


July 30, 2014

Mathgate declares its purpose as a “website for learning logic and mathematics through formal proofs”. The author and owner of Mathgate is Chad E. Brown, who is also the author of Satallax – an automated theorem prover which has won a a couple of times on the CADE ATP Systems Competition. Mathgate is powered by a different prover, however, which is described as follows:



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.


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


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.

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 Russian) 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. (more…)

Recently read

January 26, 2012

I haven’t updated this blog for a while, so I decided to try to break the writer’s block by posting a couple of quotes from the formalized mathematics stuff I read recently. (more…)

The next generation of proof assistants: ten questions

November 17, 2010

Checking for new stuff on Freek Wiedijk’s home page I stumbled upon slides of his recent talk given at the Workshop on Logical and Semantic Frameworks in Natal, Brasil. He poses there ten questions about how the next generation of proof assistants should look like. In this post I want to give my answers to those questions.

Should the next generation of proof assistants be based on ZFC set theory?


Gödel, Chaitin and formalized mathematics

March 23, 2010

The subject of formalized mathematics has shown up in Slashdot discussions a couple of times. Every time that happened someone mentioned Gödel inconsistence theorems and from that point on much of the discussion concentrated on how Gödel results imply (or not) that formalized mathematics is impossible, impractical or useless.

When I see a discussion like this I think how some seventy years ago a similar forum would discuss the idea that it would be possible and useful to do away with human computers and use machines to execute algorithms. There would be similar arguments about how you could not do that because to execute an algorithm one has to understand it first and machines can not uderstand anything. The art of designing algorithms would lose its beauty when the algorithms would have to be written in a machine language. And, due to a deep theoretical result called the “halting problem” we would have no way to know in advance if such algorithm would ever stop to produce a useful result.

It is easy to dismiss  Slasdot discussions and blame them on the general cluessness of the Slashdot crowd. However, I recently stumbled upon the text of a talk given by Chaitin at the University of Cordoba in November last year that completely puzzled me. (more…)