On Structured Proofs and the Declarative Proof Style

1. Suppose we have successfully formalized the classification theorem for finite simple groups in your favorite theorem prover (Lean, HOL, Coq, Mizar, whatever). In a century's time (or several centuries from now), do you think your theorem prover will still be around and backwards compatible? If not, what good would the formalization be?

1.1. Remark (Concerns have been partially realized). We stress, despite the concerns raised being hypothetical and distant, they have been partly realized already. The Automath project's efforts to translate Landau's Foundations of Analysis would have been lost to history but for Freek Wiedijk's heroic efforts. Or, hitting closer to home for many, Lean 3 broke compatibility with Lean 2; and, as I understand it, there still remains a large quantity of Lean 2 libraries not yet ported. Worse, Lean 4 broke compatibility with Lean 3, and the Xena project's library has not yet ported to Lean 4. The idea that we would encode mathematical knowledge in one single theorem prover seems riskier than encoding it in natural language. Why not try to have the best of both worlds?

2. Readable Proofs. One of the roles for proofs in mathematics is communication. Hence we need something analogous to the notion of "readable code" in programming: readable proofs. Consider the following proof, tell me what it does (no cheating!):

prove
 ('!p q. p * p = 2 * q * q ==> q = 0',
  MATCH_MP_TAC num_WF THEN REWRITE_TAC[RIGHT_IMP_FORALL_THM] THEN
  REPEAT STRIP_TAC THEN FIRST_ASSUM(MP_TAC o AP_TERM 'EVEN') THEN
  REWRITE_TAC[EVEN_MULT; ARITH] THEN REWRITE_TAC[EVEN_EXISTS] THEN
  DISCH_THEN(X_CHOOSE_THEN 'm:num' SUBST_ALL_TAC) THEN
  FIRST_X_ASSUM(MP_TAC o SPECL ['q:num'; 'm:num']) THEN
  POP_ASSUM MP_TAC THEN CONV_TAC SOS_RULE);;

Or the following:

Proof.
  rewrite EL2 with (p_prime := p_prime) (p_odd := p_odd) by (omega || auto).
  rewrite EL2 with (p_prime := q_prime) (p_odd := q_odd) by (omega || auto).
  rewrite m1_pow_compatible. rewrite <- m1_pow_morphism.
  f_equal. rewrite <- QR6. unfold a. unfold b. auto.
  rewrite <- Zmult_0_r with (n := (p - 1) / 2).
  apply Zmult_ge_compat_l. omega. omega.
Qed.

I honestly wouldn't guess the first example had to do with proving ${\sqrt{2}\notin\mathbb{Q}}$, nor would I have imagined the second had to do with the law of quadratic recipricocity. (The first in HOL Light, the second in Coq.) What do you suppose mathematicians of the 25th century would think of these proofs? Would our efforts formalizing mathematics in a theorem prover yield fruit akin to Euclid's Elements, or would it be more indecipherable than Russell and Whitehead's Principia?

Hence, I would like to assess the following question:

3. Puzzle. What qualities make a proof "readable"?

4. Sources. We're not in the wilderness on this matter. Some very smart people have thought very hard about this question. But we haven't progressed much in the past few decades, compared to designing programming languages. We all seem to draw waters from the same well.

Andrzej Trybulec created Mizar [10] specifically for readability. Over the years, Mizar went from an abstract idea to a concrete realization, iteratively improving its input language to make it resemble a working mathematician's proofs. A cynical critic may deride Mizar as merely natural deduction in Pascal syntax, but that concedes the point: it's readable and understandable on its own, without relying on the computer to tell us the "proof state" and remaining goals in a proof. (Empirically, it turns out that Mizar reflects how mathematicians write, based on a cursory glance at 40k articles; see Josef Urban's email to the Mizar mailing list.)

(For our earlier examples, I personally think that Mizar's proof of the theorem of quadratic recipricocity, Th49 of int_5.miz, while long, is clear and readable...even if I don't fully understand Mizar. Similarly, the proof that $\sqrt{2}\notin\mathbb{Q}$ is the first theorem in irrat_1.miz. It's longer than I would find in a textbook, as are all formal proofs, but I have no difficulty making sense of it.)

The other major source of inspiration, I think, is Mark Wenzel's Isar front-end for Isabelle [13] (and enlightening discussion of a prototype [12]). Here the system emerges bottom-up, as discussed in §3.2 of Wenzel's thesis [13]. Other theorem provers attempted to simply copy/paste Isar commands, but apparently they never caught on. I suspect this is due to copying the superficialities, rather than drawing upon the underlying principles, produced an awkward input language.

There are other sources worth perusing, like Zammit's "Structured Proof Language" [17] among others. We also mention Isar inspired many prototypes to adapt Mizar-style proofs to other theorem provers (Corbineau's Czar [2], Giero and Wiedijk's MMode [3], Harrison's Mizar Mode for HOL [4]). Also worth mentioning is ForTheL [11] which emerged from the Soviet SAD theorem prover [9], possibly a future input language for Lean.

I especially want to point out ForTheL [11] as a stand-out, partly because it was designed behind the Iron Curtain, and partly because it's more of a controlled language which resembles natural language.

5. Declarative proofs. One bit of terminology, John Harrison [5] calls the structured proof style "declarative style proofs", which seems fine. Some fanatics of the procedural camp dislike the term. Giero and Wiedijk [3] point out the differences between procedural and declarative styles are:

1. a procedural proof generally run backward (from goal to the assumptions), whereas declarative proofs run mostly forwards (from the assumptions to the goal);
2. a procedural proof generally does not have statements containing the statements which occur in the proof states, whereas declarative proofs do;
3. a procedural proofs have few proof cuts, whereas declarative proofs have nearly one cut for each proof step.

It turns out these qualities do make a difference on the readability of a proof script. But this is a bit like trying to learn an author's writing style by examining the statistics of the author's writing, like "Average number of words per sentence" or "Average number of syllables per word".

6. Natural deduction, vernacular. A key insight worth discussing further is that declarative/structured proofs emerge from the natural deduction calculus. Curiously, Jaśkowski [6] (who invented natural deduction independent of, and earlier than, Gentzen) does this in his original paper. Wiedijk [15] considers this avenue using a formal grammar for the proof steps, leaving notions like "term" and "formula" [i.e., the heart of a proposition/theorem] informal. So far, so good; but this has been predominantly first-order logic. How do we articulate readable proofs for type theory?

7. We construct proof steps for a declarative proof style by assigning "keywords" to rules of inference in natural deduction.

The problem with trying to find a readable proof format from natural deduction for type theory is, well, there are a lot more inference rules in the calculus of constructions (as opposed to, say, first-order logic).

The Lean4 developers have unwittingly started the road to reinventing lambda-typed lambda calculus, which has fewer rules and ostensibly could be encoded into a declarative proof style input.

8. One linguistic avenue may be found in de Bruijn's "mathematical vernacular" [1], which then evolved into WTT [7].

8.1. Remark (Soft typing). What's worth noting is de Bruijn [1] states in §1.17, "In particular we have a kind of meta-typing (the 'high typing', see Section 3.6) in the language, whereas most other systems would have such things in the metalanguage." We now call such 'high typing' either 'soft typing' [16], or 'semi-soft typing' [8].

9. Another avenue would be to weaken existing structured proof formats, so they become independent of foundations (e.g., instead of writing "${x\in\mathbb{N}}$", we would write "${x}$ be a natural number" — type theory provers would translate this into "${x{:}\mathbb{N}}$", and set theory provers would translate this into "${x\in\mathbb{N}}$" as before).

If GNU Hurd's failures have taught us anything about engineering, it's that "a bird in the hand is worth two in the bush." That is to say, it's wiser to take an existing working framework, and modify it slowly until it becomes what we want.

10. Conclusion? If this post seems less-than-satisfying, that's probably because I've only identified a problem. No solutions have been offered. That's because this is a hard problem somewhere between language design (very hard) and mathematical logic. Since we lack a robust framework for designing languages, this is far more of an art than science.

Although we have fewer than a half-dozen examples of declarative proof styles (really, maybe 3?), we have some avenues of exploration. But the design space may be much larger than we realize: we just lack the tools to describe it adequately.

One closing thought I'd pass off, though, is that type theorists encode logic in a rather protracted manner. It may be that structured proofs for type theory would be forced to "compile down" into many more steps, or maybe we just haven't adequately found a way to connect type theory to working mathematics.

Bibliography

1. Nick de Bruijn, "The Mathematical Vernacular". In Proceedings of the workshop on programming logic (eds. Peter Dybjer, Bengt Nordstrom, Kent Petersson, et al.), 1987. https://pure.tue.nl/ws/portalfiles/portal/4318923/599592.pdf
   
   See also F.3 of Selected Papers on Automath for a revised version of this manuscript.
2. Pierre Corbineau, "A Declarative Language For The Coq Proof Assistant". In Marino Miculan, Ivan Scagnetto, and Furio Honsell, editors, Types for Proofs and Programs, International Conference, TYPES 2007, Cividale des Friuli, Italy, May 2-5, 2007, Revised Selected Papers, volume 4941 of Lecture Notes in Computer Science, pages 69–84. Springer, 2007. https://kluedo.ub.uni-kl.de/frontdoor/deliver/index/docId/2100/file/B-065.pdf
3. Mariusz Giero and Freek Wiedijk, "MMode: A Mizar Mode for the proof assistant Coq". Technical report, ICIS, Radboud Universiteit Nijmegen, 2004. https://www.cs.ru.nl/ freek/mmode/mmode.pdf
4. John Harrison, "A Mizar Mode for HOL". In Proceedings of the 9th International Conference on Theorem Proving in Higher Order Logics, TPHOLs '96, volume 1125 of LNCS, pages 203–220. Springer, 1996. https://www.cl.cam.ac.uk/ jrh13/papers/mizar.html
5. John Harrison, "Proof Style". https://www.cl.cam.ac.uk/ jrh13/papers/style.html
6. Stanisław Jaśkowski "On the Rules of Suppositions in Formal Logic". Studia Logica 1 (1934) pp.5–32. https://www.logik.ch/daten/jaskowski.pdf
7. Fairouz Kamareddine and Rob Nederpelt, "A refinement of de Bruijn's formal language of mathematics". Journal of Logic, Language, and Information 13, 3 (2004), pp.287–340
8. Cezary Kaliszyk and Florian Rabe, "A Survey of Languages for Formalizing Mathematics". https://arxiv.org/abs/2005.12876
9. Alexander Lyaletski, "Evidence Algorithm Approach to Automated Theorem Proving and SAD Systems". http://ceur-ws.org/Vol-2833/Paper_14.pdf
10. Roman Matuszewski and Piotr Rudnicki, "Mizar: The First 30 Years". Mechanized Mathematics and Its Applications 4, 1 (2005) pp.3–24. http://mizar.org/people/romat/MatRud2005.pdf
11. Andrei Paskevich, "The syntax and semantics of the ForTheL language". Manuscript dated December 2007, http://nevidal.org/download/forthel.pdf
12. Markus Wenzel, "Isar — a Generic Interpretative Approach to Readable Formal Proof Documents". In Y. Bertot, G. Dowek, A. Hirschowitz, C. Paulin, L. Thery, editors, Theorem Proving in Higher Order Logics, TPHOLs'99, LNCS 1690, (c) Springer, 1999. https://www21.in.tum.de/ wenzelm/papers/Isar-TPHOLs99.pdf
13. Markus Wenzel, "Isabelle/Isar — a versatile environment for human-readable formal proof documents". PhD thesis, Institut für Informatik, Technische Universität München, 2002. https://mediatum.ub.tum.de/doc/601724/601724.pdf
14. Markus Wenzel and Free Wiedijk. "A comparison of the mathematical proof languages Mizar and Isar". Journal of Automated Reasoning 29 (2002), pp.389–411. https://www21.in.tum.de/~wenzelm/papers/romantic.pdf
15. Freek Wiedijk, "The Mathematical Vernacular". Undated manuscript (available since at least 2004), https://www.cs.ru.nl/ freek/notes/mv.pdf
16. Freek Wiedijk, "Mizar's Soft Type System". In: K.Schneider and J.Brandt (eds.), Theorem Proving in Higher Order Logics 2007, LNCS 4732, 383–399, 2007. https://cs.ru.nl/F.Wiedijk/mizar/miztype.pdf
17. Vincent Zammit, (1999) "On the Readability of Machine Checkable Formal Proofs". PhD Thesis, Kent University, 1999. https://kar.kent.ac.uk/21861/

The Next Generation of Theorem Provers

1. A parable. Back in the 1980s and '90s, there was a Cambrian explosion of CPU architectures: SPARC, POWER, PA-RISC, MIPS, and presumably many others. Each processor architecture had its own customized UNIX-like operating system (SPARC had Solaris née SunOS, POWER had AIX, PA-RISC had HP-UX, MIPS had IRIX, etc.).

If you wrote a program and compiled it for one architecture, but I worked on a computer with a different architecture, then you couldn't share your program with me: you had to send me your source code, and hopefully I had a compiler for the language you used, then I could compile your program for my computer.

Of course, this was a nuisance. Some compilers had special features which hindered porting programs. Thus motivated the Java programming language with the motto, "Write once, run anywhere".

2. Theorem Provers. The situation with theorem provers reminds me of the situation with competing CPU architectures in the '80s and '90s. If you wrote a proof in Lean (or Coq or HOL or...), and I work with Coq (or HOL or anything else), then I can't verify your proof in my system. Worse: I can't even "compile it" to my theorem prover. I would have to rewrite it from scratch.

2.1. Terminology. I'm going to generically refer to proof checkers, interactive theorem provers, and automatic theorem provers under the umbrella term Prover. This is non-standard, but the field is so small that any choice would be non-standard.

3. "Generations" of Provers. For the sake of clarity, I think it's useful to introduce a notion of "Generations of Provers", analogous to generations of programming languages.

"First generation provers" include: Automath, Metamath, possibly Twelf, and others lacking automation (or auto-generation of infrastructure, like inductive types which [when defined] introduce an induction principle). First generation provers require you do this manually.

"Second generation provers" range from LCF to HOL, Coq, and Lean (and, I would argue, Mizar). There is some degree of automation, the proof assistant does some of the heavy lifting for you, but you may be required to explicitly state some proof steps.

And that's where we are today: after about 70 years, we've got two "generations" of provers. (This isn't too bad, considering how few people have worked on theorem provers and proof assistants.) We emphasize that "generation" is used metaphorically for the "level of abstraction" afforded by the prover.

4. Hitting a moving target. Unlike the situation facing CPU architects or programming language designers, we who think about theorem provers are trying to formalize an evolving language (mathematics).

We could berate mathematicians for not using theorem provers. But then we have our "tower of Babel" problem, where your prover can't talk to mine. (Fanatics Evangelists resolve this problem by insisting on using their "one true Prover", but that's unrealistic and unmerited.)

A better alternative would be to try to come up with the "next generation" of provers. This is easy to say, hard to accomplish. And mathematicians would just say, "Well, can't we make it like LaTeX with custom macros for proving results?" Again: easier said than done.

Designing a language is very hard, even with simple requirements. But a step towards the next generation would be (I believe Freek Wiedijk pointed this out in some article) analogous to how compilers "eat in" a high level language, process it, and then "spit out" assembly. What's the "assembly language" of mathematics? Some first generation prover, like Metamath or Automath.

5. Designing a mathematical language. The way we have learned to design a programming language (from many years of trial and error): write many small programs in the proposed language, and in comments specify the intended outcome. This strategy applies to provers, as well: write down many examples of mathematics [definitions, theorems, proofs or proof sketches] in the hypothetical prover's vernacular, and comment on what it should be doing.

There is much freedom when designing a new prover's vernacular, and it's easy to "cheat". Simply say, "...and somehow the prover will magically do the following: ...".

Perhaps we can turn this on its head, and begin thinking about how to do mathematics as a controlled natural language? This is how I stumbled into theorem proving, running across Freek Wiedijk's note "The Mathematical Vernacular".

6. Semiformal mathematics: controlling the vernacular. I just started jotting these ideas down when I came across Jeremy Avigad's interesting recent paper, "The design of mathematical language". Although I agree with much of the paper, and I especially praise the use of "many small examples from mathematical literature" to guide the discussion, I thought it was limited in exploring the "design space" and eager to accept Lean's design decisions.

For example, consider the definition of a "normal subgroup". Are we defining an adjective ("normal") or a type modifier (since "subgroup" is a type, a "normal subgroup" would be a subtype of "subgroup") or a new type with implicit coercions (any "normal subgroup" is automatically a "subgroup", and satisfy the properties that a subgroup would have)?

Another undiscussed dimension to mathematical definitions (as a domain specific language) would be examining the "stuff, structure, and properties" idea of Baez and Dolan. This template gives us a lot "for free", and can be made somewhat "independent of foundations" by using objects in toposes. It's a small thing, but seldom discussed among provers.

The discussion also lacked adequate examples from applied mathematics (which, for me, would be things like weak solutions to PDEs, or theorems about regularity of PDEs, or something like that...my mind is focused on the Navier-Stokes equations). Granted, this is a domain where many mathematicians flinch and say, "Ouch, this is an unpleasant field." I do not intend it as a criticism, but an observation.

6.1. Analysis, Synthesis. The next natural step in Avigad's paper would be to move from analyzing examples to synthesizing some semi-formal "vernacular".

I honestly don't have a "semi-formal vernacular" at hand to present, but I have been using something similar to Wiedijk's vernacular for the past year. Since April or so of 2021, I have been transcribing my notes into a Zettelkasten (i.e., onto A6 size slips of paper). Proofs and proof sketches have been written using a slight variant of Wiedijk's vernacular.

It works fine for proofs, and forces me to fill in missing steps (or at least, make note of them). But I think proofs as a domain-specific language don't require much thought: we've had very smart people think about it for a century, and they came up with pretty good ideas (natural deduction, judgements, etc.). Now my task boils down to coming up with the right "reserved keywords" corresponding to the proof steps found in mathematical logic.

For definitions, in Field theory and Galois theory, most definitions don't neatly fit the "stuff, structure, properties" mould. This is great! Now I have some ready-to-present examples where it fails, namely whenever a definition looks like: "We call a gadget $G$ Hairy if [hairy property] holds." This occurs a lot in field theory and Galois theory. It also forces me to think deeply about what "species" of definition this is, and what's "really being defined" here.

6.2. Future of Provers? The short answer is, I don't know. The next steps may be to think about the "next generation" of provers, and try to move towards a "foundation independent framework" which resembles how working mathematicians actually operate.

But I think it's wrong-headed to say, as Leslie Lamport put it, mathematicians are "doing proofs wrong" because it resembles Euclid (and Euclid is old, thus bad). It's probably equally as misguided as suggesting that the design of the input language for provers is irrelevant, as any compiler designer will tell you, since this alienates the user-base and hinders adoptation.

Taken together, this suggests we need to make provers resemble "ordinary mathematics" as published and practiced by working mathematicians. Thus investigations along the lines of Avigad's article is well worth pursuing.

My intuition tells me that the third or fourth generation of Provers will resemble compilers, accepting more human intelligible input, producing "assembly code"-like output for a particular foundations of mathematics. Changing foundations would be a "one liner", if that. But what does the input language look like? That's hard to say.