Progress: HTML theorem display with interactivity

Skip to first unread message

Raph Levien

Sep 11, 2017, 11:16:43 AM9/11/17
I've made a fair amount of progress towards my goal of nicer HTML display of theorems. It's still rough and there's more I want to do, but I figured now is as good a checkpoint as any.

It's relatively easy to build from source, but I've also put files up on static serving:

Hovering over a proof step highlights the "arguments" of the step. Clicking on it brings up an info card. There's lots more that I want to put on the card (the statement of the theorem, the explicit substitution of the variables), but the fact that it displays the result line is a start.

Also note that the translation from Metamath is cruder than I'd like - it puts a label on every line whether needed or not, it makes lines for every step even if it could be inlined without parentheses.

Even though it's not quite my vision, I thought people on this list would like to see where I'm going with this.


Cris Perdue

Sep 13, 2017, 2:02:24 PM9/13/17
Hi Raph,

Could you review for us on the list your main goals for Ghilbert these days? I've had the impression that you have an interest in making Ghilbert in some way independent of a particular logic, or supporting interchange of proofs done in different logics?

By the way, I have admired your analysis of "bundling" of theorems in Metamath. If it is feasible to do, I would love to see a display of the multiple conventional theorems bundled into a Metamath theorem where this is the case.


You received this message because you are subscribed to the Google Groups "Ghilbert" group.
To unsubscribe from this group and stop receiving emails from it, send an email to
For more options, visit

Raph Levien

Sep 14, 2017, 10:38:42 AM9/14/17
Hi Cris,

I've written a draft of the goals here, but I'm not very satisfied with the document: . But it should be something of a start. Comments and discussion are welcome (I've already gotten some good feedback which I haven't integrated yet).

Yes, I want to support different logics, and in interchange. Lately I'm interested in supporting intuitionistic logic, so that proofs can be exported to Idris and Lean (the latter does support classical logic, but not by default).

I haven't gotten to the bundling just yet; I'm pushing on the fragment without bound variables for now. When I do, I'll try to have a reasonable presentation. Incidentally, one of the things that's missing from the current prototype is proper links back to the Metamath pages; not intentional, just something I haven't gotten around to doing yet.

Take care,


Jim Kingdon

Sep 14, 2017, 12:24:40 PM9/14/17
With respect to intuitionistic logic, I trust people have seen ? It is a development very much analogous to the propositional logic in metamath's Even adds in the law of the excluded middle and proves the "missing" theorems (in a straightforward way, rather than by going back to classical propositional logic axioms or the like) -

It is done in JHilbert (which is based on a rather old version of ghilbert), but that's not the interesting part. The interesting part (at least for me) was seeing how much of's propositional calculus carries over to intuitionistic logic, and how some of your classical habits can be replaced by ones which work intuitionistically.
Reply all
Reply to author
0 new messages