Thanks for posting. I look forward to following along.

I have had chronic pain and other annoying functional neurological symptoms for the past 4 years. It started about halfway throughout my PhD.

I was born with congenital torticollis (fibrosis of the right sternocleidomastoid muscle) and had surgery for this twice when I was young. I also had 3 other surgical procedures for different reasons as a child.

Because my pain started in my neck and shoulder, I was set on believing that my previous surgeries were the cause of my pain. But as I learned more, meditated more, did yoga more, and faced pushback (and lots of confusion) from health professionals, it became clear that my symptoms are mainly "mind-body" (I hate that dualistic term).

I'd be very interested in talking more.

The presentation of the webpage is really really nice. Especially the highlighting/linking of mathematical definitions and bound variables.

How did you achieve this?

Aljoscha initially built the macro framework for the specs on willowprotocol.org

Thanks, that's all due to my co-author. Here's what we used: https://news.ycombinator.com/item?id=41589728 (link is to a post from @msy)

from a quick look, I believe the code for the page is here: https://github.com/g-trees/g_trees

Great paper for exploring the foundations of Isabelle. It's a shame the rest of the literature needed to properly understand Isabelle is scattered amongst many papers.

Any suggestions for those papers?