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.


Tags: , ,

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s

This site uses Akismet to reduce spam. Learn how your comment data is processed.

%d bloggers like this: