The KeYmaera X web UI allows you to view a completed proof. After finishing a proof, click on the “Browse Proof” button in the top right-hand corner of the user interface:
The proof browsing interface allows you to expand the proof from the bottom up. Therefore, when the viewer launches, you will see a single sequent with the profen property and an “Expand Details” button on the top of the horizontal line:
The proof browser shows each step in the proof at the same granularity that was used when constructing the proof. Therefore, you cannot step into automated tactics. If the “auto” tactic is used then you will only be able to see that you ran “auto” and the proof completed; you won’t be able to step into the individual proof steps executed by “auto”.
If the proof branches, then clicking the “Expand Details” link might result in multiple tabs. Just like in the proving interface, each tab corresponds to a branch of the proof:
The proof displayed by the proof viewer corresponds exactly to an underlying Bellerophon proof script. The proof script can be downloaded by going to the “proofs” page and clicking the file box dialog next to the relevant model:
Thanks to Miguel Velasquez for noticing that this feature was not properly documented and asking for details on the KeYmaera X mailing list. If you have any questions about KeYmaera X, please don’t hesitate to email me (firstname.lastname@example.org) or the Keymaera X mailing list.