hckrnws

A few years back I made a concerted effort to learn Isabelle, the HOL based theorem prover. Proofs read a bit like natural languages but are fully rigorous, moreover Isabelle has application in math as well as programming. What's not to like.

What I found out was, that after diligently doing all the tutorials, and making all the exercises, there is still a huge gap between my skills and what is needed for real work. Note even that, you cannot even follow proofs of real theorems. Even with the reference manual in hand, trying to follow along word by word, there is a lot outright missing. From what I could gather, those that had successfully learned it did so at the hand of a master who explains the arcane incantations needed to get from proof state to proof state.

I'd still love to learn a formal theorem proving language, any one really, and be able to do formal proofs, but i'm not sure how. Coq seems even more arcane than Hol/Isabelle. I'm not sure about Lean, but I'm skeptical about learning it without having an expert on call.

It was a similar experience for me when I tried to learn proving with Isabelle/HOL without an expert help. I gave up and switched to Isabelle/ZF and that was easy, my standard mathematics background was sufficient. I use a subset of the Isar language that is needed for my formalized mathematics hobby (shameless plug: isarmathlib.org). Of course if your goal is software verification, then Isabelle/HOL is the way to go. Btw, Isabelle is not "the HOL based theorem prover", Isabelle/HOL is just its most popular logic.

This is a bit out of my area but...

> still a huge gap between my skills and what is needed for real work

That's kind of inevitable, you've passed your driving test but that doesn't mean you're ready to compete in Formula One race.

> Note even that, you cannot even follow proofs of real theorems

This may not be relevant to your experience or it may, but decades ago I did a tool-guided transformation of a very simple specification into a very simple program. This was done as a study for teaching people. I carefully explained every step as best I could, but the interesting thing was as my memory of doing it faded, the explanations became mainly useless – why I did a particular transformational step became lost, and my prior written explanations just didn't help. It's not like commenting code!

Now, maybe with extra experience I could do better these days, but quite possibly not. There is a certain kind of 'zone' you go into which has no parallel with programming. It may be that theorem proving at that level may only be something you can do, and do with practice, but can't follow afterwards; a state of mind. I don't know. FYI anyway.

I hear you. I picked up Isabelle relatively easily, but I had the good fortune to be at one of the places where Isabelle is developed, and actually became later part of that group for my PhD.

Still, even for me, dealing with various issues in Isabelle is frustrating (I will not even touch stuff like Coq or Lean, these are just insults on my mathematical senses). I know how this all can be made more accessible and natural and practical, and I am working on it. I, too, want to be using such a tool for real stuff. In particular, integrating LLMs with theorem provers is very promising, and I think the new logic I am developing is especially suited for it. You could argue, but well, a natural language interface is just the surface, and the complexity remains just under this surface. I would not argue against that in principle, but my new logic hopefully also takes care of a lot of unnecessary complexity and complications under the hood.

well, for lean I know there's a discord (with a fair amount of experts) and a fair share of resources nowadays. However, I did try 3 years ago and the jump between solving a simple algebra proof and contributing to Mathlib (or even understand something in it), is quite high.

Coq is well designed/easy to understand but it is missing a core mathlib like Lean. Moreover, most proofs are designed to "compile" quickly and not to be human readable.

Well, I think a DAG would generally be better than a tree for visually representing a proof. Because a premise can support multiple lemmas.

One site I've been working on uses graphs to generate arguments in that fashion:

http://concludia.org/

That's correct, in fact we would have a DAG if we displayed all possible arrows, but we conceal it to make the UI easier to interact with for the user. Hypotheses (green nodes) form many little trees, and goals (red trees) form a single tree. These must be trees, and not lattices, because that's just how Lean and Coq tactics work. However, tactics make use of hypotheses, and these can be displayed as arrows that connect hypotheses and goals, making it, in this sense, a DAG (here is an example, I moved the nodes a bit to make the arrows obvious https://github.com/Paper-Proof/paperproof/issues/9#issuecomm...). Concludia looks interesting, does it support first-order logic/ORs?

Propositional, so no exists or foralls, but yes for ORs and NOTs. Acyclic only.

Reminds me of characteristica universalis

Thanks for posting this. As a beginner, do I need to already know what "sequent-calculus-style trees" are for this to be useful?

I didn't see any broad explanation of what the tree structure means here. I can see that disjunctions split a branch into 2 branches, but I'm still pretty confused overall.

Sequent calculus trees [1] are straightforward. Essentially read them as: for each horizontal line, the judgment (assumptions ⊢ conclusion) below the line is valid if-and-only-if the judgments above the line are valid, by grace of the syntactic transformation rule named to the right of the line. These are stacked atop one another to form a tree, the leaves at the top (with nothing above the lines) being axioms of the system, the root at the bottom being the judgment whose proof is the tree.

Sometimes the trees are upside down from this, for reasons I haven't been able to divine. Some logics also permit multiple (alternative) conclusions in a judgment, which is then properly called a sequent.

Nearly the same notation is used for type judgements in type theory as well, with "assumptions ⊢ conclusion" being replaced by "environment ⊢ type assignments". [2]

[1] https://en.wikipedia.org/wiki/Sequent_calculus#The_system_LK (The preceding section introduces the notation but uses the upside-down variant, for unclear reasons -- I've rarely seen it elsewhere.)

[2] https://en.wikipedia.org/wiki/Type_theory#Technical_details

It isn't necessary to know theory for these visualisations to be useful, both Traf and Paperproof (and sequence calculus trees!) should, ideally, just reflect what's already happening in your mental image while you're writing a Lean/Coq/on-paper mathematical proof. But I agree it warrants a tutorial/explanation, got to write it. I think it might be particularly unclear what's happening if you're just looking at the full tree of the already-proved-theorem. As we're writing the proof, hypothesis nodes (green, what we have) move down; and goal nodes (red, what we want to have) move up. So it kind of goes from both sides to the center, and you should read it "from both sides to the center", takes getting used to. Here is a video of what's happening in Paperproof as we're writing the proof e.g.: https://www.youtube.com/watch?v=0dVj4ITAF1o.

Some searching found http://logitext.mit.edu/tutorial . It tries to explain sequent calculus with an interactive gui prover. Not sure how approachable it is... I've gotten too used to these things to know how to explain them properly.

Reminds me of Leslie Lamport’s „How to Write a Proof” [1]. I wonder whether there exist tools that aid in manually writing visualisable proofs?

https://lamport.azurewebsites.net/pubs/lamport-how-to-write....

Structured proofs as advocated for by Leslie Lamport are more reminiscent of natural deduction. One obvious difference with sequent calculus is that natural deduction only admits of a single goal for each proof step (though with multiple antecedents or conditions), whereas sequent calculus generalizes this to multiple goals which are understood disjunctively i.e. "at least one" has to be true. (The latter works well with the inherent duality of some types of logic, such as ordinary classical logic or linear logic. It doesn't seem to come up all that much when doing math practically, especially in areas close to CS where "direct" proofs are generally preferred.)

Thanks for the link. I've been reading Leslie Lamport's TLA works this year coincidentally, but never stumbled upon this one. His structured proofs would turn into a paperproof-style tree if he turned his 3.1.1.1. numbers into a tree, it's pretty close to paperproof conceptually.

I don't know of any software that allows for manual writing of such proofs yet, I'm drawing proof trees on paper at the moment. I would like paperproof to allow for this eventually. We want to enable ml-generation of tactics with ReProver, which will require the interface for the manual creation of goals and hypotheses. Hopefully after that it will be more clear what fully-manually-written proof interface could look like.

Interesting, the notation used in that paper presages the notation used by TLA⁺² [1]. I actually have written up an exposition of TLA⁺² proof steps using sequent calculus notation [2] with the intention of writing a proof visualizer for it.

[1] https://tla.msr-inria.inria.fr/tlaps/content/Documentation/T...

[2] https://chris.pacejo.net/stuff/tla-tips#proof-step-quick-ref...

Jonathon Gorard’s Abstract Proof Networks - in Mathematica - may be of interest

https://community.wolfram.com/groups/-/m/t/1135271

For the Coq proof assistant, a recent approach to graphical proofs is Actema: https://www.actema.xyz/

If there's one thing I never felt I properly learned in comp sci, it's proofs. I sucked at them, and I'm grateful I don't need them as part of my job.

That said, are there any good resources that can teach me how to reason through proofs better? Preferably for someone who has a weak mathmatical background? Aside from the Pidgeon Hole theorem, they never clicked with me.

> Metamath - Nothing?

Does their default proof explorer[1] not count?

[1] - https://us.metamath.org/mpeuni/mmtheorems.html

Cool idea. Here are about ~30 more that might be of interest. Not all are code proof assistants, just listing extras in case serendipity.

https://pastebin.com/bYXWj7w6

What is it with proof assistant designers and terrible naming instincts? "Lean" as a name collides with all sorts of business/engineering productivity frameworks "Lean software development", "lean business management", "running a lean startup". And of course Coq is phallic both in English and the original French. It must be the case that the people that design these things live in a separate plane of existence where these things don't bother them.

Yes, unfortunately, Lean is harder to search for than some other programming languages. Although it seems workable: both DuckDuckGo and Google return Lean-related top results for me for "lean induction" and "lean match expression," for example.

> And of course Coq is phallic both in English and the original French.

Is it phallic in French too? I am not a French speaker. According to the French Wiktionary, "coq" means rooster, male chicken, cooked rooster, male partridge, a self-important person, a rooster on top of a church bell tower, a loose coin, a tool used for ironing, a kind of fish, a part used in watchmaking, or a cook working on a ship.[1] None of these sound phallic to me.

I have not seen evidence that this was intended as an English pun. Rather, it seems to have been a double pun in French, for the calculus of constructions (CoC) which Coq is based on, and Thierry Coquand who developed CoC.[2] So I just assume that it wasn't meant to be phallic and remind myself that some people speak French and they name their software French names.

[1] https://fr.wiktionary.org/w/index.php?title=coq&oldid=325194...

[2] https://github.com/coq/coq/wiki/Alternative-names

It's practically impossible to pick names that haven't been used for something else. I've taken to using the contraction of random amusing phrases when I want a unique name, but this isn't any better. Just fun (for me).

Relevant example: my current toy proof engine and language is called lesc. There are lots of things called "lesc", but none of them to my knowledge stand for Less Elegant Space Cowboy.

you say that like it is a bad thing. Sign me up for the plane of existence without management frameworks please.

I love "Lean" actually, have you noticed ∃∀. Googling Lean concepts does primarily return the codeine syrup links though yes.

N for Natural numbers.

[dead]