etiennecallies
commented
3 years ago I found this tool that compress/uncompress json object very well http://output.jsbin.com/cayuhox with algorithm lzma
I tried it with a proof of ⊢ ?(A⅋A), ?(B⅋B⅋B), ?(A^⅋B^), ?(⊥⊗⊥) (which is one the biggest I saw for the moment) and the result is only 1387 bytes long (1.4% of the total length), therefore can fit in a URL (max ~2000 characters).
Add a button to save the current proof, maybe by encoding json into a compact string and provide an url which uses it as an argument to display the proof back. If json is too verbose, maybe define an ad-hoc compressed representation of proofs or use marshaling (possibly on a datatype with minimal required information).