We are sad to report the passing of long-time contributor Alan Sare
(Nov. 9, 1954 - Mar. 23, 2019).
Alan's first contribution to Metamath was a shorter proof for tfrlem8 in
2008.
He developed a tool called "completeusersproof" that assists developing
proofs using his "virtual deduction" method:
https://us.metamath.org/other.html#completeusersproof.
His virtual deduction method is explained in the comment for wvd1.
Below are some excerpts from his first emails to NM in 2007:
...I have been interested in proving set theory theorems for many years for
mental exercise. I enjoy it. I have used a book by Martin Zuckerman. It is
informal. I am interested in completely and perfectly proving theorems. Mr.
Zuckerman leaves out most of the steps of a proof, of course, like most
authors do, as you have noted. A complete proof for higher theorems would
require a volume of writing similar to the Metamath documents. So I am
frustrated when I am not capable of constructing a proof and Zuckerman leaves
out steps I do not understand. I could search for the steps in other texts,
but I don't do that too much. Metamath may be the answer for me....
...If we go beyond mathematics, I believe that it is possible to write down
all human knowledge in a way similar to the way you have explicated large
areas of mathematics. Of course, that would be a much, much more difficult
job. For example, it is possible to take a hard science like physics,
construct axioms based on experimental results, and to cast all of physics
into a collection of axioms and theorems. Maybe this has already been
attempted, although I am not familiar with it. When one then moves on to the
soft sciences such as social science, this job gets much more difficult. The
key is: All human thought consists of logical operations on abstract
objects. Usually, these logical operations are done informally. There is no
reason why one cannot take any subject and explicate it and take it down to
the indivisible postulates in a formal rigorous way....
...When I read a math book or an engineering book I come across something I
don't understand and I am compelled to understand it. But, often it is
hopeless. I don't have the time. Or, I would have to read the same thing by
multiple authors in the hope that different authors would give parts of the
working proof that others have omitted. It is very inefficient. Because I
have always been inclined to "get to the bottom" for a 100% fully understood
proof....