The recent issue of Notices contains an opinion piece by Melvyn B. Nathanson titled “Desperately Seeking Mathematical Truth”. The contents of this article can be summarized in the statement “Many (I think most) papers in most refereed journals are not refereed.” . This is the boldest public admission of the state of affairs from a mathematician I have ever seen.

Active researchers get one or two papers for review a week. Each of these papers would require two or more weeks if someone wanted to really check the proofs, line by line. This just can’t be done. So the reviewers cut corners. Sometimes they give the papers to graduate students to digest and report. But most of all, the reviewers rely on the reputation of the authors and the institutions they are affiliated with to make a judgment.

This of course has an impact on the quality of the proofs. I remember a case when as a graduate student I really wanted to get to the bottom of a proof of an important result. At some point the author of the paper I was reading referenced a theorem that could be found only in a very old edition of a known book. It took me more than a month to get the book as an interlibrary loan. And (not really) to my surprise it turned out that the theorem, although related to the subject could not be applied in the proof context. To me it was obvious that the author had made a concious effort to hide the fact that he did not know how make this step in the proof. However, what was the most surprising was that when I reported my findings to a specialist in the field, he did not see any problem. He knew how to fix the this step and he believed the result was correct. The fact that the the proof was not correct was of very minor importance.

The article in the Notices states the problem, but does not propose anything to fix it. To me the solution is obvious, and it is formalized mathematics. I started doing formalized mathematics as a hobby after I gave up on my mathematical career. It is a fun activity and excellent workout for my brain. And the mathematical truth is right there, no matter if the the proof is one page long or a thousand pages long. You can study a small piece of it with full confidence that there is no small mistake in the part you don’t want to dig into. And with the formal proof languages like Isar or Mizar that are based on natural language it takes little additional effort to understand what the proof is saying.

I don’t have much hope that formalized mathematics will become as important as the traditional one in my lifetime. The people who decide about such things are doing well enough in the current peer review system. But I think if only a couple of math departments started to teach writing machine verifiable proofs, there would be enough people doing it just for the fun. Those would be the people who love mathematics, but do not have access to the peer review system, like high school teachers or people who have chosen other careers like myself. Gradually, step by step, extensive libraries of basic facts could be created and writing cutting-edge research in formalized form would not be so prohibitively laborious.

But that will be the future. For now let me come back to the proof that identity is the only order automorphism of a linearly ordered finite set…

P.S. Sept. 09, 2008: See also a similar blog post at Process Algebra Diary.

Tags: formalized mathematics, reviews

August 2, 2008 at 9:02 pm |

I don’t have a lot of mathematical training, but I’m interested in getting back in and learning a bunch. But I hate the feeling of never knowing if the little doodles I’m doing contain a mistake or not. So a while ago I started writing a program that would let me manipulate mathematical statements efficiently and easily while also providing a formal proof that the manipulations were valid. Unfortunately, I lack the training to reduce it all to peano arithmetic. I wonder whether you might be able to give me some direction in how to go about it.

The first field I want to tackle is calculus. I made it through calculus 1 in college with an A, so I’m already pretty familiar with the first several chapters of my Shaum’s guide to calculus. But I want to be able to represent all the proofs presented in it in my program.

My first question would be whether you think it would be worth it to build on top of Isabelle as an engine, or if I might as well just write my own basic logic engine.

August 4, 2008 at 5:50 pm |

I suggest using Isabelle, or one of other existing theorem proving environments.

A bunch of provers are described in Freek Wiedijk’s

Seventeen Provers of the World> .

Do try a couple of them, it is an effort well spent.

If you really want to limit yourself to Peano Arithmetic, Metamath has a starting setup for that (called peano.mm). Otherwise, my personal favourite is Isabelle ZF.

July 28, 2010 at 2:37 am |

[…] clipped from slawekk.wordpress.com […]