## Tiddly Formal Math

I have posted a TiddlyWiki rendering of two IsarMathLib theories at tiddlyspot. The theories are Finite_ZF about the finite powerset and Topology_ZF about basic general topology. The rendering looks as I expected with great display of mathematical symbols and structured proofs with subproofs expanded on demand. The only problem is the indentation. I don’t know of a good method of controlling indentation in TiddlyWiki. There is a “{{indent{ ” construct, but this indents only one line instead of a block of text and does not mix well with the sliders. The “===” markup that marks the end of the slider is not noticed by TiddlyWiki when inside an indented line. In addition, indentation achieved this way is too wide – some twelve characters instead of perhaps three that I need for to see something like



{

fix $k$

fix $x$

assume A5: $k\in n$,   $x\in X$

with A1 A3 have $a(k) \in Y$

using apply_funtype

with A2 A5 I have $(T(k))(x) = f\langle x,a(k)\rangle$

using fix_var_val

}



There is an old discussion on Gower’s Weblog where Gowers says

“Terry’s discussion of skeleton proofs is closely related to a fantasy I have had for a long time, which could I think become a reality. It’s to present mathematics in such a way that no step in any proof, no definition, nothing at all, is “magic”.”

Indeed, this can easily become a reality with the NestedSliderPlugin for TiddlyWiki. The reader could choose to see a short high level proof with the main points only, or expand the proofs of the facts that are unclear and see a very long and very detailed proof. Floating sliders can provide the statements of referenced theorems. This works very well to reduce verbosity of formally verifiable proofs as on the Tiddly Formal Math site, but would work for informal math too.