Lean and Metamath Zero

It seems there is a wave of interest in formalized mathematics among professional mathematicians, driven by a very successful Lean mathlib project. There is a video of Kevin Buzzard’s talk about the project and an arXiv paper describing it. Kevin Buzzard is an algebraic number theorist and a professor of pure mathematics at Imperial College of London. In the summer 2018 he led a summer project with twenty undergraduates that were were learning Lean and formalizing mathematics in it. He also sometime uses Lean live coding while teaching classes and runs a Lean club at Imperial called the Xena Project. His article in the London Mathematical Society newsletter provides more info on this.

Lean is a programming language and software verification tool from Microsoft Research. I think Thomas Hales’ review is the best source on its strengths and weaknesses from the formalized mathematics point of view. Lean’s logic is calculus of inductive constructions (CIC, similar to what Coq is based on). So Lean mathlib formalizes mathematics in (dependent) type theory. Of course  this is a bit unfortunate from my point of view as I am more of a set theory person. There is no doubt though that type theory is nowadays more popular (not to say successful) foundation in formalization efforts. Jeremy Avigad wrote a rare compelling explanation of why this is the case.  I personally prefer the opinion of Lawrence Paulson, the original author of Isabelle and its ZF logic (he also implemented a formalization of ZFC set theory in Isabelle/HOL recently). Here is what he says:

I would guess that the amount of effort and funding going into type theory exceeds the amount that went into set theory by an order of magnitude if not two. It’s not unusual to encounter open hostility to set theory and classical logic combined with an air of moral superiority: “Oh, you aren’t constructive? And you don’t store proof objects? Really?” And I have seen “proof assistant” actually DEFINED as “a software system for doing mathematics in a constructive type theory.

The academic interest simply isn’t there. Consider the huge achievements of the Mizar group and the minimal attention they have received.(…)

I am certain that we would now have highly usable and flexible proof assistants based on some form of axiomatic set theory if this objective had enjoyed half the effort that has gone into type theory-based systems in the past 25 years.

In January 2020 there will be a conference on Formal Methods in Mathematics and Lean in Pittsburgh, Pennsylvania.

Another project related to formalized mathematics that I think is very interesting is Metamath Zero by Mario Carneiro. This is a formal proof verifier, heavily inspired by Metamath, but with a different architecture, some improvements in the metalogic and the ambition to be a “bootstraping theorem prover”, i.e. be able to verify itself. The details are in the arXiv paper, but below is the summary of what I think I understood from it.

Metamath Zero (MM0) separates the specification from the proofs, so there are two inputs to the verifier. The specification is a human readable text written in mm0 language which is as generic as the Metamath language, i.e. it can specify  logics from ZFC on FOL, through Quantum Logic(s), type theories like HOL or CIC, to the Intel x86 instruction set architecture. Anything, really. The proofs are provided separately in a binary whose format (mmb) is optimized for verification speed. This is the format that allowed MM0 to verify the material contained in the Metamath’s set.mm with its 23000 proofs in 195 ms on Intel i7 3.9GHz (the previous record was 0.7s). This part of the architecture can serve as independent backend of any theorem prover that is able to provide the mm0 specification and mmb proof binary.

An example of such theorem prover is included in the MM0 system, together with a proof language mm1 (similar to mm0) and an formal text authoring tool as a Visual Studio Code plugin implementing Language Server Protocol.

I don’t want to write about the MM0 metalogic as there is too much risk to say something wrong here. I only want to mention that the paper contains a very clear explanation of Tarski-Megill metalogic (used by Metamath) that replaces the notion of free and bound variables by the notion of distinct variable groups.

The bootstraping goal which I understand is work in progress consists of specifying Peano Arithmetic, then x86 instruction set architecture and the formal system of MM0 to get a complete specification of the working of the ELF binary file that executes the verifier.

Advertisement

FOM discussion

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 that is increasing and bounded and for any define if and, say otherwise. Then we have and for all , but we have chosen the sequence 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 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.

Mathgate

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:

ProofPeer

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.

Bitcoin epic fails

Bitcoin, or more generally cryptocurrencies  is  a somewhat complex subject in that it connects technology, economics and law. But it is kind of fashionable now, so some famous people decide to publicly formulate opinions about it without devoting time and effort to gain knowledge about how the technology actually works. As one commenter on the Marginal Revolution site nicely put it:

The situation has all the makings of your standard paradigm shift, where pundits with less neurological plasticity give future history books lots of look-how-wrong-they-were quotes.

I would like to mention two examples of such epic fails.

The Russell proof language

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.

The first formalized math wiki is here

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!

The next generation of proof assistants: ten questions

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?

How to Publish Counterexamples in 1 2 3 Easy Steps

I found some time to look over recent issues of Notices of AMS and I noticed a letter from Theodore P. Hill, a mathematician from Georgia Tech. The letter led me to read his article “How to Publish Counterexamples in 1 2 3 Easy Steps”. It’s a story that starts when he found errors in a mathematical paper that he got for review and traced those errors to a previously published article in Notices and ends almost two years later in pretty much a complete failure to cause any public admission of the problem and correction from the authors.

Goodbye ProofGeneral, again

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.