Weekly log for 10 May 2026

I’m trying to keep a weekly log of “What I’ve been working on this week”. Let’s see how long I can keep writing…

Auditing courses

I’ve been auditing graduate Mathematics courses (algebraic geometry, graduate topology, undergraduate analysis [to kill an hour of time], and graduate abstract algebra) to think about formalizing them in Mizar, what subtleties would occur, and so on.

I’m really intrigued with Riemannian geometry. We just discussed Jacobi fields this past week. Although Mizar lacks the differential topology and differential geometry “infrastructure” for Jacobi fields, I think they should be straightforward to formalize.

Initially I thought Algebraic Geometry may be good to formalize in Mizar, plus it’d give me a chance to think about relating Algebraic Geometry to Differential Geometry. But I found out Algebraic Geometry is really just commutative algebra on steroids, with trace amounts of geometry sprinkled in for flavoring.

Out of books

I’ve run out of books to read when going to bed. I finished Elaine Cunningham’s “Starlight and Shadows” trilogy (which I thought was quite good, I’m not sure how I feel about the ending).

I’m trying to read Douglas Adams’ Hitchiker’s Guide to the Galaxy. It feels unbelievable—someone working at a radio station owns a home? That could never happen if they saved up working a dozen lifetimes. But this was apparently commonplace in Adams’ day…

I don’t think I can finish Hitchiker’s Guide, but I’m out of books, so…

Myo: The Proof Assistant

I have just announced last Saturday (May 2) Myo the proof assistant. It’s a metalogical framework, heavily inspired by Isabelle.

The foundations for Myo is Intuitionistic first-order logic plus Feferman’s FS0. In some sense, it might be tempting (but wrong) to think of Myo as “Hilbert’s programme as a proof assistant”. Instead, I am trying to investigate the “design space” for Mizar-like proof assistants. Metalogical frameworks are designed for these sorts of endeavours (“exploring the design space” and “proving results about the design”).

Literate program

Myo is a literate program implemented using Noweb. I am tempted to implement my own literate programming framework (since this is a part of the Yak Shavers’ Guild, the Yak Shaving must continue!). For now, I am content to use Noweb.

This is not a great example of literate programming, in my opinion. It assumes the reader is, well, just me. First, I’d need to identify my target audience.

If I wanted to target, say, pure Mathematicians, then I’d need to include a lot more motivating material (which I just don’t have the energy for, at the moment).

Eventually, I suspect I will build my own literate programming framework, and I am incredibly tempted to use my own poor man’s LaTeX atop plain TeX for stability. One task at a time…

Unit Tests

Last Tuesday, I added the unit testing framework. It’s a simple xUnit-style framework for writing unit tests in Standard ML.

I’ve been writing unit tests for the tactics, and caught a subtle bug in the Tactic.disch function when applied to a negated goal.

I foolishly have followed the HOL community’s DISCH_TAC to transform a negated goal Gamma ?- ~A into A,Gamma ?- False. The validation function had a bug in it for this particular case. Fortunately, I caught it using unit tests.

So it’s already paying off, but I should continue working on this.

Definition principles

I want to get to supporting definitions in Myo. This requires implementing a binary search tree (of some kind) and thinking through the definition principles for Intuitionistic first-order logic.

There are two things we can define in first-order logic: predicates and terms. Predicates are easier to define, they end up looking like:

Let $x_{1}$, …, $x_{n}$ be terms. We define the predicate $P[x_{1},\dots,x_{n}]$ to be the formula $\phi$.

In Mizar, a “definitional-theorem” is produced essentially of the form “$\forall x_{1},\dots, x_{n}\ldotp P[x_{1}, \dots, x_{N}]\iff\phi$”.

Terms are trickier, because we need to prove existence and uniqueness. Sometimes. If we have an “abbreviation”-type definition (“The term T equals [expression]”), then it’s already well-defined and we don’t need to do anything.

However, the other way to define a term is “Let $t_{1}$, …, $t_{k}$ be terms. The term $T(t_{1},\dots,t_{k})$ means the object satisfying formula $\phi$”. In this situation, we need to prove two things:

  1. Existence: there really does exist at least one object satisfying the formula. Formally, $\exists t\ldotp \phi[t_{1},\dots,t_{k},t]$
  2. Uniqueness: if there are two objects satisfying the same condition, then they must be equal to each other. Formally, $\forall u_{1}, u_{2}\ldotp (\phi[t_{1},\dots,t_{k},u_{1}]\land\phi[t_{1},\dots,t_{k},u_{2}])\implies u_{1}=u_{2}$.

In Mizar, we would then admit a “definitional-theorem” of the form: $\forall t_{1},\dots,t_{k}\ldotp\phi[t_{1},\dots,t_{k},T(t_{1},\dots,t_{k})]$.

Fortunately, there’s little logical difficulty in these principles. It’s just a matter of coding it up.

Aside: Feferman asserts that every Class-sorted term $A$ has a corresponding characteristic function-sorted term $c_{A}$ defined by $c_{A}(a)=0$ if $a\in A$ and $c_{A}(x)=1$ if $x\notin A$. But this does not seem possible to construct using the axioms alone. We can construct the class-sorted term $C:=\{(x,b)\mid (x\in A\land b=0)\lor(x\notin A\land b=1)\}$ and $C\cap\pi_{1}^{-1}{x}=\{(x,b)\}$. There is no obvious way to get a function-sorted term from this, however.

Detour on binary search trees

However, actually writing code to maintain the “database” or “dictionary” of definitions is a bit distracting. I have compiled a lot of notes over the years, and I’m just using them all when writing Myo. So I’ve written 8 pages in a day on binary trees just from these accumulated notes.

At any rate, I need to pick one binary search tree data structure. I don’t need to document all the binary search tree data structures I ever encountered and show how to implement them (although that would be fun). I only need one.

Future steps with Myo

I’m still deliberating over what to do next with Myo. There are several obvious paths in the short run:

The long run, there are many different things we could do:

There are even intermediate steps to consider, which are “bigger” than the short-run concerns but “smaller” than these long-run ideas:

Actually, one thing I am trying to maintain with the literate program is a sort of “linearity constraint”: the code from sections 1, 2, …, N should compile together and form a runnable program (even if it lacks a lot of features). “Dogfooding it” may produce a situation which violates this constraint.